manual/APPNOTE_012_Verilog_to_BTOR.tex

   1
   2 % IEEEtran howto:
   3 % http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
   4 \documentclass[9pt,technote,a4paper]{IEEEtran}
   5
   6 \usepackage[T1]{fontenc}   % required for luximono!
   7 \usepackage[scaled=0.8]{luximono}  % typewriter font with bold face
   8
   9 % To install the luximono font files:
  10 % getnonfreefonts-sys --all        or
  11 % getnonfreefonts-sys luximono
  12 %
  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
  17 %
  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").
  21
  22 \usepackage[unicode,bookmarks=false]{hyperref}
  23 \usepackage[english]{babel}
  24 \usepackage[utf8]{inputenc}
  25 \usepackage{amssymb}
  26 \usepackage{amsmath}
  27 \usepackage{amsfonts}
  28 \usepackage{units}
  29 \usepackage{nicefrac}
  30 \usepackage{eurosym}
  31 \usepackage{graphicx}
  32 \usepackage{verbatim}
  33 \usepackage{algpseudocode}
  34 \usepackage{scalefnt}
  35 \usepackage{xspace}
  36 \usepackage{color}
  37 \usepackage{colortbl}
  38 \usepackage{multirow}
  39 \usepackage{hhline}
  40 \usepackage{listings}
  41 \usepackage{float}
  42
  43 \usepackage{tikz}
  44 \usetikzlibrary{calc}
  45 \usetikzlibrary{arrows}
  46 \usetikzlibrary{scopes}
  47 \usetikzlibrary{through}
  48 \usetikzlibrary{shapes.geometric}
  49
  50 \lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
  51
  52 \begin{document}
  53
  54 \title{Yosys Application Note 012: \\ Converting Verilog to BTOR}
  55 \author{Ahmed Irfan and Clifford Wolf \\ April 2015}
  56 \maketitle
  57
  58 \begin{abstract}
  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.
  68
  69 \end{abstract}
  70
  71 \section{Installation}
  72
  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.
  77
  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}.
  81
  82 \bigskip
  83
  84 This Application Note is based on GIT Rev. {\tt 082550f} from
  85 2015-04-04 of Yosys~\cite{yosys}.
  86
  87 \section{Quick Start}
  88
  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}.
  95
  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:
  99
 100 \begin{figure}[H]
 101 \begin{lstlisting}[language=sh,numbers=none]
 102 verilog2btor.sh fsm.v fsm.btor test
 103 \end{lstlisting}
 104  \renewcommand{\figurename}{Listing}
 105 \caption{Using verilog2btor script}
 106 \end{figure}
 107
 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.
 112
 113 To specify the properties (that need to be checked), we have two
 114 options:
 115 \begin{itemize}
 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}.
 124 \end{itemize}
 125
 126 \begin{figure}[H]
 127 \begin{lstlisting}[language=Verilog,numbers=none]
 128 module test(input clk, input rst, output y);
 129
 130   reg [2:0] state;
 131
 132   always @(posedge clk) begin
 133     if (rst || state == 3) begin
 134       state <= 0;
 135     end else begin
 136       assert(state < 3);
 137       state <= state + 1;
 138     end
 139   end
 140
 141   assign y = state[2];
 142
 143   assert property (y !== 1'b1);
 144
 145 endmodule
 146 \end{lstlisting}
 147 \renewcommand{\figurename}{Listing}
 148 \caption{Specifying property in Verilog design with {\tt assert}}
 149 \label{specifying_property_assert}
 150 \end{figure}
 151
 152 \begin{figure}[H]
 153 \begin{lstlisting}[language=Verilog,numbers=none]
 154 module test(input clk, input rst,
 155     output y, output safety1);
 156
 157   reg [2:0] state;
 158
 159   always @(posedge clk) begin
 160     if (rst || state == 3)
 161       state <= 0;
 162     else
 163       state <= state + 1;
 164   end
 165
 166   assign y = state[2];
 167
 168   assign safety1 = !(y !== 1'b1);
 169
 170 endmodule
 171 \end{lstlisting}
 172 \renewcommand{\figurename}{Listing}
 173 \caption{Specifying property in Verilog design with output wire}
 174 \label{specifying_property_output}
 175 \end{figure}
 176
 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
 181 file:
 182
 183 \begin{figure}[H]
 184 \begin{lstlisting}[language=sh,numbers=none]
 185 $ boolector fsm.btor
 186 unsat
 187 \end{lstlisting}
 188  \renewcommand{\figurename}{Listing}
 189 \caption{Running boolector on BTOR file}
 190 \end{figure}
 191
 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.
 195
 196 \section{Detailed Flow}
 197
 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}.
 204
 205 \begin{figure}[H]
 206 \begin{lstlisting}[language=sh]
 207 read_verilog -sv $1;
 208 hierarchy -top $3; hierarchy -libdir $DIR;
 209 hierarchy -check;
 210 proc; opt;
 211 opt_expr -mux_undef; opt;
 212 rename -hide;;;
 213 splice; opt;
 214 memory_dff -wr_only; memory_collect;;
 215 flatten;;
 216 memory_unpack;
 217 splitnets -driver;
 218 setundef -zero -undriven;
 219 opt;;;
 220 write_btor $2;
 221 \end{lstlisting}
 222  \renewcommand{\figurename}{Listing}
 223 \caption{Synthesis Flow for BTOR with memories}
 224 \label{btor_script_memory}
 225 \end{figure}
 226
 227 Here is short description of what is happening in the script line by
 228 line:
 229
 230 \begin{enumerate}
 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
 234   read in first line.
 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
 240   in the circuit.
 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.
 249 \end{enumerate}
 250
 251 For detailed description of the commands mentioned above, please refer
 252 to the Yosys documentation, or run {\tt yosys -h \it command\_name}.
 253
 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:
 259
 260 \begin{figure}[H]
 261 \begin{lstlisting}[language=sh,numbers=none]
 262 read_verilog -sv $1;
 263 hierarchy -top $3; hierarchy -libdir $DIR;
 264 hierarchy -check;
 265 proc; opt;
 266 opt_expr -mux_undef; opt;
 267 rename -hide;;;
 268 splice; opt;
 269 memory;;
 270 flatten;;
 271 splitnets -driver;
 272 setundef -zero -undriven;
 273 opt;;;
 274 write_btor $2;
 275 \end{lstlisting}
 276  \renewcommand{\figurename}{Listing}
 277 \caption{Synthesis Flow for BTOR without memories}
 278 \label{btor_script_without_memory}
 279 \end{figure}
 280
 281 \section{Example}
 282
 283 Here is an example Verilog design that we want to convert to BTOR:
 284
 285 \begin{figure}[H]
 286 \begin{lstlisting}[language=Verilog,numbers=none]
 287 module array(input clk);
 288
 289   reg [7:0] counter;
 290   reg [7:0] mem [7:0];
 291
 292   always @(posedge clk) begin
 293     counter <= counter + 8'd1;
 294     mem[counter] <= counter;
 295   end
 296
 297   assert property (!(counter > 8'd0) ||
 298     mem[counter - 8'd1] == counter - 8'd1);
 299
 300 endmodule
 301 \end{lstlisting}
 302 \renewcommand{\figurename}{Listing}
 303 \caption{Example - Verilog Design}
 304 \label{example_verilog}
 305 \end{figure}
 306
 307 The generated BTOR file that contain memories, using the script shown
 308 in Listing~\ref{btor_script_memory}:
 309 \begin{figure}[H]
 310 \begin{lstlisting}[numbers=none]
 311 1 var 1 clk
 312 2 array 8 3
 313 3 var 8 $auto$rename.cc:150:execute$20
 314 4 const 8 00000001
 315 5 sub 8 3 4
 316 6 slice 3 5 2 0
 317 7 read 8 2 6
 318 8 slice 3 3 2 0
 319 9 add 8 3 4
 320 10 const 8 00000000
 321 11 ugt 1 3 10
 322 12 not 1 11
 323 13 const 8 11111111
 324 14 slice 1 13 0 0
 325 15 one 1
 326 16 eq 1 1 15
 327 17 and 1 16 14
 328 18 write 8 3 2 8 3
 329 19 acond 8 3 17 18 2
 330 20 anext 8 3 2 19
 331 21 eq 1 7 5
 332 22 or 1 12 21
 333 23 const 1 1
 334 24 one 1
 335 25 eq 1 23 24
 336 26 cond 1 25 22 24
 337 27 root 1 -26
 338 28 cond 8 1 9 3
 339 29 next 8 3 28
 340 \end{lstlisting}
 341 \renewcommand{\figurename}{Listing}
 342 \caption{Example - Converted BTOR with memory}
 343 \label{example_btor}
 344 \end{figure}
 345
 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:
 349 \begin{figure}[H]
 350 \begin{lstlisting}[numbers=none,escapechar=@]
 351 1 var 1 clk
 352 2 var 8 mem[0]
 353 3 var 8 $auto$rename.cc:150:execute$20
 354 4 slice 3 3 2 0
 355 5 slice 1 4 0 0
 356 6 not 1 5
 357 7 slice 1 4 1 1
 358 8 not 1 7
 359 9 slice 1 4 2 2
 360 10 not 1 9
 361 11 and 1 8 10
 362 12 and 1 6 11
 363 13 cond 8 12 3 2
 364 14 cond 8 1 13 2
 365 15 next 8 2 14
 366 16 const 8 00000001
 367 17 add 8 3 16
 368 18 const 8 00000000
 369 19 ugt 1 3 18
 370 20 not 1 19
 371 21 var 8 mem[2]
 372 22 and 1 7 10
 373 23 and 1 6 22
 374 24 cond 8 23 3 21
 375 25 cond 8 1 24 21
 376 26 next 8 21 25
 377 27 sub 8 3 16
 378
 379 @\vbox to 0pt{\vss\vdots\vskip3pt}@
 380 54 cond 1 53 50 52
 381 55 root 1 -54
 382
 383 @\vbox to 0pt{\vss\vdots\vskip3pt}@
 384 77 cond 8 76 3 44
 385 78 cond 8 1 77 44
 386 79 next 8 44 78
 387 \end{lstlisting}
 388 \renewcommand{\figurename}{Listing}
 389 \caption{Example - Converted BTOR without memory}
 390 \label{example_btor}
 391 \end{figure}
 392
 393 \section{Limitations}
 394
 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}
 399 values of Verilog.
 400
 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.
 404
 405 \section{Conclusion}
 406
 407 Using the described flow, we can use Yosys to generate word-level
 408 verification benchmarks with or without memories from Verilog designs.
 409
 410 \begin{thebibliography}{9}
 411
 412 \bibitem{yosys}
 413 Clifford Wolf. The Yosys Open SYnthesis Suite. \\
 414 \url{http://www.clifford.at/yosys/}
 415
 416 \bibitem{boolector}
 417 Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays\\
 418 \url{http://fmv.jku.at/boolector/}
 419
 420 \bibitem{btor}
 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}
 424
 425 \bibitem{nuxmv}
 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
 429 Checker\\
 430 \url{https://es-static.fbk.eu/tools/nuxmv/index.php}
 431
 432 \end{thebibliography}
 433
 434
 435 \end{document}