Model Checking Verilog Descriptions of Cell Libraries

We present a formal semantics for a subset of Verilog, commonly used to describe cell libraries, in terms of transition systems. Such transition systems can serve as input to symbolic model checking, for example equivalence checking with a transistor netlist description. We implement our formal semantics as an encoding from the subset of Verilog to the input language of the SMV model-checker. Experiments show that this approach is able to verify complete cell libraries.

• Type: Conference
• Year: 2009
• Where: ACSD
• Authors: Matthias Raffelsieper, Jan-Willem Roorda, Mohammad Reza Mousavi
• Keywords: ACSD 2009, Cell Libraries, Formal Semantics, Hardware, Transition Systems