Verilog2SMV: A Tool for Word-level Verification

Verification is an essential step of the hardware design lifecycle. Usually verification is done at the gate level (Boolean level). We present verilog2smv, a tool that generates word-level model checking problems from Verilog designs augmented with assertions. A key aspect of our tool is that memories in the designs are treated without any form of abstraction. verilog2smv can be used for RTL verification by chaining with a word-level model checker like NUXMV. To this extent, we present also some experimental results over Verilog verification benchmarks, using verilog2smv+NUXMV as a tool-chain