Title :
Formal model construction using HDL simulation semantics
Author :
Buck, Joseph ; Wang, Dong ; Zhu, Yunshan
Author_Institution :
Synopsys Inc., Mountain View
Abstract :
All formal hardware verification tools in the market today interpret hardware description languages (HDLs) based on their synthesis semantics. This limits formal verification to synthesizable designs. The result, either a proof or a counterexample, produced by a formal tool can be inconsistent with simulation due to synthesis and simulation mismatches. And finally, conversion from a synthesized gate-level circuit to a formal model such as a Kripke structure or a Mealy machine is complex for designs containing gated clocks or latches. Existing solutions are often based on heuristics rather than language semantics. In this paper, we propose a new approach that constructs formal models based on simulation semantics. We symbolically simulate HDL designs using non-canonical word-level expressions to represent the values of design signals. We show that the formal model is consistent with simulation at specified sample points, which can be chosen to represent a clock cycle or a transaction. Our approach has been implemented in a tool called Simon. Experimental results show that Simon can efficiently construct formal models for large industrial designs.
Keywords :
formal verification; hardware description languages; simulation languages; Kripke structure; Mealy machine; formal model construction; formal verification; hardware description languages; hardware verification tools; simulation semantics; Automata; Circuit simulation; Circuit synthesis; Clocks; Formal verification; Hardware design languages; Latches; Logic arrays; Signal design; Testing; HDL simulation semantics; symbolic simulation; transaction level equivalence checking;
Conference_Titel :
High Level Design Validation and Test Workshop, 2007. HLVDT 2007. IEEE International
Conference_Location :
Irvine, CA
Print_ISBN :
978-1-4244-1480-2
DOI :
10.1109/HLDVT.2007.4392797