Formal model construction using HDL simulation semantics

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.