012: Converting Verilog to BTOR page#

Abstract#

Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used to easily create complex designs from small HDL code. BTOR is a bit-precise word-level format for model checking. It is a simple format and easy to parse. It allows to model the model checking problem over the theory of bit-vectors with one-dimensional arrays, thus enabling to model Verilog designs with registers and memories. Yosys is an Open-Source Verilog synthesis tool that can be used to convert Verilog designs with simple assertions to BTOR format.

Download#

This document was originally published in November 2013: Converting Verilog to BTOR PDF