Verilog2SMV is an open source tool that takes a Verilog design with simple SystemVerilog assertions and generates a model checking problem at Register Transfer Level in SMV format.
For further information, please refer to the Verilog2SMV’s web page.