From: Ahmed Irfan Date: Fri, 3 Apr 2015 14:20:29 +0000 (+0200) Subject: appnote for verilog to btor X-Git-Tag: yosys-0.6~367^2~6 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ad179151bc444eb7ee664b2145b41de199c4920;p=yosys.git appnote for verilog to btor --- diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex new file mode 100644 index 000000000..c441d9502 --- /dev/null +++ b/manual/APPNOTE_012_Verilog_to_BTOR.tex @@ -0,0 +1,435 @@ + +% 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 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, + output safety1); +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}