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.
|Title of host publication||Proceedings 9th International Conference on Application of Concurrency to System Design (ACSD'09, Augsburg, Germany, July 1-3, 2009)|
|Publisher||Institute of Electrical and Electronics Engineers|
|Publication status||Published - 2009|