mirror of https://github.com/YosysHQ/yosys.git
appnote added
This commit is contained in:
Ahmed Irfan
parent
d3c67ad9b6
commit
6c6cdf736a
|
|
@ -0,0 +1,434 @@
|
|||
|
||||
% 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);
|
||||
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}
|
||||
Loading…
Reference in New Issue