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.

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 [BBL08].

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:

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 Listing 16. 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 Listing 17.

Listing 16 Specifying property in Verilog design with 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

Listing 17 Specifying property in Verilog design with output wire¶

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

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. Listing 18 shows the Yosys commands that are executed by verilog2btor.sh.

Listing 18 Synthesis Flow for BTOR with memories¶

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. Listing 19 shows the modified Yosys script file:

Listing 19 Synthesis Flow for BTOR without memories¶

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:

Listing 20 Example - Verilog Design¶

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 Listing 21:

Listing 21 Example - Converted BTOR with memory¶

var 1 clk
array 8 3
var 8 $auto$rename.cc:150:execute$20
const 8 00000001
sub 8 3 4
slice 3 5 2 0
read 8 2 6
slice 3 3 2 0
add 8 3 4
const 8 00000000
ugt 1 3 10
not 1 11
const 8 11111111
slice 1 13 0 0
one 1
eq 1 1 15
and 1 16 14
write 8 3 2 8 3
acond 8 3 17 18 2
anext 8 3 2 19
eq 1 7 5
or 1 12 21
const 1 1
one 1
eq 1 23 24
cond 1 25 22 24
root 1 -26
cond 8 1 9 3
next 8 3 28

And the BTOR file obtained by the script shown in Listing 22, which expands the memory into individual elements:

Listing 22 Example - Converted BTOR with memory¶

var 1 clk
var 8 mem[0]
var 8 $auto$rename.cc:150:execute$20
slice 3 3 2 0
slice 1 4 0 0
not 1 5
slice 1 4 1 1
not 1 7
slice 1 4 2 2
not 1 9
and 1 8 10
and 1 6 11
cond 8 12 3 2
cond 8 1 13 2
next 8 2 14
const 8 00000001
add 8 3 16
const 8 00000000
ugt 1 3 18
not 1 19
var 8 mem[2]
and 1 7 10
and 1 6 22
cond 8 23 3 21
cond 8 1 24 21
next 8 21 25
sub 8 3 16

...

cond 1 53 50 52
root 1 -54

...

cond 8 76 3 44
cond 8 1 77 44
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.