Verilog2SMV
Verilog2SMV is an opensource tool that takes a Verilog design with
simple SystemVerilog assertions and generates a model checking problem
at Register Transfer Level in SMV format. It handles natively memories
in the design using fixed size bit-vectors and arrays.
Verilog2SMV can also be used to generate model checking problems in
BTOR, AIGER, and VMT (using nuXmv).
Tool Download
DATE-2016 Submission
- date2016-paper-verilog2smv.pdf
Abstract: 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.
Authors
Verilog2SMV Page