Merge pull request #55 from ahmedirfan1983/master

added appnote and impr in btor

4 files changed, 492 insertions, 27 deletions

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 <irfan@fbk.eu> - 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<RTLIL::IdString, bool> basic_wires;//input wires and registers	
 	RTLIL::IdString curr_cell; //current cell being dumped
 	std::map<std::string, std::string> cell_type_translation, s_cell_type_translation; //RTLIL to BTOR translation
-	std::set<int> mem_next; //if memory (line_number) already has next
+        std::map<int, std::set<std::pair<int,int>>> 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<std::pair<int,int>>& 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}