path: root/manual/APPNOTE_012_Verilog_to_BTOR.tex

% IEEEtran howto:
% http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
\documentclass[9pt,technote,a4paper]{IEEEtran}

\usepackage[T1]{fontenc}   % required for luximono!
\usepackage[scaled=0.8]{luximono}  % typewriter font with bold face

% To install the luximono font files:
% getnonfreefonts-sys --all        or
% getnonfreefonts-sys luximono
%
% when there are trouble you might need to:
% - Create /etc/texmf/updmap.d/99local-luximono.cfg
%   containing the single line: Map ul9.map
% - Run update-updmap followed by mktexlsr and updmap-sys
%
% This commands must be executed as root with a root environment
% (i.e. run "sudo su" and then execute the commands in the root
% shell, don't just prefix the commands with "sudo").

\usepackage[unicode,bookmarks=false]{hyperref}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{units}
\usepackage{nicefrac}
\usepackage{eurosym}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{algpseudocode}
\usepackage{scalefnt}
\usepackage{xspace}
\usepackage{color}
\usepackage{colortbl}
\usepackage{multirow}
\usepackage{hhline}
\usepackage{listings}
\usepackage{float}

\usepackage{tikz}
\usetikzlibrary{calc}
\usetikzlibrary{arrows}
\usetikzlibrary{scopes}
\usetikzlibrary{through}
\usetikzlibrary{shapes.geometric}

\lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}

\begin{document}

\title{Yosys Application Note 012: \\ Converting Verilog to BTOR}
\author{Ahmed Irfan and Clifford Wolf \\ April 2015}
\maketitle

\begin{abstract}
Verilog-2005 is a powerful Hardware Description Language (HDL) that
can be used to easily create complex designs from small HDL code.
BTOR~\cite{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~\cite{yosys} is an Open-Source Verilog
synthesis tool that can be used to convert Verilog designs with simple
assertions to BTOR format.

\end{abstract}

\section{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 {\tt TCL}
and {\tt ABC} support in the {\tt Makefile}.

\bigskip

This Application Note is based on GIT Rev. {\tt 082550f} from
2015-04-04 of Yosys~\cite{yosys}.

\section{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{btor}.

We provide a shell script {\tt verilog2btor.sh} which can be used to
convert a Verilog design to BTOR. The script can be found in the
{\tt backends/btor} directory. The following example shows its usage:

\begin{figure}[H]
\begin{lstlisting}[language=sh,numbers=none]
verilog2btor.sh fsm.v fsm.btor test
\end{lstlisting}
 \renewcommand{\figurename}{Listing}
\caption{Using verilog2btor script}
\end{figure}

The script {\tt verilog2btor.sh} takes three parameters.  In the above
example, the first parameter {\tt fsm.v} is the input design, the second
parameter {\tt fsm.btor} is the file name of BTOR output, and the third
parameter {\tt test} is the name of top module in the design.

To specify the properties (that need to be checked), we have two
options:
\begin{itemize}
\item We can use the Verilog {\tt assert} statement in the procedural block
  or module body of the Verilog design, as shown in
  Listing~\ref{specifying_property_assert}. This is the preferred option.
\item We can use a single-bit output wire, whose name starts with
  {\tt 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~\ref{specifying_property_output}.
\end{itemize}

\begin{figure}[H]
\begin{lstlisting}[language=Verilog,numbers=none]
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
\end{lstlisting}
\renewcommand{\figurename}{Listing}
\caption{Specifying property in Verilog design with {\tt assert}}
\label{specifying_property_assert}
\end{figure}

\begin{figure}[H]
\begin{lstlisting}[language=Verilog,numbers=none]
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
\end{lstlisting}
\renewcommand{\figurename}{Listing}
\caption{Specifying property in Verilog design with output wire}
\label{specifying_property_output}
\end{figure}

We can run Boolector~\cite{boolector}~$1.4.1$\footnote{
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.} on the generated BTOR
file:

\begin{figure}[H]
\begin{lstlisting}[language=sh,numbers=none]
$ boolector fsm.btor
unsat
\end{lstlisting}
 \renewcommand{\figurename}{Listing}
\caption{Running boolector on BTOR file}
\end{figure}

We can also use nuXmv~\cite{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.

\section{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 {\tt verilog2btor.sh} script.
Listing~\ref{btor_script_memory} shows the Yosys commands that are
executed by {\tt verilog2btor.sh}.

\begin{figure}[H]
\begin{lstlisting}[language=sh]
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;
\end{lstlisting}
 \renewcommand{\figurename}{Listing}
\caption{Synthesis Flow for BTOR with memories}
\label{btor_script_memory}
\end{figure}

Here is short description of what is happening in the script line by
line:

\begin{enumerate}
\item Reading the input file.
\item Setting the top module in the hierarchy and trying to read
  automatically the files which are given as {\tt include} in the file
  read in first line.
\item Checking the design hierarchy.
\item Converting processes to multiplexers (muxs) and flip-flops.
\item Removing undef signals from muxs.
\item Hiding all signal names that are not used as module ports.
\item Explicit type conversion, by introducing slice and concat cells
  in the circuit.
\item Converting write memories to synchronous memories, and
  collecting the memories to multi-port memories.
\item Flattening the design to get only one module.
\item Separating read and write memories.
\item Splitting the signals that are partially assigned
\item Setting undef to zero value.
\item Final optimization pass.
\item Writing BTOR file.
\end{enumerate}

For detailed description of the commands mentioned above, please refer
to the Yosys documentation, or run {\tt yosys -h \it 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 {\tt memory} at line
number~8. Listing~\ref{btor_script_without_memory} shows the
modified Yosys script file:

\begin{figure}[H]
\begin{lstlisting}[language=sh,numbers=none]
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;
\end{lstlisting}
 \renewcommand{\figurename}{Listing}
\caption{Synthesis Flow for BTOR without memories}
\label{btor_script_without_memory}
\end{figure}

\section{Example}

Here is an example Verilog design that we want to convert to BTOR:

\begin{figure}[H]
\begin{lstlisting}[language=Verilog,numbers=none]
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
\end{lstlisting}
\renewcommand{\figurename}{Listing}
\caption{Example - Verilog Design}
\label{example_verilog}
\end{figure}

The generated BTOR file that contain memories, using the script shown
in Listing~\ref{btor_script_memory}:
\begin{figure}[H]
\begin{lstlisting}[numbers=none]
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
\end{lstlisting}
\renewcommand{\figurename}{Listing}
\caption{Example - Converted BTOR with memory}
\label{example_btor}
\end{figure}

And the BTOR file obtained by the script shown in
Listing~\ref{btor_script_without_memory}, which expands the memory
into individual elements:
\begin{figure}[H]
\begin{lstlisting}[numbers=none,escapechar=@]
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

@\vbox to 0pt{\vss\vdots\vskip3pt}@
54 cond 1 53 50 52
55 root 1 -54

@\vbox to 0pt{\vss\vdots\vskip3pt}@
77 cond 8 76 3 44
78 cond 8 1 77 44
79 next 8 44 78
\end{lstlisting}
\renewcommand{\figurename}{Listing}
\caption{Example - Converted BTOR without memory}
\label{example_btor}
\end{figure}

\section{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 {\tt x} or {\tt 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.

\section{Conclusion}

Using the described flow, we can use Yosys to generate word-level
verification benchmarks with or without memories from Verilog designs.

\begin{thebibliography}{9}

\bibitem{yosys}
Clifford Wolf. The Yosys Open SYnthesis Suite. \\
\url{http://www.clifford.at/yosys/}

\bibitem{boolector}
Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays\\
\url{http://fmv.jku.at/boolector/}

\bibitem{btor}
Robert Brummayer and Armin Biere and Florian Lonsing, BTOR:
Bit-Precise Modelling of Word-Level Problems for Model Checking\\
\url{http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf}

\bibitem{nuxmv}
Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and
Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio
Mover and Marco Roveri and Stefano Tonetta, The nuXmv Symbolic Model
Checker\\
\url{https://es-static.fbk.eu/tools/nuxmv/index.php}

\end{thebibliography}


\end{document}