mirror of https://github.com/YosysHQ/yosys.git
And appnotes
This commit is contained in:
KrystalDelusion
parent
1eec255e60
commit
a955c42d6c
|
|
@ -1,466 +0,0 @@
|
|||
|
||||
% 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 010: \\ Converting Verilog to BLIF}
|
||||
\author{Claire Xenia Wolf \\ November 2013}
|
||||
\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. It is the preferred
|
||||
method of design entry for many designers\footnote{The other half prefers VHDL,
|
||||
a very different but -- of course -- equally powerful language.}.
|
||||
|
||||
The Berkeley Logic Interchange Format (BLIF) \cite{blif} is a simple file format for
|
||||
exchanging sequential logic between programs. It is easy to generate and
|
||||
easy to parse and is therefore the preferred method of design entry for
|
||||
many authors of logic synthesis tools.
|
||||
|
||||
Yosys \cite{yosys} is a feature-rich
|
||||
Open-Source Verilog synthesis tool that can be used to bridge the gap between
|
||||
the two file formats. It implements most of Verilog-2005 and thus can be used
|
||||
to import modern behavioral Verilog designs into BLIF-based design flows
|
||||
without dependencies on proprietary synthesis tools.
|
||||
|
||||
The scope of Yosys goes of course far beyond Verilog logic synthesis. But
|
||||
it is a useful and important feature and this Application Note will focus
|
||||
on this aspect of Yosys.
|
||||
\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 a couple of dependencies. It is,
|
||||
however, possible to deactivate some of the dependencies in the Makefile,
|
||||
resulting in features in Yosys becoming unavailable. When problems with building
|
||||
Yosys are encountered, a user who is only interested in the features of Yosys
|
||||
that are discussed in this Application Note may deactivate {\tt TCL}, {\tt Qt}
|
||||
and {\tt MiniSAT} support in the {\tt Makefile} and may opt against building
|
||||
{\tt yosys-abc}.
|
||||
|
||||
\bigskip
|
||||
|
||||
This Application Note is based on GIT Rev. {\tt e216e0e} from 2013-11-23 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{Getting Started}
|
||||
|
||||
We start our tour with the Navr\'e processor from yosys-bigsim. The Navr\'e
|
||||
processor \cite{navre} is an Open Source AVR clone. It is a single module ({\tt
|
||||
softusb\_navre}) in a single design file ({\tt softusb\_navre.v}). It also is
|
||||
using only features that map nicely to the BLIF format, for example it only
|
||||
uses synchronous resets.
|
||||
|
||||
Converting {\tt softusb\_navre.v} to {\tt softusb\_navre.blif} could not be
|
||||
easier:
|
||||
|
||||
\begin{figure}[H]
|
||||
\begin{lstlisting}[language=sh]
|
||||
yosys -o softusb_navre.blif -S softusb_navre.v
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{Calling Yosys without script file}
|
||||
\end{figure}
|
||||
|
||||
Behind the scenes Yosys is controlled by synthesis scripts that execute
|
||||
commands that operate on Yosys' internal state. For example, the {\tt -o
|
||||
softusb\_navre.blif} option just adds the command {\tt write\_blif
|
||||
softusb\_navre.blif} to the end of the script. Likewise a file on the
|
||||
command line -- {\tt softusb\_navre.v} in this case -- adds the command
|
||||
{\tt read\_verilog softusb\_navre.v} to the beginning of the
|
||||
synthesis script. In both cases the file type is detected from the
|
||||
file extension.
|
||||
|
||||
Finally the option {\tt -S} instantiates a built-in default synthesis script.
|
||||
Instead of using {\tt -S} one could also specify the synthesis commands
|
||||
for the script on the command line using the {\tt -p} option, either using
|
||||
individual options for each command or by passing one big command string
|
||||
with a semicolon-separated list of commands. But in most cases it is more
|
||||
convenient to use an actual script file.
|
||||
|
||||
\section{Using a Synthesis Script}
|
||||
|
||||
With a script file we have better control over Yosys. The following script
|
||||
file replicates what the command from the last section did:
|
||||
|
||||
\begin{figure}[H]
|
||||
\begin{lstlisting}[language=sh]
|
||||
read_verilog softusb_navre.v
|
||||
hierarchy
|
||||
proc; opt; memory; opt; techmap; opt
|
||||
write_blif softusb_navre.blif
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{\tt softusb\_navre.ys}
|
||||
\end{figure}
|
||||
|
||||
The first and last line obviously read the Verilog file and write the BLIF
|
||||
file.
|
||||
|
||||
\medskip
|
||||
|
||||
The 2nd line checks the design hierarchy and instantiates parametrized
|
||||
versions of the modules in the design, if necessary. In the case of this
|
||||
simple design this is a no-op. However, as a general rule a synthesis script
|
||||
should always contain this command as first command after reading the input
|
||||
files.
|
||||
|
||||
\medskip
|
||||
|
||||
The 3rd line does most of the actual work:
|
||||
|
||||
\begin{itemize}
|
||||
\item The command {\tt opt} is the Yosys' built-in optimizer. It can perform
|
||||
some simple optimizations such as const-folding and removing unconnected parts
|
||||
of the design. It is common practice to call opt after each major step in the
|
||||
synthesis procedure. In cases where too much optimization is not appreciated
|
||||
(for example when analyzing a design), it is recommended to call {\tt clean}
|
||||
instead of {\tt opt}.
|
||||
\item The command {\tt proc} converts {\it processes} (Yosys' internal
|
||||
representation of Verilog {\tt always}- and {\tt initial}-blocks) to circuits
|
||||
of multiplexers and storage elements (various types of flip-flops).
|
||||
\item The command {\tt memory} converts Yosys' internal representations of
|
||||
arrays and array accesses to multi-port block memories, and then maps this
|
||||
block memories to address decoders and flip-flops, unless the option {\tt -nomap}
|
||||
is used, in which case the multi-port block memories stay in the design
|
||||
and can then be mapped to architecture-specific memory primitives using
|
||||
other commands.
|
||||
\item The command {\tt techmap} turns a high-level circuit with coarse grain
|
||||
cells such as wide adders and multipliers to a fine-grain circuit of simple
|
||||
logic primitives and single-bit storage elements. The command does that by
|
||||
substituting the complex cells by circuits of simpler cells. It is possible
|
||||
to provide a custom set of rules for this process in the form of a Verilog
|
||||
source file, as we will see in the next section.
|
||||
\end{itemize}
|
||||
|
||||
Now Yosys can be run with the filename of the synthesis script as argument:
|
||||
|
||||
\begin{figure}[H]
|
||||
\begin{lstlisting}[language=sh]
|
||||
yosys softusb_navre.ys
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{Calling Yosys with script file}
|
||||
\end{figure}
|
||||
|
||||
\medskip
|
||||
|
||||
Now that we are using a synthesis script we can easily modify how Yosys
|
||||
synthesizes the design. The first thing we should customize is the
|
||||
call to the {\tt hierarchy} command:
|
||||
|
||||
Whenever it is known that there are no implicit blackboxes in the design, i.e.
|
||||
modules that are referenced but are not defined, the {\tt hierarchy} command
|
||||
should be called with the {\tt -check} option. This will then cause synthesis
|
||||
to fail when implicit blackboxes are found in the design.
|
||||
|
||||
The 2nd thing we can improve regarding the {\tt hierarchy} command is that we
|
||||
can tell it the name of the top level module of the design hierarchy. It will
|
||||
then automatically remove all modules that are not referenced from this top
|
||||
level module.
|
||||
|
||||
\medskip
|
||||
|
||||
For many designs it is also desired to optimize the encodings for the finite
|
||||
state machines (FSMs) in the design. The {\tt fsm} command finds FSMs, extracts
|
||||
them, performs some basic optimizations and then generate a circuit from
|
||||
the extracted and optimized description. It would also be possible to tell
|
||||
the {\tt fsm} command to leave the FSMs in their extracted form, so they can be
|
||||
further processed using custom commands. But in this case we don't want that.
|
||||
|
||||
\medskip
|
||||
|
||||
So now we have the final synthesis script for generating a BLIF file
|
||||
for the Navr\'e CPU:
|
||||
|
||||
\begin{figure}[H]
|
||||
\begin{lstlisting}[language=sh]
|
||||
read_verilog softusb_navre.v
|
||||
hierarchy -check -top softusb_navre
|
||||
proc; opt; memory; opt; fsm; opt; techmap; opt
|
||||
write_blif softusb_navre.blif
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{{\tt softusb\_navre.ys} (improved)}
|
||||
\end{figure}
|
||||
|
||||
\section{Advanced Example: The Amber23 ARMv2a CPU}
|
||||
|
||||
Our 2nd example is the Amber23 \cite{amber}
|
||||
ARMv2a CPU. Once again we base our example on the Verilog code that is included
|
||||
in yosys-bigsim \cite{bigsim}.
|
||||
|
||||
\begin{figure}[b!]
|
||||
\begin{lstlisting}[language=sh]
|
||||
read_verilog a23_alu.v
|
||||
read_verilog a23_barrel_shift_fpga.v
|
||||
read_verilog a23_barrel_shift.v
|
||||
read_verilog a23_cache.v
|
||||
read_verilog a23_coprocessor.v
|
||||
read_verilog a23_core.v
|
||||
read_verilog a23_decode.v
|
||||
read_verilog a23_execute.v
|
||||
read_verilog a23_fetch.v
|
||||
read_verilog a23_multiply.v
|
||||
read_verilog a23_ram_register_bank.v
|
||||
read_verilog a23_register_bank.v
|
||||
read_verilog a23_wishbone.v
|
||||
read_verilog generic_sram_byte_en.v
|
||||
read_verilog generic_sram_line_en.v
|
||||
hierarchy -check -top a23_core
|
||||
add -global_input globrst 1
|
||||
proc -global_arst globrst
|
||||
techmap -map adff2dff.v
|
||||
opt; memory; opt; fsm; opt; techmap
|
||||
write_blif amber23.blif
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{\tt amber23.ys}
|
||||
\label{aber23.ys}
|
||||
\end{figure}
|
||||
|
||||
The problem with this core is that it contains no dedicated reset logic.
|
||||
Instead the coding techniques shown in Listing~\ref{glob_arst} are used to
|
||||
define reset values for the global asynchronous reset in an FPGA
|
||||
implementation. This design can not be expressed in BLIF as it is. Instead we
|
||||
need to use a synthesis script that transforms this form to synchronous resets that
|
||||
can be expressed in BLIF.
|
||||
|
||||
(Note that there is no problem if this coding techniques are used to model
|
||||
ROM, where the register is initialized using this syntax but is never updated
|
||||
otherwise.)
|
||||
|
||||
\medskip
|
||||
|
||||
Listing~\ref{aber23.ys} shows the synthesis script for the Amber23 core. In
|
||||
line 17 the {\tt add} command is used to add a 1-bit wide global input signal
|
||||
with the name {\tt globrst}. That means that an input with that name is added
|
||||
to each module in the design hierarchy and then all module instantiations are
|
||||
altered so that this new signal is connected throughout the whole design
|
||||
hierarchy.
|
||||
|
||||
\begin{figure}[t!]
|
||||
\begin{lstlisting}[language=Verilog]
|
||||
reg [7:0] a = 13, b;
|
||||
initial b = 37;
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{Implicit coding of global asynchronous resets}
|
||||
\label{glob_arst}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[b!]
|
||||
\begin{lstlisting}[language=Verilog]
|
||||
(* techmap_celltype = "$adff" *)
|
||||
module adff2dff (CLK, ARST, D, Q);
|
||||
|
||||
parameter WIDTH = 1;
|
||||
parameter CLK_POLARITY = 1;
|
||||
parameter ARST_POLARITY = 1;
|
||||
parameter ARST_VALUE = 0;
|
||||
|
||||
input CLK, ARST;
|
||||
input [WIDTH-1:0] D;
|
||||
output reg [WIDTH-1:0] Q;
|
||||
|
||||
wire [1023:0] _TECHMAP_DO_ = "proc";
|
||||
|
||||
wire _TECHMAP_FAIL_ =
|
||||
!CLK_POLARITY || !ARST_POLARITY;
|
||||
|
||||
always @(posedge CLK)
|
||||
if (ARST)
|
||||
Q <= ARST_VALUE;
|
||||
else
|
||||
Q <= D;
|
||||
|
||||
endmodule
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{\tt adff2dff.v}
|
||||
\label{adff2dff.v}
|
||||
\end{figure}
|
||||
|
||||
In line 18 the {\tt proc} command is called. But in this script the signal name
|
||||
{\tt globrst} is passed to the command as a global reset signal for resetting
|
||||
the registers to their assigned initial values.
|
||||
|
||||
Finally in line 19 the {\tt techmap} command is used to replace all instances
|
||||
of flip-flops with asynchronous resets with flip-flops with synchronous resets.
|
||||
The map file used for this is shown in Listing~\ref{adff2dff.v}. Note how the
|
||||
{\tt techmap\_celltype} attribute is used in line 1 to tell the techmap command
|
||||
which cells to replace in the design, how the {\tt \_TECHMAP\_FAIL\_} wire in
|
||||
lines 15 and 16 (which evaluates to a constant value) determines if the
|
||||
parameter set is compatible with this replacement circuit, and how the {\tt
|
||||
\_TECHMAP\_DO\_} wire in line 13 provides a mini synthesis-script to be used to
|
||||
process this cell.
|
||||
|
||||
\begin{figure*}
|
||||
\begin{lstlisting}[language=C]
|
||||
#include <stdint.h>
|
||||
#include <stdbool.h>
|
||||
|
||||
#define BITMAP_SIZE 64
|
||||
#define OUTPORT 0x10000000
|
||||
|
||||
static uint32_t bitmap[BITMAP_SIZE/32];
|
||||
|
||||
static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); }
|
||||
static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; }
|
||||
static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; }
|
||||
|
||||
int main() {
|
||||
uint32_t i, j, k;
|
||||
output(2);
|
||||
for (i = 0; i < BITMAP_SIZE; i++) {
|
||||
if (bitmap_get(i)) continue;
|
||||
output(3+2*i);
|
||||
for (j = 2*(3+2*i);; j += 3+2*i) {
|
||||
if (j%2 == 0) continue;
|
||||
k = (j-3)/2;
|
||||
if (k >= BITMAP_SIZE) break;
|
||||
bitmap_set(k);
|
||||
}
|
||||
}
|
||||
output(0);
|
||||
return 0;
|
||||
}
|
||||
\end{lstlisting}
|
||||
\renewcommand{\figurename}{Listing}
|
||||
\caption{Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled using
|
||||
GCC 4.6.3 for ARM with {\tt -Os -marm -march=armv2a -mno-thumb-interwork
|
||||
-ffreestanding}, linked with {\tt -{}-fix-v4bx} set and booted with a custom
|
||||
setup routine written in ARM assembler.}
|
||||
\label{sieve}
|
||||
\end{figure*}
|
||||
|
||||
\section{Verification of the Amber23 CPU}
|
||||
|
||||
The BLIF file for the Amber23 core, generated using Listings~\ref{aber23.ys}
|
||||
and \ref{adff2dff.v} and the version of the Amber23 RTL source that is bundled
|
||||
with yosys-bigsim, was verified using the test-bench from yosys-bigsim.
|
||||
It successfully executed the program shown in Listing~\ref{sieve} in the
|
||||
test-bench.
|
||||
|
||||
For simulation the BLIF file was converted back to Verilog using ABC
|
||||
\cite{ABC}. So this test includes the successful transformation of the BLIF
|
||||
file into ABC's internal format as well.
|
||||
|
||||
The only thing left to write about the simulation itself is that it probably
|
||||
was one of the most energy inefficient and time consuming ways of successfully
|
||||
calculating the first 31 primes the author has ever conducted.
|
||||
|
||||
\section{Limitations}
|
||||
|
||||
At the time of this writing Yosys does not support multi-dimensional memories,
|
||||
does not support writing to individual bits of array elements, does not
|
||||
support initialization of arrays with {\tt \$readmemb} and {\tt \$readmemh},
|
||||
and has only limited support for tristate logic, to name just a few
|
||||
limitations.
|
||||
|
||||
That being said, Yosys can synthesize an overwhelming majority of real-world
|
||||
Verilog RTL code. The remaining cases can usually be modified to be compatible
|
||||
with Yosys quite easily.
|
||||
|
||||
The various designs in yosys-bigsim are a good place to look for examples
|
||||
of what is within the capabilities of Yosys.
|
||||
|
||||
\section{Conclusion}
|
||||
|
||||
Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses, but
|
||||
one is to provide an easy gateway from high-level Verilog code to low-level
|
||||
logic circuits.
|
||||
|
||||
The command line option {\tt -S} can be used to quickly synthesize Verilog
|
||||
code to BLIF files without a hassle.
|
||||
|
||||
With custom synthesis scripts it becomes possible to easily perform high-level
|
||||
optimizations, such as re-encoding FSMs. In some extreme cases, such as the
|
||||
Amber23 ARMv2 CPU, the more advanced Yosys features can be used to change a
|
||||
design to fit a certain need without actually touching the RTL code.
|
||||
|
||||
\begin{thebibliography}{9}
|
||||
|
||||
\bibitem{yosys}
|
||||
Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\
|
||||
\url{https://yosyshq.net/yosys/}
|
||||
|
||||
\bibitem{bigsim}
|
||||
yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\
|
||||
\url{https://github.com/YosysHQ/yosys-bigsim}
|
||||
|
||||
\bibitem{navre}
|
||||
Sebastien Bourdeauducq. Navr\'e 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{blif}
|
||||
Berkeley Logic Interchange Format (BLIF) \\
|
||||
\url{http://vlsi.colorado.edu/~vis/blif.ps}
|
||||
|
||||
\end{thebibliography}
|
||||
|
||||
|
||||
\end{document}
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -1,3 +0,0 @@
|
|||
module cmos_demo(input a, b, output [1:0] y);
|
||||
assign y = a + b;
|
||||
endmodule
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
digraph "cmos_demo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c10 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g0\nNOR|{}}" ];
|
||||
c11 [ shape=record, label="{{<p7> A|<p9> Y}|$g1\nNOT|{}}" ];
|
||||
c12 [ shape=record, label="{{<p7> A|<p9> Y}|$g2\nNOT|{}}" ];
|
||||
c13 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g3\nNOR|{}}" ];
|
||||
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
|
||||
x0:e -> c13:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c14 [ shape=record, label="{{<p7> A|<p8> B|<p9> Y}|$g4\nNOR|{}}" ];
|
||||
x1 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
|
||||
x1:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
|
||||
x2:e -> c14:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
n1 [ shape=diamond, label="$n4" ];
|
||||
n1:e -> c10:p9:w [color="black", label=""];
|
||||
n1:e -> c14:p7:w [color="black", label=""];
|
||||
n2 [ shape=diamond, label="$n5" ];
|
||||
n2:e -> c11:p9:w [color="black", label=""];
|
||||
n2:e -> c13:p7:w [color="black", label=""];
|
||||
n3 [ shape=diamond, label="$n6_1" ];
|
||||
n3:e -> c12:p9:w [color="black", label=""];
|
||||
n3:e -> c13:p8:w [color="black", label=""];
|
||||
n4:e -> c10:p8:w [color="black", label=""];
|
||||
n4:e -> c12:p7:w [color="black", label=""];
|
||||
n5:e -> c10:p7:w [color="black", label=""];
|
||||
n5:e -> c11:p7:w [color="black", label=""];
|
||||
n6:e -> x0:s0:w [color="black", label=""];
|
||||
n6:e -> x1:s0:w [color="black", label=""];
|
||||
n6:e -> x2:s0:w [color="black", label=""];
|
||||
}
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
digraph "cmos_demo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="y[0]", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="y[1]", color="black", fontcolor="black" ];
|
||||
c11 [ shape=record, label="{{<p8> A|<p9> B}|$g0\nNOR|{<p10> Y}}" ];
|
||||
c12 [ shape=record, label="{{<p8> A}|$g1\nNOT|{<p10> Y}}" ];
|
||||
c13 [ shape=record, label="{{<p8> A}|$g2\nNOT|{<p10> Y}}" ];
|
||||
c14 [ shape=record, label="{{<p8> A|<p9> B}|$g3\nNOR|{<p10> Y}}" ];
|
||||
c15 [ shape=record, label="{{<p8> A|<p9> B}|$g4\nNOR|{<p10> Y}}" ];
|
||||
c11:p10:e -> c15:p8:w [color="black", label=""];
|
||||
c12:p10:e -> c14:p8:w [color="black", label=""];
|
||||
c13:p10:e -> c14:p9:w [color="black", label=""];
|
||||
n4:e -> c11:p9:w [color="black", label=""];
|
||||
n4:e -> c13:p8:w [color="black", label=""];
|
||||
n5:e -> c11:p8:w [color="black", label=""];
|
||||
n5:e -> c12:p8:w [color="black", label=""];
|
||||
c15:p10:e -> n6:w [color="black", label=""];
|
||||
c14:p10:e -> n7:w [color="black", label=""];
|
||||
n7:e -> c15:p9:w [color="black", label=""];
|
||||
}
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
module example(input clk, a, b, c,
|
||||
output reg [1:0] y);
|
||||
always @(posedge clk)
|
||||
if (c)
|
||||
y <= c ? a + b : 2'd0;
|
||||
endmodule
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
read_verilog example.v
|
||||
show -format dot -prefix example_00
|
||||
proc
|
||||
show -format dot -prefix example_01
|
||||
opt
|
||||
show -format dot -prefix example_02
|
||||
|
||||
cd example
|
||||
select t:$add
|
||||
show -format dot -prefix example_03
|
||||
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
digraph "example" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n4 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c12 [ shape=record, label="{{<p9> A|<p10> B}|$2\n$add|{<p11> Y}}" ];
|
||||
v0 [ label="2'00" ];
|
||||
c14 [ shape=record, label="{{<p9> A|<p10> B|<p13> S}|$3\n$mux|{<p11> Y}}" ];
|
||||
p1 [shape=box, style=rounded, label="PROC $1\nexample.v:3"];
|
||||
c12:p11:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c14:p11:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n4:e -> c12:p9:w [color="black", label=""];
|
||||
n5:e -> c12:p10:w [color="black", label=""];
|
||||
n6:e -> c14:p13:w [color="black", label=""];
|
||||
n6:e -> p1:w [color="black", label=""];
|
||||
n7:e -> p1:w [color="black", label=""];
|
||||
p1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n8:e -> p1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v0:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
digraph "example" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n6 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n8 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n9 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c14 [ shape=record, label="{{<p11> A|<p12> B}|$2\n$add|{<p13> Y}}" ];
|
||||
c18 [ shape=record, label="{{<p15> CLK|<p16> D}|$7\n$dff|{<p17> Q}}" ];
|
||||
c20 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$5\n$mux|{<p13> Y}}" ];
|
||||
v0 [ label="2'00" ];
|
||||
c21 [ shape=record, label="{{<p11> A|<p12> B|<p19> S}|$3\n$mux|{<p13> Y}}" ];
|
||||
x1 [shape=box, style=rounded, label="BUF"];
|
||||
x2 [shape=box, style=rounded, label="BUF"];
|
||||
n1 [ shape=diamond, label="$0\\y[1:0]" ];
|
||||
x2:e:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c18:p17:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n10:e -> c20:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c14:p13:e -> c21:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3 [ shape=point ];
|
||||
c20:p13:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> c18:p16:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> x2:w:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x1:e:e -> c20:p19:w [color="black", label=""];
|
||||
c21:p13:e -> c20:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> c14:p11:w [color="black", label=""];
|
||||
n7:e -> c14:p12:w [color="black", label=""];
|
||||
n8:e -> c21:p19:w [color="black", label=""];
|
||||
n8:e -> x1:w:w [color="black", label=""];
|
||||
n9:e -> c18:p15:w [color="black", label=""];
|
||||
v0:e -> c21:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
digraph "example" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n3 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n4 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c11 [ shape=record, label="{{<p8> A|<p9> B}|$2\n$add|{<p10> Y}}" ];
|
||||
c15 [ shape=record, label="{{<p12> CLK|<p13> D}|$7\n$dff|{<p14> Q}}" ];
|
||||
c17 [ shape=record, label="{{<p8> A|<p9> B|<p16> S}|$5\n$mux|{<p10> Y}}" ];
|
||||
c17:p10:e -> c15:p13:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c11:p10:e -> c17:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> c11:p8:w [color="black", label=""];
|
||||
n4:e -> c11:p9:w [color="black", label=""];
|
||||
n5:e -> c17:p16:w [color="black", label=""];
|
||||
n6:e -> c15:p12:w [color="black", label=""];
|
||||
c15:p14:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n7:e -> c17:p8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
digraph "example" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
v0 [ label="a" ];
|
||||
v1 [ label="b" ];
|
||||
v2 [ label="$2_Y" ];
|
||||
c4 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
|
||||
v0:e -> c4:p1:w [color="black", label=""];
|
||||
v1:e -> c4:p2:w [color="black", label=""];
|
||||
c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
module foobaraddsub(a, b, c, d, fa, fs, ba, bs);
|
||||
input [7:0] a, b, c, d;
|
||||
output [7:0] fa, fs, ba, bs;
|
||||
assign fa = a + (* foo *) b;
|
||||
assign fs = a - (* foo *) b;
|
||||
assign ba = c + (* bar *) d;
|
||||
assign bs = c - (* bar *) d;
|
||||
endmodule
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
#!/bin/bash
|
||||
set -ex
|
||||
if false; then
|
||||
rm -f *.dot
|
||||
../../yosys example.ys
|
||||
../../yosys -p 'proc; opt; show -format dot -prefix splice' splice.v
|
||||
../../yosys -p 'techmap; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -format dot -prefix cmos_00' cmos.v
|
||||
../../yosys -p 'techmap; splitnets -ports; abc -liberty ../../techlibs/cmos/cmos_cells.lib;; show -lib ../../techlibs/cmos/cmos_cells.v -format dot -prefix cmos_01' cmos.v
|
||||
../../yosys -p 'opt; cd sumprod; select a:sumstuff; show -format dot -prefix sumprod_00' sumprod.v
|
||||
../../yosys -p 'opt; cd sumprod; select a:sumstuff %x; show -format dot -prefix sumprod_01' sumprod.v
|
||||
../../yosys -p 'opt; cd sumprod; select prod; show -format dot -prefix sumprod_02' sumprod.v
|
||||
../../yosys -p 'opt; cd sumprod; select prod %ci; show -format dot -prefix sumprod_03' sumprod.v
|
||||
../../yosys -p 'opt; cd sumprod; select prod %ci2; show -format dot -prefix sumprod_04' sumprod.v
|
||||
../../yosys -p 'opt; cd sumprod; select prod %ci3; show -format dot -prefix sumprod_05' sumprod.v
|
||||
../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_00' memdemo.v
|
||||
../../yosys -p 'proc; opt; memory; opt; cd memdemo; show -format dot -prefix memdemo_01 y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff' memdemo.v
|
||||
../../yosys submod.ys
|
||||
sed -i '/^label=/ d;' *.dot
|
||||
fi
|
||||
for dot_file in *.dot; do
|
||||
pdf_file=${dot_file%.dot}.pdf
|
||||
dot -Tpdf -o $pdf_file $dot_file
|
||||
done
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
module memdemo(clk, d, y);
|
||||
|
||||
input clk;
|
||||
input [3:0] d;
|
||||
output reg [3:0] y;
|
||||
|
||||
integer i;
|
||||
reg [1:0] s1, s2;
|
||||
reg [3:0] mem [0:3];
|
||||
|
||||
always @(posedge clk) begin
|
||||
for (i = 0; i < 4; i = i+1)
|
||||
mem[i] <= mem[(i+1) % 4] + mem[(i+2) % 4];
|
||||
{ s2, s1 } = d ? { s1, s2 } ^ d : 4'b0;
|
||||
mem[s1] <= d;
|
||||
y <= mem[s2];
|
||||
end
|
||||
|
||||
endmodule
|
||||
|
|
@ -1,138 +0,0 @@
|
|||
digraph "memdemo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n24 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n25 [ shape=octagon, label="d", color="black", fontcolor="black" ];
|
||||
n26 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
|
||||
n27 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
|
||||
n28 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
|
||||
n29 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
|
||||
n30 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
|
||||
n31 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
|
||||
n32 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c36 [ shape=record, label="{{<p33> A|<p34> B}|$28\n$add|{<p35> Y}}" ];
|
||||
c37 [ shape=record, label="{{<p33> A|<p34> B}|$31\n$add|{<p35> Y}}" ];
|
||||
c38 [ shape=record, label="{{<p33> A|<p34> B}|$34\n$add|{<p35> Y}}" ];
|
||||
c39 [ shape=record, label="{{<p33> A|<p34> B}|$37\n$add|{<p35> Y}}" ];
|
||||
c41 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$110\n$mux|{<p35> Y}}" ];
|
||||
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
|
||||
x0:e -> c41:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c42 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$113\n$mux|{<p35> Y}}" ];
|
||||
x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
|
||||
x1:e -> c42:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c43 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$116\n$mux|{<p35> Y}}" ];
|
||||
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
|
||||
x2:e -> c43:p40:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
v3 [ label="1'1" ];
|
||||
c44 [ shape=record, label="{{<p33> A|<p34> B}|$145\n$and|{<p35> Y}}" ];
|
||||
v4 [ label="1'1" ];
|
||||
c45 [ shape=record, label="{{<p33> A|<p34> B}|$175\n$and|{<p35> Y}}" ];
|
||||
v5 [ label="1'1" ];
|
||||
c46 [ shape=record, label="{{<p33> A|<p34> B}|$205\n$and|{<p35> Y}}" ];
|
||||
v6 [ label="1'1" ];
|
||||
c47 [ shape=record, label="{{<p33> A|<p34> B}|$235\n$and|{<p35> Y}}" ];
|
||||
v7 [ label="2'00" ];
|
||||
c48 [ shape=record, label="{{<p33> A|<p34> B}|$143\n$eq|{<p35> Y}}" ];
|
||||
v8 [ label="2'01" ];
|
||||
c49 [ shape=record, label="{{<p33> A|<p34> B}|$173\n$eq|{<p35> Y}}" ];
|
||||
v9 [ label="2'10" ];
|
||||
c50 [ shape=record, label="{{<p33> A|<p34> B}|$203\n$eq|{<p35> Y}}" ];
|
||||
v10 [ label="2'11" ];
|
||||
c51 [ shape=record, label="{{<p33> A|<p34> B}|$233\n$eq|{<p35> Y}}" ];
|
||||
c52 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$147\n$mux|{<p35> Y}}" ];
|
||||
c53 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$177\n$mux|{<p35> Y}}" ];
|
||||
c54 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$207\n$mux|{<p35> Y}}" ];
|
||||
c55 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$237\n$mux|{<p35> Y}}" ];
|
||||
c59 [ shape=record, label="{{<p56> CLK|<p57> D}|$66\n$dff|{<p58> Q}}" ];
|
||||
c60 [ shape=record, label="{{<p56> CLK|<p57> D}|$68\n$dff|{<p58> Q}}" ];
|
||||
c61 [ shape=record, label="{{<p56> CLK|<p57> D}|$70\n$dff|{<p58> Q}}" ];
|
||||
c62 [ shape=record, label="{{<p56> CLK|<p57> D}|$72\n$dff|{<p58> Q}}" ];
|
||||
c63 [ shape=record, label="{{<p56> CLK|<p57> D}|$59\n$dff|{<p58> Q}}" ];
|
||||
c64 [ shape=record, label="{{<p56> CLK|<p57> D}|$63\n$dff|{<p58> Q}}" ];
|
||||
c65 [ shape=record, label="{{<p56> CLK|<p57> D}|$64\n$dff|{<p58> Q}}" ];
|
||||
c66 [ shape=record, label="{{<p33> A}|$39\n$reduce_bool|{<p35> Y}}" ];
|
||||
v11 [ label="4'0000" ];
|
||||
c67 [ shape=record, label="{{<p33> A|<p34> B|<p40> S}|$40\n$mux|{<p35> Y}}" ];
|
||||
x12 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
|
||||
c67:p35:e -> x12:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
c68 [ shape=record, label="{{<p33> A|<p34> B}|$38\n$xor|{<p35> Y}}" ];
|
||||
x13 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
|
||||
x13:e -> c68:p33:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
c36:p35:e -> c52:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c44:p35:e -> c52:p40:w [color="black", label=""];
|
||||
c45:p35:e -> c53:p40:w [color="black", label=""];
|
||||
c46:p35:e -> c54:p40:w [color="black", label=""];
|
||||
c47:p35:e -> c55:p40:w [color="black", label=""];
|
||||
c48:p35:e -> c44:p33:w [color="black", label=""];
|
||||
c49:p35:e -> c45:p33:w [color="black", label=""];
|
||||
c50:p35:e -> c46:p33:w [color="black", label=""];
|
||||
c51:p35:e -> c47:p33:w [color="black", label=""];
|
||||
c52:p35:e -> c59:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c53:p35:e -> c60:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c37:p35:e -> c53:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c54:p35:e -> c61:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c55:p35:e -> c62:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c66:p35:e -> c67:p40:w [color="black", label=""];
|
||||
c68:p35:e -> c67:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n24:e -> c59:p56:w [color="black", label=""];
|
||||
n24:e -> c60:p56:w [color="black", label=""];
|
||||
n24:e -> c61:p56:w [color="black", label=""];
|
||||
n24:e -> c62:p56:w [color="black", label=""];
|
||||
n24:e -> c63:p56:w [color="black", label=""];
|
||||
n24:e -> c64:p56:w [color="black", label=""];
|
||||
n24:e -> c65:p56:w [color="black", label=""];
|
||||
n25:e -> c52:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n25:e -> c53:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n25:e -> c54:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n25:e -> c55:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n25:e -> c66:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n25:e -> c68:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c59:p58:e -> n26:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n26:e -> c38:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n26:e -> c39:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n26:e -> c42:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c60:p58:e -> n27:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n27:e -> c36:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n27:e -> c39:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n27:e -> c42:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c61:p58:e -> n28:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n28:e -> c36:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n28:e -> c37:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n28:e -> c43:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c62:p58:e -> n29:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n29:e -> c37:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n29:e -> c38:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n29:e -> c43:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c38:p35:e -> c54:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c63:p58:e -> n30:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n30:e -> x13:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c64:p58:e -> n31:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n31:e -> x13:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c65:p58:e -> n32:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c39:p35:e -> c55:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5 [ shape=point ];
|
||||
x12:s0:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c48:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c49:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c50:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c51:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c63:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6 [ shape=point ];
|
||||
x12:s1:e -> n6:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> c64:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> x1:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c41:p35:e -> c65:p57:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c42:p35:e -> c41:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c43:p35:e -> c41:p34:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v10:e -> c51:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v11:e -> c67:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v3:e -> c44:p34:w [color="black", label=""];
|
||||
v4:e -> c45:p34:w [color="black", label=""];
|
||||
v5:e -> c46:p34:w [color="black", label=""];
|
||||
v6:e -> c47:p34:w [color="black", label=""];
|
||||
v7:e -> c48:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v8:e -> c49:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v9:e -> c50:p33:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,29 +0,0 @@
|
|||
digraph "memdemo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n4 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
|
||||
n5 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
|
||||
n6 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
|
||||
n7 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
|
||||
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
v0 [ label="$0\\s2[1:0] [1]" ];
|
||||
c13 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$110\n$mux|{<p12> Y}}" ];
|
||||
v1 [ label="$0\\s2[1:0] [0]" ];
|
||||
c14 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$113\n$mux|{<p12> Y}}" ];
|
||||
v2 [ label="$0\\s2[1:0] [0]" ];
|
||||
c15 [ shape=record, label="{{<p9> A|<p10> B|<p11> S}|$116\n$mux|{<p12> Y}}" ];
|
||||
v3 [ label="clk" ];
|
||||
c19 [ shape=record, label="{{<p16> CLK|<p17> D}|$64\n$dff|{<p18> Q}}" ];
|
||||
c13:p12:e -> c19:p17:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c14:p12:e -> c13:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c15:p12:e -> c13:p10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n4:e -> c14:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c14:p10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> c15:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n7:e -> c15:p10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c19:p18:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v0:e -> c13:p11:w [color="black", label=""];
|
||||
v1:e -> c14:p11:w [color="black", label=""];
|
||||
v2:e -> c15:p11:w [color="black", label=""];
|
||||
v3:e -> c19:p16:w [color="black", label=""];
|
||||
}
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
module primetest(p, a, b, ok);
|
||||
input [15:0] p, a, b;
|
||||
output ok = p != a*b || a == 1 || b == 1;
|
||||
endmodule
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
digraph "splice_demo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n1 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n2 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n3 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n4 [ shape=octagon, label="d", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="e", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="f", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="x", color="black", fontcolor="black" ];
|
||||
n8 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c11 [ shape=record, label="{{<p9> A}|$2\n$neg|{<p10> Y}}" ];
|
||||
x0 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
|
||||
x0:e -> c11:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
x1 [ shape=record, style=rounded, label="<s0> 3:0 - 7:4 " ];
|
||||
c11:p10:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
c12 [ shape=record, label="{{<p9> A}|$1\n$not|{<p10> Y}}" ];
|
||||
x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
|
||||
x2:e -> c12:p9:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
x3 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 3:2 " ];
|
||||
c12:p10:e -> x3:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
x4 [ shape=record, style=rounded, label="<s1> 0:0 - 1:1 |<s0> 1:1 - 0:0 " ];
|
||||
x5 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
|
||||
x6 [ shape=record, style=rounded, label="<s0> 3:0 - 11:8 " ];
|
||||
x5:e -> x6:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
n1:e -> x4:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n1:e -> x4:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n1:e -> x5:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> x5:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> x0:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n4:e -> x0:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x4:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x1:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x3:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x3:s1:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x6:s0:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
module splice_demo(a, b, c, d, e, f, x, y);
|
||||
|
||||
input [1:0] a, b, c, d, e, f;
|
||||
output [1:0] x = {a[0], a[1]};
|
||||
|
||||
output [11:0] y;
|
||||
assign {y[11:4], y[1:0], y[3:2]} =
|
||||
{a, b, -{c, d}, ~{e, f}};
|
||||
|
||||
endmodule
|
||||
|
|
@ -1,16 +0,0 @@
|
|||
read_verilog memdemo.v
|
||||
proc; opt; memory; opt
|
||||
|
||||
cd memdemo
|
||||
select -set outstage y %ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff
|
||||
select -set selstage y %ci2:+$dff[Q,D] %ci*:-$dff @outstage %d
|
||||
select -set scramble mem* %ci2 %ci*:-$dff mem* %d @selstage %d
|
||||
submod -name scramble @scramble
|
||||
submod -name outstage @outstage
|
||||
submod -name selstage @selstage
|
||||
|
||||
cd ..
|
||||
show -format dot -prefix submod_00 memdemo
|
||||
show -format dot -prefix submod_01 scramble
|
||||
show -format dot -prefix submod_02 outstage
|
||||
show -format dot -prefix submod_03 selstage
|
||||
|
|
@ -1,45 +0,0 @@
|
|||
digraph "memdemo" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n5 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="d", color="black", fontcolor="black" ];
|
||||
n7 [ shape=diamond, label="mem[0]", color="black", fontcolor="black" ];
|
||||
n8 [ shape=diamond, label="mem[1]", color="black", fontcolor="black" ];
|
||||
n9 [ shape=diamond, label="mem[2]", color="black", fontcolor="black" ];
|
||||
n10 [ shape=diamond, label="mem[3]", color="black", fontcolor="black" ];
|
||||
n11 [ shape=diamond, label="s1", color="black", fontcolor="black" ];
|
||||
n12 [ shape=diamond, label="s2", color="black", fontcolor="black" ];
|
||||
n13 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c17 [ shape=record, label="{{<p14> CLK|<p15> D}|$59\n$dff|{<p16> Q}}" ];
|
||||
c18 [ shape=record, label="{{<p14> CLK|<p15> D}|$63\n$dff|{<p16> Q}}" ];
|
||||
c20 [ shape=record, label="{{<p5> clk|<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]|<p19> n1}|outstage\noutstage|{<p13> y}}" ];
|
||||
c21 [ shape=record, label="{{<p5> clk|<p6> d|<p19> n1}|scramble\nscramble|{<p7> mem[0]|<p8> mem[1]|<p9> mem[2]|<p10> mem[3]}}" ];
|
||||
c23 [ shape=record, label="{{<p6> d|<p11> s1|<p12> s2}|selstage\nselstage|{<p19> n1|<p22> n2}}" ];
|
||||
n1 [ shape=point ];
|
||||
c23:p19:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n1:e -> c17:p15:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n1:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c21:p10:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n10:e -> c20:p10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c17:p16:e -> n11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n11:e -> c23:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c18:p16:e -> n12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n12:e -> c23:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c20:p13:e -> n13:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2 [ shape=point ];
|
||||
c23:p22:e -> n2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> c18:p15:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> c20:p19:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n5:e -> c17:p14:w [color="black", label=""];
|
||||
n5:e -> c18:p14:w [color="black", label=""];
|
||||
n5:e -> c20:p5:w [color="black", label=""];
|
||||
n5:e -> c21:p5:w [color="black", label=""];
|
||||
n6:e -> c21:p6:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> c23:p6:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c21:p7:e -> n7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n7:e -> c20:p7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c21:p8:e -> n8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n8:e -> c20:p8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c21:p9:e -> n9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n9:e -> c20:p9:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,87 +0,0 @@
|
|||
digraph "scramble" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n17 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n18 [ shape=octagon, label="d", color="black", fontcolor="black" ];
|
||||
n19 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
|
||||
n20 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
|
||||
n21 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
|
||||
n22 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
|
||||
n23 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
|
||||
c27 [ shape=record, label="{{<p24> A|<p25> B}|$28\n$add|{<p26> Y}}" ];
|
||||
c28 [ shape=record, label="{{<p24> A|<p25> B}|$31\n$add|{<p26> Y}}" ];
|
||||
c29 [ shape=record, label="{{<p24> A|<p25> B}|$34\n$add|{<p26> Y}}" ];
|
||||
c30 [ shape=record, label="{{<p24> A|<p25> B}|$37\n$add|{<p26> Y}}" ];
|
||||
v0 [ label="1'1" ];
|
||||
c31 [ shape=record, label="{{<p24> A|<p25> B}|$145\n$and|{<p26> Y}}" ];
|
||||
v1 [ label="1'1" ];
|
||||
c32 [ shape=record, label="{{<p24> A|<p25> B}|$175\n$and|{<p26> Y}}" ];
|
||||
v2 [ label="1'1" ];
|
||||
c33 [ shape=record, label="{{<p24> A|<p25> B}|$205\n$and|{<p26> Y}}" ];
|
||||
v3 [ label="1'1" ];
|
||||
c34 [ shape=record, label="{{<p24> A|<p25> B}|$235\n$and|{<p26> Y}}" ];
|
||||
v4 [ label="2'00" ];
|
||||
c35 [ shape=record, label="{{<p24> A|<p25> B}|$143\n$eq|{<p26> Y}}" ];
|
||||
v5 [ label="2'01" ];
|
||||
c36 [ shape=record, label="{{<p24> A|<p25> B}|$173\n$eq|{<p26> Y}}" ];
|
||||
v6 [ label="2'10" ];
|
||||
c37 [ shape=record, label="{{<p24> A|<p25> B}|$203\n$eq|{<p26> Y}}" ];
|
||||
v7 [ label="2'11" ];
|
||||
c38 [ shape=record, label="{{<p24> A|<p25> B}|$233\n$eq|{<p26> Y}}" ];
|
||||
c40 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$147\n$mux|{<p26> Y}}" ];
|
||||
c41 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$177\n$mux|{<p26> Y}}" ];
|
||||
c42 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$207\n$mux|{<p26> Y}}" ];
|
||||
c43 [ shape=record, label="{{<p24> A|<p25> B|<p39> S}|$237\n$mux|{<p26> Y}}" ];
|
||||
c47 [ shape=record, label="{{<p44> CLK|<p45> D}|$66\n$dff|{<p46> Q}}" ];
|
||||
c48 [ shape=record, label="{{<p44> CLK|<p45> D}|$68\n$dff|{<p46> Q}}" ];
|
||||
c49 [ shape=record, label="{{<p44> CLK|<p45> D}|$70\n$dff|{<p46> Q}}" ];
|
||||
c50 [ shape=record, label="{{<p44> CLK|<p45> D}|$72\n$dff|{<p46> Q}}" ];
|
||||
c27:p26:e -> c40:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c36:p26:e -> c32:p24:w [color="black", label=""];
|
||||
c37:p26:e -> c33:p24:w [color="black", label=""];
|
||||
c38:p26:e -> c34:p24:w [color="black", label=""];
|
||||
c40:p26:e -> c47:p45:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c41:p26:e -> c48:p45:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c42:p26:e -> c49:p45:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c43:p26:e -> c50:p45:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n17:e -> c47:p44:w [color="black", label=""];
|
||||
n17:e -> c48:p44:w [color="black", label=""];
|
||||
n17:e -> c49:p44:w [color="black", label=""];
|
||||
n17:e -> c50:p44:w [color="black", label=""];
|
||||
n18:e -> c40:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n18:e -> c41:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n18:e -> c42:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n18:e -> c43:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c47:p46:e -> n19:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n19:e -> c29:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n19:e -> c30:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c28:p26:e -> c41:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c48:p46:e -> n20:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n20:e -> c27:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n20:e -> c30:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c49:p46:e -> n21:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n21:e -> c27:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n21:e -> c28:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c50:p46:e -> n22:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n22:e -> c28:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n22:e -> c29:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n23:e -> c35:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n23:e -> c36:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n23:e -> c37:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n23:e -> c38:p25:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c29:p26:e -> c42:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c30:p26:e -> c43:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c31:p26:e -> c40:p39:w [color="black", label=""];
|
||||
c32:p26:e -> c41:p39:w [color="black", label=""];
|
||||
c33:p26:e -> c42:p39:w [color="black", label=""];
|
||||
c34:p26:e -> c43:p39:w [color="black", label=""];
|
||||
c35:p26:e -> c31:p24:w [color="black", label=""];
|
||||
v0:e -> c31:p25:w [color="black", label=""];
|
||||
v1:e -> c32:p25:w [color="black", label=""];
|
||||
v2:e -> c33:p25:w [color="black", label=""];
|
||||
v3:e -> c34:p25:w [color="black", label=""];
|
||||
v4:e -> c35:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v5:e -> c36:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v6:e -> c37:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v7:e -> c38:p24:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
digraph "outstage" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n4 [ shape=octagon, label="clk", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="mem[0]", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="mem[1]", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="mem[2]", color="black", fontcolor="black" ];
|
||||
n8 [ shape=octagon, label="mem[3]", color="black", fontcolor="black" ];
|
||||
n9 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
|
||||
n10 [ shape=octagon, label="y", color="black", fontcolor="black" ];
|
||||
c15 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$110\n$mux|{<p14> Y}}" ];
|
||||
x0 [ shape=record, style=rounded, label="<s0> 1:1 - 0:0 " ];
|
||||
x0:e -> c15:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c16 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$113\n$mux|{<p14> Y}}" ];
|
||||
x1 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
|
||||
x1:e -> c16:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c17 [ shape=record, label="{{<p11> A|<p12> B|<p13> S}|$116\n$mux|{<p14> Y}}" ];
|
||||
x2 [ shape=record, style=rounded, label="<s0> 0:0 - 0:0 " ];
|
||||
x2:e -> c17:p13:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", label=""];
|
||||
c21 [ shape=record, label="{{<p18> CLK|<p19> D}|$64\n$dff|{<p20> Q}}" ];
|
||||
c15:p14:e -> c21:p19:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c21:p20:e -> n10:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c16:p14:e -> c15:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c17:p14:e -> c15:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n4:e -> c21:p18:w [color="black", label=""];
|
||||
n5:e -> c16:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> c16:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n7:e -> c17:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n8:e -> c17:p12:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n9:e -> x0:s0:w [color="black", label=""];
|
||||
n9:e -> x1:s0:w [color="black", label=""];
|
||||
n9:e -> x2:s0:w [color="black", label=""];
|
||||
}
|
||||
|
|
@ -1,26 +0,0 @@
|
|||
digraph "selstage" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n3 [ shape=octagon, label="d", color="black", fontcolor="black" ];
|
||||
n4 [ shape=octagon, label="n1", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="n2", color="black", fontcolor="black" ];
|
||||
n6 [ shape=octagon, label="s1", color="black", fontcolor="black" ];
|
||||
n7 [ shape=octagon, label="s2", color="black", fontcolor="black" ];
|
||||
c10 [ shape=record, label="{{<p8> A}|$39\n$reduce_bool|{<p9> Y}}" ];
|
||||
v0 [ label="4'0000" ];
|
||||
c13 [ shape=record, label="{{<p8> A|<p11> B|<p12> S}|$40\n$mux|{<p9> Y}}" ];
|
||||
x1 [ shape=record, style=rounded, label="<s1> 3:2 - 1:0 |<s0> 1:0 - 1:0 " ];
|
||||
c13:p9:e -> x1:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
c14 [ shape=record, label="{{<p8> A|<p11> B}|$38\n$xor|{<p9> Y}}" ];
|
||||
x2 [ shape=record, style=rounded, label="<s1> 1:0 - 3:2 |<s0> 1:0 - 1:0 " ];
|
||||
x2:e -> c14:p8:w [arrowhead=odiamond, arrowtail=odiamond, dir=both, color="black", style="setlinewidth(3)", label=""];
|
||||
c10:p9:e -> c13:p12:w [color="black", label=""];
|
||||
c14:p9:e -> c13:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> c10:p8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> c14:p11:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x1:s0:e -> n4:w [color="black", style="setlinewidth(3)", label=""];
|
||||
x1:s1:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n6:e -> x2:s1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n7:e -> x2:s0:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v0:e -> c13:p8:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
module sumprod(a, b, c, sum, prod);
|
||||
|
||||
input [7:0] a, b, c;
|
||||
output [7:0] sum, prod;
|
||||
|
||||
{* sumstuff *}
|
||||
assign sum = a + b + c;
|
||||
{* *}
|
||||
|
||||
assign prod = a * b * c;
|
||||
|
||||
endmodule
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
v0 [ label="a" ];
|
||||
v1 [ label="b" ];
|
||||
v2 [ label="$1_Y" ];
|
||||
c4 [ shape=record, label="{{<p1> A|<p2> B}|$1\n$add|{<p3> Y}}" ];
|
||||
v3 [ label="$1_Y" ];
|
||||
v4 [ label="c" ];
|
||||
v5 [ label="sum" ];
|
||||
c5 [ shape=record, label="{{<p1> A|<p2> B}|$2\n$add|{<p3> Y}}" ];
|
||||
v0:e -> c4:p1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v1:e -> c4:p2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c4:p3:e -> v2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v3:e -> c5:p1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v4:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c5:p3:e -> v5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n2 [ shape=octagon, label="a", color="black", fontcolor="black" ];
|
||||
n3 [ shape=octagon, label="b", color="black", fontcolor="black" ];
|
||||
n4 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n5 [ shape=octagon, label="sum", color="black", fontcolor="black" ];
|
||||
c9 [ shape=record, label="{{<p6> A|<p7> B}|$1\n$add|{<p8> Y}}" ];
|
||||
c10 [ shape=record, label="{{<p6> A|<p7> B}|$2\n$add|{<p8> Y}}" ];
|
||||
c9:p8:e -> c10:p6:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> c9:p6:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n3:e -> c9:p7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n4:e -> c10:p7:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c10:p8:e -> n5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
|
||||
}
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n1 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
|
||||
v0 [ label="$3_Y" ];
|
||||
v1 [ label="c" ];
|
||||
c5 [ shape=record, label="{{<p2> A|<p3> B}|$4\n$mul|{<p4> Y}}" ];
|
||||
c5:p4:e -> n1:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v0:e -> c5:p2:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v1:e -> c5:p3:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,11 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
|
||||
c7 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
|
||||
n1 [ shape=diamond, label="$3_Y" ];
|
||||
n1:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c7:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,15 +0,0 @@
|
|||
digraph "sumprod" {
|
||||
rankdir="LR";
|
||||
remincross=true;
|
||||
n2 [ shape=octagon, label="c", color="black", fontcolor="black" ];
|
||||
n3 [ shape=octagon, label="prod", color="black", fontcolor="black" ];
|
||||
v0 [ label="a" ];
|
||||
v1 [ label="b" ];
|
||||
c7 [ shape=record, label="{{<p4> A|<p5> B}|$3\n$mul|{<p6> Y}}" ];
|
||||
c8 [ shape=record, label="{{<p4> A|<p5> B}|$4\n$mul|{<p6> Y}}" ];
|
||||
c7:p6:e -> c8:p4:w [color="black", style="setlinewidth(3)", label=""];
|
||||
n2:e -> c8:p5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
c8:p6:e -> n3:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v0:e -> c7:p4:w [color="black", style="setlinewidth(3)", label=""];
|
||||
v1:e -> c7:p5:w [color="black", style="setlinewidth(3)", label=""];
|
||||
}
|
||||
|
|
@ -1,435 +0,0 @@
|
|||
|
||||
% 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 Claire Xenia Wolf \\ April 2015}
|
||||
\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 a simple format and easy to parse. It allows to model
|
||||
the model checking problem over the 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 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
|
||||
uninitialized, 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_expr -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_expr -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}
|
||||
Claire Xenia Wolf. The Yosys Open SYnthesis Suite. \\
|
||||
\url{https://yosyshq.net/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}
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -ex
|
||||
for job in APPNOTE_010_Verilog_to_BLIF APPNOTE_011_Design_Investigation APPNOTE_012_Verilog_to_BTOR
|
||||
do
|
||||
[ -f $job.ok -a $job.ok -nt $job.tex ] && continue
|
||||
if [ -f $job/make.sh ]; then
|
||||
cd $job
|
||||
bash make.sh
|
||||
cd ..
|
||||
fi
|
||||
old_md5=$([ -f $job.aux ] && md5sum < $job.aux || true)
|
||||
while
|
||||
pdflatex -shell-escape -halt-on-error $job.tex || exit
|
||||
new_md5=$(md5sum < $job.aux)
|
||||
[ "$old_md5" != "$new_md5" ]
|
||||
do
|
||||
old_md5="$new_md5"
|
||||
done
|
||||
touch $job.ok
|
||||
done
|
||||
|
||||
Loading…
Reference in New Issue