Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Annals of Computer Science and Information Systems

1 2017

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

A proof system for MDESL

Lu Jianyu, Xie Wanling, Zhu Huibiao, Fei Yuan

Annals of Computer Science and Information Systems

2017

Vol. 13

387--393

Hardware description language (HDL) Verilog has been standardized and widely used in industry. To describe the features such as event-driven computation, time and shared-variable concurrency of hardware, a Verilog-like language MDESL (multithreaded discrete event simulation language), has been introduced. In this paper, we put forward a proof system for MDESL which is based on the classical Hoare Logic (precondition, program, postcondition). To deal with the guard statement, we add a new element trace to Hoare triples. We extend the primitives of assertion to express the global time of current program, and interpret the triples so that it can verify both terminating and nonterminating computations. To verify a concurrent program, we use a merger method of the trace to combine the traces in our parallel rule. Finally, there is an example about using our proof system to verify the correctness of a program written by MDESL.