diff --git a/backends/btor/README b/backends/btor/README index 26cb377c..fcfe1482 100644 --- a/backends/btor/README +++ b/backends/btor/README @@ -3,7 +3,7 @@ This is the Yosys BTOR backend. It is developed by Ahmed Irfan - Fondazione Bruno Kessler, Trento, Italy Master git repository for the BTOR backend: -https://github.com/ahmedirfan1983/yosys/tree/btor +https://github.com/ahmedirfan1983/yosys [[CITE]] BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking @@ -19,5 +19,5 @@ Todos: - async resets - etc.. -- Add support for $pmux and $lut cells +- Add support for $lut cells diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index c8fbf8d6..bcee505b 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -78,7 +78,7 @@ struct BtorDumper std::map basic_wires;//input wires and registers RTLIL::IdString curr_cell; //current cell being dumped std::map cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation - std::set mem_next; //if memory (line_number) already has next + std::map>> mem_next; // memory (line_number)'s set of condition and write BtorDumper(std::ostream &f, RTLIL::Module *module, RTLIL::Design *design, BtorDumperConfig *config) : f(f), module(module), design(design), config(config), ct(design), sigmap(module) { @@ -269,6 +269,45 @@ struct BtorDumper else return it->second; } + int dump_memory_next(const RTLIL::Memory* memory) + { + auto mem_it = line_ref.find(memory->name); + int address_bits = ceil(log(memory->size)/log(2)); + if(mem_it==std::end(line_ref)) + { + log("can not write next of a memory that is not dumped yet\n"); + log_abort(); + } + else + { + auto acond_list_it = mem_next.find(mem_it->second); + if(acond_list_it!=std::end(mem_next)) + { + std::set>& cond_list = acond_list_it->second; + if(cond_list.empty()) + { + return 0; + } + auto it=cond_list.begin(); + ++line_num; + str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, mem_it->second); + f << stringf("%s\n", str.c_str()); + ++it; + for(; it!=cond_list.end(); ++it) + { + ++line_num; + str = stringf("%d acond %d %d %d %d %d", line_num, memory->width, address_bits, it->first, it->second, line_num-1); + f << stringf("%s\n", str.c_str()); + } + ++line_num; + str = stringf("%d anext %d %d %d %d", line_num, memory->width, address_bits, mem_it->second, line_num-1); + f << stringf("%s\n", str.c_str()); + return 1; + } + return 0; + } + } + int dump_const(const RTLIL::Const* data, int width, int offset) { log("writing const \n"); @@ -775,7 +814,8 @@ struct BtorDumper str = cell->parameters.at(RTLIL::IdString("\\MEMID")).decode_string(); int mem = dump_memory(module->memories.at(RTLIL::IdString(str.c_str()))); //check if the memory has already next - auto it = mem_next.find(mem); + /* + auto it = mem_next.find(mem); if(it != std::end(mem_next)) { ++line_num; @@ -785,10 +825,11 @@ struct BtorDumper str = stringf("%d array %d %d", line_num, memory->width, address_bits); f << stringf("%s\n", str.c_str()); ++line_num; - str = stringf("%d eq 1 %d %d", line_num, mem, line_num - 1); + str = stringf("%d eq 1 %d %d; mem invar", line_num, mem, line_num - 1); f << stringf("%s\n", str.c_str()); mem = line_num - 1; - } + } + */ ++line_num; if(polarity) str = stringf("%d one 1", line_num); @@ -804,14 +845,15 @@ struct BtorDumper ++line_num; str = stringf("%d write %d %d %d %d %d", line_num, data_width, address_width, mem, address, data); f << stringf("%s\n", str.c_str()); + /* ++line_num; - str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2/*enable*/, line_num-1, mem); + str = stringf("%d acond %d %d %d %d %d", line_num, data_width, address_width, line_num-2, line_num-1, mem); f << stringf("%s\n", str.c_str()); ++line_num; str = stringf("%d anext %d %d %d %d", line_num, data_width, address_width, mem, line_num-1); f << stringf("%s\n", str.c_str()); - mem_next.insert(mem); - line_ref[cell->name]=line_num; + */ + mem_next[mem].insert(std::make_pair(line_num-1, line_num)); } else if(cell->type == "$slice") { @@ -975,6 +1017,12 @@ struct BtorDumper dump_cell(cell_it->second); } + log("writing memory next"); + for(auto mem_it = module->memories.begin(); mem_it != module->memories.end(); ++mem_it) + { + dump_memory_next(mem_it->second); + } + for(auto it: safety) dump_property(it); diff --git a/backends/btor/btor.ys b/backends/btor/btor.ys deleted file mode 100644 index ec28245d..00000000 --- a/backends/btor/btor.ys +++ /dev/null @@ -1,18 +0,0 @@ -proc; -opt; opt_const -mux_undef; opt; -rename -hide;;; -#converting pmux to mux -techmap -share_map pmux2mux.v;; -#explicit type conversion -splice; opt; -#extracting memories; -memory_dff -wr_only; memory_collect;; -#flatten design -flatten;; -#converting asyn memory write to syn memory -memory_unpack; -#cell output to be a single wire -splitnets -driver; -setundef -zero -undriven; -opt;;; - diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex new file mode 100644 index 00000000..c441d950 --- /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}