diff options
Diffstat (limited to 'docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst')
| -rw-r--r-- | docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst | 333 |
1 files changed, 333 insertions, 0 deletions
diff --git a/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst new file mode 100644 index 000000000..e9e44d1cd --- /dev/null +++ b/docs/source/appendix/APPNOTE_012_Verilog_to_BTOR.rst @@ -0,0 +1,333 @@ +==================================== +012: Converting Verilog to BTOR page +==================================== + +Installation +============ + +Yosys written in C++ (using features from C++11) and is tested on modern Linux. +It should compile fine on most UNIX systems with a C++11 compiler. The README +file contains useful information on building Yosys and its prerequisites. + +Yosys is a large and feature-rich program with some dependencies. For this work, +we may deactivate other extra features such as TCL and ABC support in the +Makefile. + +This Application Note is based on `Yosys GIT`_ `Rev. 082550f` from 2015-04-04. + +.. _Yosys GIT: https://github.com/YosysHQ/yosys + +.. _Rev. 082550f: https://github.com/YosysHQ/yosys/tree/082550f + +Quick start +=========== + +We assume that the Verilog design is synthesizable and we also assume that the +design does not have multi-dimensional memories. As BTOR implicitly initializes +registers to zero value and memories stay uninitialized, we assume that the +Verilog design does not contain initial blocks. For more details about the BTOR +format, please refer to :cite:p:`btor`. + +We provide a shell script ``verilog2btor.sh`` which can be used to convert a +Verilog design to BTOR. The script can be found in the ``backends/btor`` +directory. The following example shows its usage: + +.. code:: sh + + verilog2btor.sh fsm.v fsm.btor test + +The script ``verilog2btor.sh`` takes three parameters. In the above example, the +first parameter ``fsm.v`` is the input design, the second parameter ``fsm.btor`` +is the file name of BTOR output, and the third parameter ``test`` is the name of +top module in the design. + +To specify the properties (that need to be checked), we have two +options: + +- We can use the Verilog ``assert`` statement in the procedural block or module + body of the Verilog design, as shown in :numref:`specifying_property_assert`. + This is the preferred option. + +- We can use a single-bit output wire, whose name starts with ``safety``. The + value of this output wire needs to be driven low when the property is met, + i.e. the solver will try to find a model that makes the safety pin go high. + This is demonstrated in :numref:`specifying_property_output`. + +.. code-block:: verilog + :caption: Specifying property in Verilog design with ``assert`` + :name: specifying_property_assert + + module test(input clk, input rst, output y); + + reg [2:0] state; + + always @(posedge clk) begin + if (rst || state == 3) begin + state <= 0; + end else begin + assert(state < 3); + state <= state + 1; + end + end + + assign y = state[2]; + + assert property (y !== 1'b1); + + endmodule + +.. code-block:: verilog + :caption: Specifying property in Verilog design with output wire + :name: specifying_property_output + + module test(input clk, input rst, + output y, output safety1); + + reg [2:0] state; + + always @(posedge clk) begin + if (rst || state == 3) + state <= 0; + else + state <= state + 1; + end + + assign y = state[2]; + + assign safety1 = !(y !== 1'b1); + + endmodule + +We can run `Boolector`_ ``1.4.1`` [1]_ on the generated BTOR file: + +.. _Boolector: http://fmv.jku.at/boolector/ + +.. code:: sh + + $ boolector fsm.btor + unsat + +We can also use `nuXmv`_, but on BTOR designs it does not support memories yet. +With the next release of nuXmv, we will be also able to verify designs with +memories. + +.. _nuXmv: https://es-static.fbk.eu/tools/nuxmv/index.php + +Detailed flow +============= + +Yosys is able to synthesize Verilog designs up to the gate level. We are +interested in keeping registers and memories when synthesizing the design. For +this purpose, we describe a customized Yosys synthesis flow, that is also +provided by the ``verilog2btor.sh`` script. :numref:`btor_script_memory` shows +the Yosys commands that are executed by ``verilog2btor.sh``. + +.. code-block:: yoscrypt + :caption: Synthesis Flow for BTOR with memories + :name: btor_script_memory + + read_verilog -sv $1; + hierarchy -top $3; hierarchy -libdir $DIR; + hierarchy -check; + proc; opt; + opt_expr -mux_undef; opt; + rename -hide;;; + splice; opt; + memory_dff -wr_only; memory_collect;; + flatten;; + memory_unpack; + splitnets -driver; + setundef -zero -undriven; + opt;;; + write_btor $2; + +Here is short description of what is happening in the script line by +line: + +#. Reading the input file. + +#. Setting the top module in the hierarchy and trying to read automatically the + files which are given as ``include`` in the file read in first line. + +#. Checking the design hierarchy. + +#. Converting processes to multiplexers (muxs) and flip-flops. + +#. Removing undef signals from muxs. + +#. Hiding all signal names that are not used as module ports. + +#. Explicit type conversion, by introducing slice and concat cells in the + circuit. + +#. Converting write memories to synchronous memories, and collecting the + memories to multi-port memories. + +#. Flattening the design to get only one module. + +#. Separating read and write memories. + +#. Splitting the signals that are partially assigned + +#. Setting undef to zero value. + +#. Final optimization pass. + +#. Writing BTOR file. + +For detailed description of the commands mentioned above, please refer +to the Yosys documentation, or run ``yosys -h <command_name>``. + +The script presented earlier can be easily modified to have a BTOR file that +does not contain memories. This is done by removing the line number 8 and 10, +and introduces a new command ``memory`` at line number 8. +:numref:`btor_script_without_memory` shows the modified Yosys script file: + +.. code-block:: sh + :caption: Synthesis Flow for BTOR without memories + :name: btor_script_without_memory + + read_verilog -sv $1; + hierarchy -top $3; hierarchy -libdir $DIR; + hierarchy -check; + proc; opt; + opt_expr -mux_undef; opt; + rename -hide;;; + splice; opt; + memory;; + flatten;; + splitnets -driver; + setundef -zero -undriven; + opt;;; + write_btor $2; + +Example +======= + +Here is an example Verilog design that we want to convert to BTOR: + +.. code-block:: verilog + :caption: Example - Verilog Design + :name: example_verilog + + module array(input clk); + + reg [7:0] counter; + reg [7:0] mem [7:0]; + + always @(posedge clk) begin + counter <= counter + 8'd1; + mem[counter] <= counter; + end + + assert property (!(counter > 8'd0) || + mem[counter - 8'd1] == counter - 8'd1); + + endmodule + +The generated BTOR file that contain memories, using the script shown in +:numref:`btor_memory`: + +.. code-block:: + :caption: Example - Converted BTOR with memory + :name: btor_memory + + 1 var 1 clk + 2 array 8 3 + 3 var 8 $auto$rename.cc:150:execute$20 + 4 const 8 00000001 + 5 sub 8 3 4 + 6 slice 3 5 2 0 + 7 read 8 2 6 + 8 slice 3 3 2 0 + 9 add 8 3 4 + 10 const 8 00000000 + 11 ugt 1 3 10 + 12 not 1 11 + 13 const 8 11111111 + 14 slice 1 13 0 0 + 15 one 1 + 16 eq 1 1 15 + 17 and 1 16 14 + 18 write 8 3 2 8 3 + 19 acond 8 3 17 18 2 + 20 anext 8 3 2 19 + 21 eq 1 7 5 + 22 or 1 12 21 + 23 const 1 1 + 24 one 1 + 25 eq 1 23 24 + 26 cond 1 25 22 24 + 27 root 1 -26 + 28 cond 8 1 9 3 + 29 next 8 3 28 + +And the BTOR file obtained by the script shown in +:numref:`btor_without_memory`, which expands the memory into individual +elements: + +.. code-block:: + :caption: Example - Converted BTOR with memory + :name: btor_without_memory + + 1 var 1 clk + 2 var 8 mem[0] + 3 var 8 $auto$rename.cc:150:execute$20 + 4 slice 3 3 2 0 + 5 slice 1 4 0 0 + 6 not 1 5 + 7 slice 1 4 1 1 + 8 not 1 7 + 9 slice 1 4 2 2 + 10 not 1 9 + 11 and 1 8 10 + 12 and 1 6 11 + 13 cond 8 12 3 2 + 14 cond 8 1 13 2 + 15 next 8 2 14 + 16 const 8 00000001 + 17 add 8 3 16 + 18 const 8 00000000 + 19 ugt 1 3 18 + 20 not 1 19 + 21 var 8 mem[2] + 22 and 1 7 10 + 23 and 1 6 22 + 24 cond 8 23 3 21 + 25 cond 8 1 24 21 + 26 next 8 21 25 + 27 sub 8 3 16 + + ... + + 54 cond 1 53 50 52 + 55 root 1 -54 + + ... + + 77 cond 8 76 3 44 + 78 cond 8 1 77 44 + 79 next 8 44 78 + +Limitations +=========== + +BTOR does not support initialization of memories and registers, i.e. they are +implicitly initialized to value zero, so the initial block for memories need to +be removed when converting to BTOR. It should also be kept in consideration that +BTOR does not support the ``x`` or ``z`` values of Verilog. + +Another thing to bear in mind is that Yosys will convert multi-dimensional +memories to one-dimensional memories and address decoders. Therefore +out-of-bounds memory accesses can yield unexpected results. + +Conclusion +========== + +Using the described flow, we can use Yosys to generate word-level verification +benchmarks with or without memories from Verilog designs. + +.. [1] + Newer version of Boolector do not support sequential models. + Boolector 1.4.1 can be built with picosat-951. Newer versions of + picosat have an incompatible API. |