Formal verification of vhdl designs using temporal logics
Subash Shankar, James Robert Slagle · 1998
Formal verification of hardware has been recognized to be essential for many domains. One particularly important class of problems in this area is the formal verification of hardware expressed in a hardware description language such as VHDL ((Very High Speed Integrated Circuit) Hardware Description Language) against specifications of temporal properties. Two major roadblocks are the lack of a formal semantics for VHDL, and the lack of efficient proof procedures for the resulting semantics. The research presented here addresses these two problems, and provides a means for using these results for formal verification. For sequential and concurrent programming languages, axiomatic semantics in temporal logics have been provided by others. The primary problem in extending these semantics to VHDL is the presence of the control flows in programming languages as well as an additional flow of simulation time. We tackle this problem by introducing a new type of polymodal logic that captures the semantics of VHDL control and time flows as distinct flows corresponding to the different modes of the logic. The second problem we address is propositional temporal logic theorem proving. There exist several tableau-based techniques for deciding temporal logic. However, these are sometimes limited in their applicability to the formal verification domain, since they do not generally allow for heuristics that can be used to guide the proof search. Connection methods have been successfully used to guide proof search in classical logics, but have not been applied to temporal logics. We provide a new concept of connections along with strategies that exploit these temporal connections to intelligently guide proof search in temporal logics, thus achieving many of the benefits of connection methods. A prototype theorem prover based on these concepts has been implemented and shown to result in significant efficiency improvements. Finally, we provide a scheme for relating our two approaches into a system that can be used for formal verification of VHDL designs.