aboutsummaryrefslogtreecommitdiffstats
path: root/manual/CHAPTER_Approach.tex
blob: 691225805996fd72b6420a2f2609f1213ba2ffa0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
\chapter{Approach}
\label{chapter:approach}

Yosys is a tool for synthesising (behavioural) Verilog HDL code to target architecture netlists. Yosys aims at a wide
range of application domains and thus must be flexible and easy to adapt to new tasks. This chapter covers the general
approach followed in the effort to implement this tool.

\section{Data- and Control-Flow}

The data- and control-flow of a typical synthesis tool is very similar to the data- and control-flow of a typical
compiler: different subsystems are called in a predetermined order, each consuming the data generated by the
last subsystem and generating the data for the next subsystem (see Fig.~\ref{fig:approach_flow}).

\begin{figure}[b]
	\hfil
	\begin{tikzpicture}
		\path (-1.5,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);
		\draw[fill=orange!10] ($ (cursor) + (1,-3) $) rectangle node[rotate=90] {Frontend} ++(1,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);
		\draw[fill=green!10] ($ (cursor) + (1,-3) $) rectangle node[rotate=90] {Pass} ++(1,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);
		\draw[fill=green!10] ($ (cursor) + (1,-3) $) rectangle node[rotate=90] {Pass} ++(1,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);
		\draw[fill=green!10] ($ (cursor) + (1,-3) $) rectangle node[rotate=90] {Pass} ++(1,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);
		\draw[fill=orange!10] ($ (cursor) + (1,-3) $) rectangle node[rotate=90] {Backend} ++(1,3) coordinate (cursor);
		\draw[-latex] ($ (cursor) + (0,-1.5) $) -- ++(1,0);

		\path (-3,-0.5) coordinate (cursor);
		\draw (cursor) -- node[below] {HDL} ++(3,0) coordinate (cursor);
		\draw[|-|] (cursor) -- node[below] {Internal Format(s)} ++(8,0) coordinate (cursor);
		\draw (cursor) -- node[below] {Netlist} ++(3,0);

		\path (-3,3.5) coordinate (cursor);
		\draw[-] (cursor) -- node[above] {High-Level} ++(3,0) coordinate (cursor);
		\draw[-] (cursor) -- ++(8,0) coordinate (cursor);
		\draw[->] (cursor) -- node[above] {Low-Level} ++(3,0);

	\end{tikzpicture}
	\caption{General data- and control-flow of a synthesis tool}
	\label{fig:approach_flow}
\end{figure}

The first subsystem to be called is usually called a {\it frontend}. It does not process the data generated by
another subsystem but instead reads the user input---in the case of a HDL synthesis tool, the behavioural
HDL code.

The subsystems that consume data from previous subsystems and produce data for the next subsystems (usually in the
same or a similar format) are called {\it passes}.

The last subsystem that is executed transforms the data generated by the last pass into a suitable output
format and writes it to a disk file. This subsystem is usually called the {\it backend}.

In Yosys all frontends, passes and backends are directly available as commands in the synthesis script. Thus
the user can easily create a custom synthesis flow just by calling passes in the right order in a synthesis
script.

\section{Internal Formats in Yosys}

Yosys uses two different internal formats. The first is used to store an abstract syntax tree (AST) of a verilog
input file. This format is simply called {\it AST} and is generated by the Verilog Frontend. This data structure
is consumed by a subsystem called {\it AST Frontend}\footnote{In Yosys the term {\it pass} is only used to
refer to commands that operate on the RTLIL data structure.}. This AST Frontend then generates a design in Yosys'
main internal format, the Register-Transfer-Level-Intermediate-Language (RTLIL) representation. It does that
by first performing a number of simplifications within the AST representation and then generating RTLIL from
the simplified AST data structure.

The RTLIL representation is used by all passes as input and outputs. This has the following advantages over
using different representational formats between different passes:

\begin{itemize}
\item The passes can be rearranged in a different order and passes can be removed or inserted.
\item Passes can simply pass-thru the parts of the design they don't change without the need
      to convert between formats. In fact Yosys passes output the same data structure they received
      as input and performs all changes in place.
\item All passes use the same interface, thus reducing the effort required to understand a pass
      when reading the Yosys source code, e.g.~when adding additional features.
\end{itemize}

The RTLIL representation is basically a netlist representation with the following additional features:

\begin{itemize}
\item An internal cell library with fixed-function cells to represent RTL datapath and register cells as well
as logical gate-level cells (single-bit gates and registers).
\item Support for multi-bit values that can use individual bits from wires as well as constant bits to
represent coarse-grain netlists.
\item Support for basic behavioural constructs (if-then-else structures and multi-case switches with
a sensitivity list for updating the outputs).
\item Support for multi-port memories.
\end{itemize}

The use of RTLIL also has the disadvantage of having a very powerful format
between all passes, even when doing gate-level synthesis where the more
advanced features are not needed. In order to reduce complexity for passes that
operate on a low-level representation, these passes check the features used in
the input RTLIL and fail to run when unsupported high-level constructs are
used. In such cases a pass that transforms the higher-level constructs to
lower-level constructs must be called from the synthesis script first.

\section{Typical Use Case}
\label{sec:typusecase}

The following example script may be used in a synthesis flow to convert the behavioural Verilog code
from the input file {\tt design.v} to a gate-level netlist {\tt synth.v} using the cell library
described by the Liberty file \citeweblink{LibertyFormat} {\tt cells.lib}:

\begin{lstlisting}[language=sh,numbers=left,frame=single]
# read input file tpo internal representation
read_verilog design.v

# convert high-level behavioral parts ("processes") to d-type flip-flops and muxes
proc

# perform some simple optimizations
opt

# convert high-level memory constructs to d-type flip-flops and multiplexers
memory

# perform some simple optimizations
opt

# convert design to (logical) gate-level netlists
techmap

# perform some simple optimizations
opt

# map internal register types to the ones from the cell library
dfflibmap -liberty cells.lib

# use ABC to map remaining logic to cells from the cell library
abc -liberty cells.lib

# cleanup
opt

# write results to output file
write_verilog synth.v
\end{lstlisting}

A detailed description of the commands available in Yosys can be found in App.~\ref{commandref}.
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 uninitilized, 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_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 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_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,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}