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


Verilog2SMV Page