manual/APPNOTE_012_Verilog_to_BTOR.tex - third_party/yosys - Git at Google


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

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