3 % http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
4 \documentclass[9pt,technote,
a4paper]{IEEEtran
}
6 \usepackage[T1]{fontenc} % required for luximono!
7 \usepackage[scaled=
0.8]{luximono
} % typewriter font with bold face
9 % To install the luximono font files:
10 % getnonfreefonts-sys --all or
11 % getnonfreefonts-sys luximono
13 % when there are trouble you might need to:
14 % - Create /etc/texmf/updmap.d/99local-luximono.cfg
15 % containing the single line: Map ul9.map
16 % - Run update-updmap followed by mktexlsr and updmap-sys
18 % This commands must be executed as root with a root environment
19 % (i.e. run "sudo su" and then execute the commands in the root
20 % shell, don't just prefix the commands with "sudo").
22 \usepackage[unicode,bookmarks=false
]{hyperref
}
23 \usepackage[english
]{babel
}
24 \usepackage[utf8
]{inputenc}
33 \usepackage{algpseudocode
}
45 \usetikzlibrary{arrows
}
46 \usetikzlibrary{scopes
}
47 \usetikzlibrary{through
}
48 \usetikzlibrary{shapes.geometric
}
50 \lstset{basicstyle=
\ttfamily,frame=trBL,xleftmargin=
2em,xrightmargin=
1em,numbers=left
}
54 \title{Yosys Application Note
012: \\ Converting Verilog to BTOR
}
55 \author{Ahmed Irfan and Clifford Wolf \\ April
2015}
59 Verilog-
2005 is a powerful Hardware Description Language (HDL) that
60 can be used to easily create complex designs from small HDL code.
61 BTOR~
\cite{btor
} is a bit-precise word-level format for model
62 checking. It is a simple format and easy to parse. It allows to model
63 the model checking problem over the theory of bit-vectors with
64 one-dimensional arrays, thus enabling to model Verilog designs with
65 registers and memories. Yosys~
\cite{yosys
} is an Open-Source Verilog
66 synthesis tool that can be used to convert Verilog designs with simple
67 assertions to BTOR format.
71 \section{Installation
}
73 Yosys written in C++ (using features from C++
11) and is tested on
74 modern Linux. It should compile fine on most UNIX systems with a
75 C++
11 compiler. The README file contains useful information on
76 building Yosys and its prerequisites.
78 Yosys is a large and feature-rich program with some dependencies. For
79 this work, we may deactivate other extra features such as
{\tt TCL
}
80 and
{\tt ABC
} support in the
{\tt Makefile
}.
84 This Application Note is based on GIT Rev.
{\tt 082550f
} from
85 2015-
04-
04 of Yosys~
\cite{yosys
}.
89 We assume that the Verilog design is synthesizable and we also assume
90 that the design does not have multi-dimensional memories. As BTOR
91 implicitly initializes registers to zero value and memories stay
92 uninitialized, we assume that the Verilog design does
93 not contain initial blocks. For more details about the BTOR format,
94 please refer to~
\cite{btor
}.
96 We provide a shell script
{\tt verilog2btor.sh
} which can be used to
97 convert a Verilog design to BTOR. The script can be found in the
98 {\tt backends/btor
} directory. The following example shows its usage:
101 \begin{lstlisting
}[language=sh,numbers=none
]
102 verilog2btor.sh fsm.v fsm.btor test
104 \renewcommand{\figurename}{Listing
}
105 \caption{Using verilog2btor script
}
108 The script
{\tt verilog2btor.sh
} takes three parameters. In the above
109 example, the first parameter
{\tt fsm.v
} is the input design, the second
110 parameter
{\tt fsm.btor
} is the file name of BTOR output, and the third
111 parameter
{\tt test
} is the name of top module in the design.
113 To specify the properties (that need to be checked), we have two
116 \item We can use the Verilog
{\tt assert
} statement in the procedural block
117 or module body of the Verilog design, as shown in
118 Listing~
\ref{specifying_property_assert
}. This is the preferred option.
119 \item We can use a single-bit output wire, whose name starts with
120 {\tt safety
}. The value of this output wire needs to be driven low
121 when the property is met, i.e. the solver will try to find a model
122 that makes the safety pin go high. This is demonstrated in
123 Listing~
\ref{specifying_property_output
}.
127 \begin{lstlisting
}[language=Verilog,numbers=none
]
128 module test(input clk, input rst, output y);
132 always @(posedge clk) begin
133 if (rst || state ==
3) begin
143 assert property (y !==
1'b1);
147 \renewcommand{\figurename}{Listing
}
148 \caption{Specifying property in Verilog design with
{\tt assert
}}
149 \label{specifying_property_assert
}
153 \begin{lstlisting
}[language=Verilog,numbers=none
]
154 module test(input clk, input rst,
155 output y, output safety1);
159 always @(posedge clk) begin
160 if (rst || state ==
3)
168 assign safety1 = !(y !==
1'b1);
172 \renewcommand{\figurename}{Listing
}
173 \caption{Specifying property in Verilog design with output wire
}
174 \label{specifying_property_output
}
177 We can run Boolector~
\cite{boolector
}~$
1.4.1$
\footnote{
178 Newer version of Boolector do not support sequential models.
179 Boolector
1.4.1 can be built with picosat-
951. Newer versions
180 of picosat have an incompatible API.
} on the generated BTOR
184 \begin{lstlisting
}[language=sh,numbers=none
]
188 \renewcommand{\figurename}{Listing
}
189 \caption{Running boolector on BTOR file
}
192 We can also use nuXmv~
\cite{nuxmv
}, but on BTOR designs it does not
193 support memories yet. With the next release of nuXmv, we will be also
194 able to verify designs with memories.
196 \section{Detailed Flow
}
198 Yosys is able to synthesize Verilog designs up to the gate level.
199 We are interested in keeping registers and memories when synthesizing
200 the design. For this purpose, we describe a customized Yosys synthesis
201 flow, that is also provided by the
{\tt verilog2btor.sh
} script.
202 Listing~
\ref{btor_script_memory
} shows the Yosys commands that are
203 executed by
{\tt verilog2btor.sh
}.
206 \begin{lstlisting
}[language=sh
]
208 hierarchy -top $
3; hierarchy -libdir $DIR;
211 opt_expr -mux_undef; opt;
214 memory_dff -wr_only; memory_collect;;
218 setundef -zero -undriven;
222 \renewcommand{\figurename}{Listing
}
223 \caption{Synthesis Flow for BTOR with memories
}
224 \label{btor_script_memory
}
227 Here is short description of what is happening in the script line by
231 \item Reading the input file.
232 \item Setting the top module in the hierarchy and trying to read
233 automatically the files which are given as
{\tt include
} in the file
235 \item Checking the design hierarchy.
236 \item Converting processes to multiplexers (muxs) and flip-flops.
237 \item Removing undef signals from muxs.
238 \item Hiding all signal names that are not used as module ports.
239 \item Explicit type conversion, by introducing slice and concat cells
241 \item Converting write memories to synchronous memories, and
242 collecting the memories to multi-port memories.
243 \item Flattening the design to get only one module.
244 \item Separating read and write memories.
245 \item Splitting the signals that are partially assigned
246 \item Setting undef to zero value.
247 \item Final optimization pass.
248 \item Writing BTOR file.
251 For detailed description of the commands mentioned above, please refer
252 to the Yosys documentation, or run
{\tt yosys -h
\it command
\_name}.
254 The script presented earlier can be easily modified to have a BTOR
255 file that does not contain memories. This is done by removing the line
256 number~
8 and
10, and introduces a new command
{\tt memory
} at line
257 number~
8. Listing~
\ref{btor_script_without_memory
} shows the
258 modified Yosys script file:
261 \begin{lstlisting
}[language=sh,numbers=none
]
263 hierarchy -top $
3; hierarchy -libdir $DIR;
266 opt_expr -mux_undef; opt;
272 setundef -zero -undriven;
276 \renewcommand{\figurename}{Listing
}
277 \caption{Synthesis Flow for BTOR without memories
}
278 \label{btor_script_without_memory
}
283 Here is an example Verilog design that we want to convert to BTOR:
286 \begin{lstlisting
}[language=Verilog,numbers=none
]
287 module array(input clk);
292 always @(posedge clk) begin
293 counter <= counter +
8'd1;
294 mem
[counter
] <= counter;
297 assert property (!(counter >
8'd0) ||
298 mem
[counter -
8'd1
] == counter -
8'd1);
302 \renewcommand{\figurename}{Listing
}
303 \caption{Example - Verilog Design
}
304 \label{example_verilog
}
307 The generated BTOR file that contain memories, using the script shown
308 in Listing~
\ref{btor_script_memory
}:
310 \begin{lstlisting
}[numbers=none
]
313 3 var
8 $auto$rename.cc:
150:execute$
20
341 \renewcommand{\figurename}{Listing
}
342 \caption{Example - Converted BTOR with memory
}
346 And the BTOR file obtained by the script shown in
347 Listing~
\ref{btor_script_without_memory
}, which expands the memory
348 into individual elements:
350 \begin{lstlisting
}[numbers=none,escapechar=@
]
353 3 var
8 $auto$rename.cc:
150:execute$
20
379 @
\vbox to
0pt
{\vss\vdots\vskip3pt}@
383 @
\vbox to
0pt
{\vss\vdots\vskip3pt}@
388 \renewcommand{\figurename}{Listing
}
389 \caption{Example - Converted BTOR without memory
}
393 \section{Limitations
}
395 BTOR does not support initialization of memories and registers, i.e. they are
396 implicitly initialized to value zero, so the initial block for
397 memories need to be removed when converting to BTOR. It should
398 also be kept in consideration that BTOR does not support the
{\tt x
} or
{\tt z
}
401 Another thing to bear in mind is that Yosys will convert multi-dimensional
402 memories to one-dimensional memories and address decoders. Therefore
403 out-of-bounds memory accesses can yield unexpected results.
407 Using the described flow, we can use Yosys to generate word-level
408 verification benchmarks with or without memories from Verilog designs.
410 \begin{thebibliography
}{9}
413 Clifford Wolf. The Yosys Open SYnthesis Suite. \\
414 \url{http://www.clifford.at/yosys/
}
417 Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays\\
418 \url{http://fmv.jku.at/boolector/
}
421 Robert Brummayer and Armin Biere and Florian Lonsing, BTOR:
422 Bit-Precise Modelling of Word-Level Problems for Model Checking\\
423 \url{http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf
}
426 Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and
427 Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio
428 Mover and Marco Roveri and Stefano Tonetta, The nuXmv Symbolic Model
430 \url{https://es-static.fbk.eu/tools/nuxmv/index.php
}
432 \end{thebibliography
}