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
+uninitialized, we assume that the Verilog design does
not contain initial blocks. For more details about the BTOR format,
please refer to~\cite{btor}.
\begin{figure}[H]
\begin{lstlisting}[language=sh,numbers=none]
-$ boolector fsm.btor
+$ 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
-support memories. With the next release of nuXmv, we will be also
+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}
\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;
+read_verilog -sv $1;
+hierarchy -top $3; hierarchy -libdir $DIR;
+hierarchy -check;
+proc; opt;
+opt_expr -mux_undef; opt;
rename -hide;;;
splice; opt;
memory_dff -wr_only; memory_collect;;
flatten;;
-memory_unpack;
+memory_unpack;
splitnets -driver;
setundef -zero -undriven;
opt;;;
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 Splitting the signals that are partially assigned
\item Setting undef to zero value.
\item Final optimization pass.
\item Writing BTOR 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;
+read_verilog -sv $1;
+hierarchy -top $3; hierarchy -libdir $DIR;
+hierarchy -check;
+proc; opt;
+opt_expr -mux_undef; opt;
rename -hide;;;
splice; opt;
memory;;
mem[counter] <= counter;
end
- assert property (!(counter > 8'd0) ||
+ assert property (!(counter > 8'd0) ||
mem[counter - 8'd1] == counter - 8'd1);
endmodule
Bit-Precise Modelling of Word-Level Problems for Model Checking\\
\url{http://fmv.jku.at/papers/BrummayerBiereLonsing-BPR08.pdf}
-\bibitem{nuxmv}
+\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