1 files changed, 0 insertions, 435 deletions
diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex
deleted file mode 100644
index aabdc63c4..000000000
--- a/manual/APPNOTE_012_Verilog_to_BTOR.tex
+++ /dev/null
@@ -1,435 +0,0 @@
-
-% 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 Claire Xenia 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}
-Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\
-\url{https://yosyshq.net/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}