A Proof System for MDESL
Jianyu Lu, Wanling Xie, Huibiao Zhu, Yuan Fei · Annals of Computer Science and Information Systems · 2017
Hardware description language (HDL) Verilog has been standardized and widely used in industry.To describe the features such as event-driven computation, time and sharedvariable 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.