path: root/manual
diff options
authorClifford Wolf <>2013-11-23 17:33:26 +0100
committerClifford Wolf <>2013-11-23 18:52:41 +0100
commite216e0e2917afb6516c0499f8880d68cf71b7c40 (patch)
tree14849196b7f189a7320005a477e11d5755f5a785 /manual
parent5f9c7fc6eadd7bc70e13df4131c059ec9ae18103 (diff)
AppNote 010 progress
Diffstat (limited to 'manual')
4 files changed, 230 insertions, 75 deletions
diff --git a/manual/.gitignore b/manual/.gitignore
index 15063c48..7412c4d4 100644
--- a/manual/.gitignore
+++ b/manual/.gitignore
@@ -6,3 +6,4 @@
diff --git a/manual/APPNOTE_010_Verilog_to_BLIF.tex b/manual/APPNOTE_010_Verilog_to_BLIF.tex
index 514f50e2..aee21aff 100644
--- a/manual/APPNOTE_010_Verilog_to_BLIF.tex
+++ b/manual/APPNOTE_010_Verilog_to_BLIF.tex
@@ -1,7 +1,61 @@
-\appnote{010}{Converting Verilog to BLIF}{Clifford Wolf}
+% IEEEtran howto:
+\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
+% - 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").
+\title{Yosys Application Note 010: \\ Converting Verilog to BLIF}
+\author{Clifford Wolf}
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 prefered
method of design entry for many designers\footnote{The other half prefers VHDL,
@@ -12,11 +66,16 @@ exchanging sequential logic between programs. It is easy to generate and
easy to parse and is therefore the prefered method of design entry for
many authors of logic synthesis tools.
-Yosys\footnote{\url{}} 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.
+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.
@@ -35,14 +94,13 @@ and {\tt MiniSAT} support and not build {\tt yosys-abc}.
This Application Note is based on GIT Rev. {\color{red} FIXME} from
{\color{red} DATE} of Yosys. The Verilog sources used for the examples
-is taken from the {\it yosys-bigsim test
-bench}\footnote{\url{}}, GIT
-Rev. {\color{red} FIXME}.
+is taken from yosys-bigsim \cite{bigsim},
+a collection of real-world designs used for regression testing Yosys.
\section{Getting Started}
-We start with the {\tt softusb\_navre} core from {\it yosys-bigsim}. The navre
-processor\footnote{\url{,navre}} is an Open Source
+We start with the {\tt softusb\_navre} core from yosys-bigsim. The Navré
+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.
@@ -51,7 +109,7 @@ Converting {\tt softusb\_navre.v} to {\tt softusb\_navre.blif} could not be
yosys -o softusb_navre.blif \
-S softusb_navre.v
@@ -81,7 +139,7 @@ With a script file we have better control over Yosys. The following script
file replicates what the command from the last section did:
read_verilog softusb_navre.v
proc; opt; memory; opt; techmap; opt
@@ -133,7 +191,7 @@ source file, as we will see in the next section.
Now Yosys can be run with the file of the synthesis script as argument:
yosys softusb_navre.ys
@@ -168,7 +226,7 @@ So now we have the final synthesis script for generating a BLIF file
for the navre CPU:
read_verilog softusb_navre.v
hierarchy -check -top softusb_navre
proc; opt; memory; opt;
@@ -181,12 +239,12 @@ write_blif softusb_navre.blif
\section{Advanced Example: The Amber23 ARMv2a CPU}
-Our 2nd example is the Amber23\footnote{\url{,amber}}
+Our 2nd example is the Amber23 \cite{amber}
ARMv2a CPU. Once again we base our example on the Verilog code that is included
-in {\it yosys-bigsim}.
+in yosys-bigsim \cite{bigsim}.
read_verilog a23_alu.v
read_verilog a23_barrel_shift_fpga.v
read_verilog a23_barrel_shift.v
@@ -221,6 +279,10 @@ implementation. This design can not be expressed in BLIF as it is. Instead we
need to use a synthesis script that transforms this to synchonous resets that
can be expressed in BLIF.
+(Note that this is not a problem if this coding techiques are used to model
+ROM, where the register is initialized using this syntax but is never updated
Listing~\ref{aber23.ys} shows the synthesis script for the Amber23 core. In
@@ -231,7 +293,7 @@ altered so that this new signal is connected throughout the whole design
reg [7:0] a = 13, b;
initial b = 37;
@@ -241,41 +303,155 @@ initial b = 37;
-module \$adff (CLK, ARST, D, Q);
+(* techmap_celltype = "$adff" *)
+module adff2dff (CLK, ARST, D, Q);
parameter WIDTH = 1;
-parameter CLK_POLARITY = 1'b1;
-parameter ARST_POLARITY = 1'b1;
+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";
always @(posedge CLK)
- if (ARST)
- else
- Q <= D;
+ if (ARST)
+ else
+ Q <= D;
- \renewcommand{\figurename}{Listing}
\caption{\tt adff2dff.v}
-In line 18 the {\tt proc} command is called. But this time the newly created
-reset signal is passed to the core as a global reset line to use for resetting
-all registers to their initial values.
+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 line to be used for
+resetting all registers to their initial values.
Finally in line 19 the {\tt techmap} command is used to replace all instances
-of flip-flops with asynchronous resets to flip-flops with synchronous resets.
-The map file used fo this is shown in Lising~\ref{adff2dff.v}.
+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
+(which evaluates to a constant value) determines if the parameter set is
+compatible with this replacement circuit in lines 15 and 16, and how the {\tt
+\_TECHMAP\_DO\_} wire in line 13 provides a mini synthesis-script to be used to
+process this cell.
+#include <stdint.h>
+#include <stdbool.h>
+#define BITMAP_SIZE 64
+#define OUTPORT 0x10000000
+static uint16_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;
+\caption{Test program for Amber23 CPU (Sieve of Eratosthenes)}
+\section{Validation 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 validated using the test-bench from yosys-bigsim
+and successfully executed the program shown in Listing~\ref{sieve}. The
+test program was compiled using GCC 4.6.3.
+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 the ABC internal format as well.
+The only interesting thing to write about the simulation itself is that this is
+probably one of the most wasteful and time consuming ways of successfully
+calculating the first 50 primes the author has ever conducted.
+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
+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.
+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.
+Clifford Wolf. The Yosys Open SYnthesis Suite. \\
+yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\
+Sebastien Bourdeauducq. Navré AVR clone (8-bit RISC). \\
+Conor Santifort. Amber ARM-compatible core. \\
+Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. \\
-{\color{red} FIXME}
diff --git a/manual/appnote.tex b/manual/appnote.tex
deleted file mode 100644
index 4c543d6a..00000000
--- a/manual/appnote.tex
+++ /dev/null
@@ -1,39 +0,0 @@
-% IEEEtran howto:
-\def\appnote#1#2#3{\title{Yosy Application Note #1: \\ #2} \author{#3} \maketitle}
diff --git a/manual/ b/manual/
new file mode 100644
index 00000000..00f87576
--- /dev/null
+++ b/manual/
@@ -0,0 +1,17 @@
+set -ex
+for job in APPNOTE_010_Verilog_to_BLIF
+ [ -f $job.ok -a $job.ok -nt $job.tex ] && continue
+ old_md5=$([ -f $job.aux ] && md5sum < $job.aux)
+ while
+ pdflatex -shell-escape -halt-on-error $job.tex
+ new_md5=$(md5sum < $job.aux)
+ [ "$old_md5" != "$new_md5" ]
+ do
+ old_md5="$new_md5"
+ done
+ touch $job.ok