yosys/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 \\ November 2014}
\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 simple format and easy to parse.  It allows to model
the model checking problem over extensional 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 that are {\tt TCL},
{\tt Qt}, {\tt MiniSAT}, and {\tt yosys-abc} support in the {\tt
  Makefile}.

\bigskip

This Application Note is based on GIT Rev. {\tt d3c67ad} from
2014-09-22 of Yosys \cite{yosys}.
%The Verilog sources used for the examples are taken from
%yosys-bigsim \cite{bigsim}, a collection of real-world designs used for
%regression testing 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
uninitilized, we assume that the the Verilog design does
not contain initial block. 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 {\tt
  backends/btor} directory.  Following example shows its usage:

\begin{figure}[H]
\begin{lstlisting}[language=sh]
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, first parameter {\tt fsm.v} is the input design, second
parameter {\tt fsm.btor} is the file name of BTOR output, and 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 simple {\tt assert} command in the procedural block
  or continuous block of the Verilog design, as shown in
  Listing~\ref{specifying_property_assert}. This is preferred option.
\item We can use a output wire (single bit), whose name starts with
  {\tt safety}.  The value of this output wire needs to be handled in
  the Verilog code, as shown in
  Listing~\ref{specifying_property_output}.
\end{itemize}

\begin{figure}[H]
\begin{lstlisting}[language=Verilog]
module test(input clk, input rst, output y);
reg [2:0] state;
output safety1;
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]
module test(input clk, input rst, output y, 
  output safety1);
reg [2:0] state;
output safety1;
always @(posedge clk) begin
  if (rst || state == 3)
    state <= 0;
  else
    state <= state + 1;
end
assign y = state[2];
always @(*)
begin
  if (y !== 1'b1)
    safety1 <= 1;
  else
    safety1 <= 0;
end
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~$1.4$~\cite{boolector} on the generated BTOR
file.  The url for boolector provided in the references, contains
installation and usage guide.

We can also run nuXmv~\cite{nuxmv} but on the BTOR designs that does
not have memories. With the next release of nuXmv, we will be also
able to verify the designs with memories.

\section{Detailed Flow}

Yosys is able to synthesize the 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 as a script {\tt verilog2btor.sh} in Yosys
distribution. The following script shows the operations that are
performed in {\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_const -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 heirarchy.
\item Converting processes to multiplexers (muxs) and flip-flops.
\item Removing undef signals from muxs.
\item Hiding the signals that are not used.
\item Explicit type conversion, by introducing slice and concat cells
  in the circuit.
\item Converting write memories to synchronuos memories, and
  collecting the memories to multiport 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 documentation of Yosys~\cite{yosys}.

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.  Following is the modified yosys script file:

\begin{figure}[H]
\begin{lstlisting}[language=sh]
read_verilog -sv $1; 
hierarchy -top $3; hierarchy -libdir $DIR; 
hierarchy -check; 
proc; opt; 
opt_const -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]
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}

Here is 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]
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
\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 are
implicitly initialized to value zero, so the initial block for
memories need to be removed when converting to BTOR. This should be
also kept in consideration that BTOR does not handle multi-dimensional
memories, and does not support {\tt x} or {\tt z} value of Verilog.


\section{Conclusion}

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

\begin{thebibliography}{9}

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

%\bibitem{bigsim}
%yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\
%\url{https://github.com/cliffordwolf/yosys-bigsim}

%\bibitem{navre}
%Sebastien Bourdeauducq. Navré AVR clone (8-bit RISC). \\
%\url{http://opencores.org/project,navre}

%\bibitem{amber}
%Conor Santifort. Amber ARM-compatible core. \\
%\url{http://opencores.org/project,amber}

%\bibitem{ABC}
%Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. \\
%\url{http://www.eecs.berkeley.edu/~alanmi/abc/}

\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}