A Proof System For Multithreaded Discrete Event Simulation Language

With the rapid development of hardware description language(HDL),Verilog is widely used in digital circuit design and system design as a standard hardware description language.At the same time,as the requirements of the correctness of the HDL are getting higher and higher,formal verification method is used as one of the most effective verification methods.However,due to the fact that the existing theorem proving methods lacks some verification support for some of the special properties of HDL,such as event-driven computation and real-time properties,there is little formal verification work for HDL.This paper presents a new real-time Hoare Logic by modifying the classic Hoare Logic,then we put forward a proof system for HDL with the new Hoare Logic.Multithreaded Discrete Event Simulation Language(MDESL)is a formal lan-guage which is like Verilog.It has many features about the behavior of hardware,such as event-driven property,real-time property and shared variable concurrency.Based on the study of the semantic model of MDESL and combined with our pro-posed real-time Hoare Logic,we first give the rules of state behavior of the program and the sequential program.Then we give the rules of the guard statements in the parallel environment and parallel statements according to the concurrency model of MDESL.We also give the structural statements rules and auxiliary rules,and all those rules form a complete proof system for MDESL.This proof system can analyze and validate the characteristics of event-driven,real-time,and concurrent behavior based on discrete-time control in MDESL.This proof system not only enriches the semantic model of MDESL,but also lays a theoretical foundation for the study of semantic connection theory of MDESL.In addition,in order to prove the soundness of the system,we validate the reasoning rules in the system.Finally,we give an example to explain how to use our proof system to validate a parallel program described by MDESL.