====================================
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.