manual/APPNOTE_010_Verilog_to_BLIF.tex

   1
   2 % IEEEtran howto:
   3 % http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf
   4 \documentclass[9pt,technote,a4paper]{IEEEtran}
   5
   6 \usepackage[T1]{fontenc}   % required for luximono!
   7 \usepackage[scaled=0.8]{luximono}  % typewriter font with bold face
   8
   9 % To install the luximono font files:
  10 % getnonfreefonts-sys --all        or
  11 % getnonfreefonts-sys luximono
  12 %
  13 % when there are trouble you might need to:
  14 % - Create /etc/texmf/updmap.d/99local-luximono.cfg
  15 %   containing the single line: Map ul9.map
  16 % - Run update-updmap followed by mktexlsr and updmap-sys
  17 %
  18 % This commands must be executed as root with a root environment
  19 % (i.e. run "sudo su" and then execute the commands in the root
  20 % shell, don't just prefix the commands with "sudo").
  21
  22 \usepackage[unicode,bookmarks=false]{hyperref}
  23 \usepackage[english]{babel}
  24 \usepackage[utf8]{inputenc}
  25 \usepackage{amssymb}
  26 \usepackage{amsmath}
  27 \usepackage{amsfonts}
  28 \usepackage{units}
  29 \usepackage{nicefrac}
  30 \usepackage{eurosym}
  31 \usepackage{graphicx}
  32 \usepackage{verbatim}
  33 \usepackage{algpseudocode}
  34 \usepackage{scalefnt}
  35 \usepackage{xspace}
  36 \usepackage{color}
  37 \usepackage{colortbl}
  38 \usepackage{multirow}
  39 \usepackage{hhline}
  40 \usepackage{listings}
  41 \usepackage{float}
  42
  43 \usepackage{tikz}
  44 \usetikzlibrary{calc}
  45 \usetikzlibrary{arrows}
  46 \usetikzlibrary{scopes}
  47 \usetikzlibrary{through}
  48 \usetikzlibrary{shapes.geometric}
  49
  50 \lstset{basicstyle=\ttfamily,frame=trBL,xleftmargin=2em,xrightmargin=1em,numbers=left}
  51
  52 \begin{document}
  53
  54 \title{Yosys Application Note 010: \\ Converting Verilog to BLIF}
  55 \author{Clifford Wolf \\ November 2013}
  56 \maketitle
  57
  58 \begin{abstract}
  59 Verilog-2005 is a powerful Hardware Description Language (HDL) that can be used
  60 to easily create complex designs from small HDL code. It is the preferred
  61 method of design entry for many designers\footnote{The other half prefers VHDL,
  62 a very different but -- of course -- equally powerful language.}.
  63
  64 The Berkeley Logic Interchange Format (BLIF) \cite{blif} is a simple file format for
  65 exchanging sequential logic between programs. It is easy to generate and
  66 easy to parse and is therefore the preferred method of design entry for
  67 many authors of logic synthesis tools.
  68
  69 Yosys \cite{yosys} is a feature-rich
  70 Open-Source Verilog synthesis tool that can be used to bridge the gap between
  71 the two file formats. It implements most of Verilog-2005 and thus can be used
  72 to import modern behavioral Verilog designs into BLIF-based design flows
  73 without dependencies on proprietary synthesis tools.
  74
  75 The scope of Yosys goes of course far beyond Verilog logic synthesis. But
  76 it is a useful and important feature and this Application Note will focus
  77 on this aspect of Yosys.
  78 \end{abstract}
  79
  80 \section{Installation}
  81
  82 Yosys written in C++ (using features from C++11) and is tested on modern Linux.
  83 It should compile fine on most UNIX systems with a C++11 compiler. The README
  84 file contains useful information on building Yosys and its prerequisites.
  85
  86 Yosys is a large and feature-rich program with a couple of dependencies. It is,
  87 however, possible to deactivate some of the dependencies in the Makefile,
  88 resulting in features in Yosys becoming unavailable. When problems with building
  89 Yosys are encountered, a user who is only interested in the features of Yosys
  90 that are discussed in this Application Note may deactivate {\tt TCL}, {\tt Qt}
  91 and {\tt MiniSAT} support in the {\tt Makefile} and may opt against building
  92 {\tt yosys-abc}.
  93
  94 \bigskip
  95
  96 This Application Note is based on GIT Rev. {\tt e216e0e} from 2013-11-23 of
  97 Yosys \cite{yosys}. The Verilog sources used for the examples are taken from
  98 yosys-bigsim \cite{bigsim}, a collection of real-world designs used for
  99 regression testing Yosys.
 100
 101 \section{Getting Started}
 102
 103 We start our tour with the Navr\'e processor from yosys-bigsim. The Navr\'e
 104 processor \cite{navre} is an Open Source AVR clone. It is a single module ({\tt
 105 softusb\_navre}) in a single design file ({\tt softusb\_navre.v}). It also is
 106 using only features that map nicely to the BLIF format, for example it only
 107 uses synchronous resets.
 108
 109 Converting {\tt softusb\_navre.v} to {\tt softusb\_navre.blif} could not be
 110 easier:
 111
 112 \begin{figure}[H]
 113 \begin{lstlisting}[language=sh]
 114 yosys -o softusb_navre.blif -S softusb_navre.v
 115 \end{lstlisting}
 116  \renewcommand{\figurename}{Listing}
 117 \caption{Calling Yosys without script file}
 118 \end{figure}
 119
 120 Behind the scenes Yosys is controlled by synthesis scripts that execute
 121 commands that operate on Yosys' internal state. For example, the {\tt -o
 122 softusb\_navre.blif} option just adds the command {\tt write\_blif
 123 softusb\_navre.blif} to the end of the script. Likewise a file on the
 124 command line -- {\tt softusb\_navre.v} in this case -- adds the command
 125 {\tt read\_verilog softusb\_navre.v} to the beginning of the
 126 synthesis script. In both cases the file type is detected from the
 127 file extension.
 128
 129 Finally the option {\tt -S} instantiates a built-in default synthesis script.
 130 Instead of using {\tt -S} one could also specify the synthesis commands
 131 for the script on the command line using the {\tt -p} option, either using
 132 individual options for each command or by passing one big command string
 133 with a semicolon-separated list of commands. But in most cases it is more
 134 convenient to use an actual script file.
 135
 136 \section{Using a Synthesis Script}
 137
 138 With a script file we have better control over Yosys. The following script
 139 file replicates what the command from the last section did:
 140
 141 \begin{figure}[H]
 142 \begin{lstlisting}[language=sh]
 143 read_verilog softusb_navre.v
 144 hierarchy
 145 proc; opt; memory; opt; techmap; opt
 146 write_blif softusb_navre.blif
 147 \end{lstlisting}
 148  \renewcommand{\figurename}{Listing}
 149 \caption{\tt softusb\_navre.ys}
 150 \end{figure}
 151
 152 The first and last line obviously read the Verilog file and write the BLIF
 153 file.
 154
 155 \medskip
 156
 157 The 2nd line checks the design hierarchy and instantiates parametrized
 158 versions of the modules in the design, if necessary. In the case of this
 159 simple design this is a no-op. However, as a general rule a synthesis script
 160 should always contain this command as first command after reading the input
 161 files.
 162
 163 \medskip
 164
 165 The 3rd line does most of the actual work:
 166
 167 \begin{itemize}
 168 \item The command {\tt opt} is the Yosys' built-in optimizer. It can perform
 169 some simple optimizations such as const-folding and removing unconnected parts
 170 of the design. It is common practice to call opt after each major step in the
 171 synthesis procedure. In cases where too much optimization is not appreciated
 172 (for example when analyzing a design), it is recommended to call {\tt clean}
 173 instead of {\tt opt}.
 174 \item The command {\tt proc} converts {\it processes} (Yosys' internal
 175 representation of Verilog {\tt always}- and {\tt initial}-blocks) to circuits
 176 of multiplexers and storage elements (various types of flip-flops).
 177 \item The command {\tt memory} converts Yosys' internal representations of
 178 arrays and array accesses to multi-port block memories, and then maps this
 179 block memories to address decoders and flip-flops, unless the option {\tt -nomap}
 180 is used, in which case the multi-port block memories stay in the design
 181 and can then be mapped to architecture-specific memory primitives using
 182 other commands.
 183 \item The command {\tt techmap} turns a high-level circuit with coarse grain
 184 cells such as wide adders and multipliers to a fine-grain circuit of simple
 185 logic primitives and single-bit storage elements. The command does that by
 186 substituting the complex cells by circuits of simpler cells. It is possible
 187 to provide a custom set of rules for this process in the form of a Verilog
 188 source file, as we will see in the next section.
 189 \end{itemize}
 190
 191 Now Yosys can be run with the filename of the synthesis script as argument:
 192
 193 \begin{figure}[H]
 194 \begin{lstlisting}[language=sh]
 195 yosys softusb_navre.ys
 196 \end{lstlisting}
 197  \renewcommand{\figurename}{Listing}
 198 \caption{Calling Yosys with script file}
 199 \end{figure}
 200
 201 \medskip
 202
 203 Now that we are using a synthesis script we can easily modify how Yosys
 204 synthesizes the design. The first thing we should customize is the
 205 call to the {\tt hierarchy} command:
 206
 207 Whenever it is known that there are no implicit blackboxes in the design, i.e.
 208 modules that are referenced but are not defined, the {\tt hierarchy} command
 209 should be called with the {\tt -check} option. This will then cause synthesis
 210 to fail when implicit blackboxes are found in the design.
 211
 212 The 2nd thing we can improve regarding the {\tt hierarchy} command is that we
 213 can tell it the name of the top level module of the design hierarchy. It will
 214 then automatically remove all modules that are not referenced from this top
 215 level module.
 216
 217 \medskip
 218
 219 For many designs it is also desired to optimize the encodings for the finite
 220 state machines (FSMs) in the design. The {\tt fsm} command finds FSMs, extracts
 221 them, performs some basic optimizations and then generate a circuit from
 222 the extracted and optimized description. It would also be possible to tell
 223 the {\tt fsm} command to leave the FSMs in their extracted form, so they can be
 224 further processed using custom commands. But in this case we don't want that.
 225
 226 \medskip
 227
 228 So now we have the final synthesis script for generating a BLIF file
 229 for the Navr\'e CPU:
 230
 231 \begin{figure}[H]
 232 \begin{lstlisting}[language=sh]
 233 read_verilog softusb_navre.v
 234 hierarchy -check -top softusb_navre
 235 proc; opt; memory; opt; fsm; opt; techmap; opt
 236 write_blif softusb_navre.blif
 237 \end{lstlisting}
 238  \renewcommand{\figurename}{Listing}
 239 \caption{{\tt softusb\_navre.ys} (improved)}
 240 \end{figure}
 241
 242 \section{Advanced Example: The Amber23 ARMv2a CPU}
 243
 244 Our 2nd example is the Amber23 \cite{amber}
 245 ARMv2a CPU. Once again we base our example on the Verilog code that is included
 246 in yosys-bigsim \cite{bigsim}.
 247
 248 \begin{figure}[b!]
 249 \begin{lstlisting}[language=sh]
 250 read_verilog a23_alu.v
 251 read_verilog a23_barrel_shift_fpga.v
 252 read_verilog a23_barrel_shift.v
 253 read_verilog a23_cache.v
 254 read_verilog a23_coprocessor.v
 255 read_verilog a23_core.v
 256 read_verilog a23_decode.v
 257 read_verilog a23_execute.v
 258 read_verilog a23_fetch.v
 259 read_verilog a23_multiply.v
 260 read_verilog a23_ram_register_bank.v
 261 read_verilog a23_register_bank.v
 262 read_verilog a23_wishbone.v
 263 read_verilog generic_sram_byte_en.v
 264 read_verilog generic_sram_line_en.v
 265 hierarchy -check -top a23_core
 266 add -global_input globrst 1
 267 proc -global_arst globrst
 268 techmap -map adff2dff.v
 269 opt; memory; opt; fsm; opt; techmap
 270 write_blif amber23.blif
 271 \end{lstlisting}
 272  \renewcommand{\figurename}{Listing}
 273 \caption{\tt amber23.ys}
 274 \label{aber23.ys}
 275 \end{figure}
 276
 277 The problem with this core is that it contains no dedicated reset logic.
 278 Instead the coding techniques shown in Listing~\ref{glob_arst} are used to
 279 define reset values for the global asynchronous reset in an FPGA
 280 implementation. This design can not be expressed in BLIF as it is. Instead we
 281 need to use a synthesis script that transforms this form to synchronous resets that
 282 can be expressed in BLIF.
 283
 284 (Note that there is no problem if this coding techniques are used to model
 285 ROM, where the register is initialized using this syntax but is never updated
 286 otherwise.)
 287
 288 \medskip
 289
 290 Listing~\ref{aber23.ys} shows the synthesis script for the Amber23 core. In
 291 line 17 the {\tt add} command is used to add a 1-bit wide global input signal
 292 with the name {\tt globrst}. That means that an input with that name is added
 293 to each module in the design hierarchy and then all module instantiations are
 294 altered so that this new signal is connected throughout the whole design
 295 hierarchy.
 296
 297 \begin{figure}[t!]
 298 \begin{lstlisting}[language=Verilog]
 299 reg [7:0] a = 13, b;
 300 initial b = 37;
 301 \end{lstlisting}
 302  \renewcommand{\figurename}{Listing}
 303 \caption{Implicit coding of global asynchronous resets}
 304 \label{glob_arst}
 305 \end{figure}
 306
 307 \begin{figure}[b!]
 308 \begin{lstlisting}[language=Verilog]
 309 (* techmap_celltype = "$adff" *)
 310 module adff2dff (CLK, ARST, D, Q);
 311
 312 parameter WIDTH = 1;
 313 parameter CLK_POLARITY = 1;
 314 parameter ARST_POLARITY = 1;
 315 parameter ARST_VALUE = 0;
 316
 317 input CLK, ARST;
 318 input [WIDTH-1:0] D;
 319 output reg [WIDTH-1:0] Q;
 320
 321 wire [1023:0] _TECHMAP_DO_ = "proc";
 322
 323 wire _TECHMAP_FAIL_ =
 324     !CLK_POLARITY || !ARST_POLARITY;
 325
 326 always @(posedge CLK)
 327         if (ARST)
 328                 Q <= ARST_VALUE;
 329         else
 330                 Q <= D;
 331
 332 endmodule
 333 \end{lstlisting}
 334 \renewcommand{\figurename}{Listing}
 335 \caption{\tt adff2dff.v}
 336 \label{adff2dff.v}
 337 \end{figure}
 338
 339 In line 18 the {\tt proc} command is called. But in this script the signal name
 340 {\tt globrst} is passed to the command as a global reset signal for resetting
 341 the registers to their assigned initial values.
 342
 343 Finally in line 19 the {\tt techmap} command is used to replace all instances
 344 of flip-flops with asynchronous resets with flip-flops with synchronous resets.
 345 The map file used for this is shown in Listing~\ref{adff2dff.v}. Note how the
 346 {\tt techmap\_celltype} attribute is used in line 1 to tell the techmap command
 347 which cells to replace in the design, how the {\tt \_TECHMAP\_FAIL\_} wire in
 348 lines 15 and 16 (which evaluates to a constant value) determines if the
 349 parameter set is compatible with this replacement circuit, and how the {\tt
 350 \_TECHMAP\_DO\_} wire in line 13 provides a mini synthesis-script to be used to
 351 process this cell.
 352
 353 \begin{figure*}
 354 \begin{lstlisting}[language=C]
 355 #include <stdint.h>
 356 #include <stdbool.h>
 357
 358 #define BITMAP_SIZE 64
 359 #define OUTPORT 0x10000000
 360
 361 static uint32_t bitmap[BITMAP_SIZE/32];
 362
 363 static void bitmap_set(uint32_t idx) { bitmap[idx/32] |= 1 << (idx % 32); }
 364 static bool bitmap_get(uint32_t idx) { return (bitmap[idx/32] & (1 << (idx % 32))) != 0; }
 365 static void output(uint32_t val) { *((volatile uint32_t*)OUTPORT) = val; }
 366
 367 int main() {
 368         uint32_t i, j, k;
 369         output(2);
 370         for (i = 0; i < BITMAP_SIZE; i++) {
 371                 if (bitmap_get(i)) continue;
 372                 output(3+2*i);
 373                 for (j = 2*(3+2*i);; j += 3+2*i) {
 374                         if (j%2 == 0) continue;
 375                         k = (j-3)/2;
 376                         if (k >= BITMAP_SIZE) break;
 377                         bitmap_set(k);
 378                 }
 379         }
 380         output(0);
 381         return 0;
 382 }
 383 \end{lstlisting}
 384 \renewcommand{\figurename}{Listing}
 385 \caption{Test program for the Amber23 CPU (Sieve of Eratosthenes). Compiled using
 386 GCC 4.6.3 for ARM with {\tt -Os -marm -march=armv2a -mno-thumb-interwork
 387 -ffreestanding}, linked with {\tt -{}-fix-v4bx} set and booted with a custom
 388 setup routine written in ARM assembler.}
 389 \label{sieve}
 390 \end{figure*}
 391
 392 \section{Verification of the Amber23 CPU}
 393
 394 The BLIF file for the Amber23 core, generated using Listings~\ref{aber23.ys}
 395 and \ref{adff2dff.v} and the version of the Amber23 RTL source that is bundled
 396 with yosys-bigsim, was verified using the test-bench from yosys-bigsim.
 397 It successfully executed the program shown in Listing~\ref{sieve} in the
 398 test-bench.
 399
 400 For simulation the BLIF file was converted back to Verilog using ABC
 401 \cite{ABC}. So this test includes the successful transformation of the BLIF
 402 file into ABC's internal format as well.
 403
 404 The only thing left to write about the simulation itself is that it probably
 405 was one of the most energy inefficient and time consuming ways of successfully
 406 calculating the first 31 primes the author has ever conducted.
 407
 408 \section{Limitations}
 409
 410 At the time of this writing Yosys does not support multi-dimensional memories,
 411 does not support writing to individual bits of array elements, does not
 412 support initialization of arrays with {\tt \$readmemb} and {\tt \$readmemh},
 413 and has only limited support for tristate logic, to name just a few
 414 limitations.
 415
 416 That being said, Yosys can synthesize an overwhelming majority of real-world
 417 Verilog RTL code. The remaining cases can usually be modified to be compatible
 418 with Yosys quite easily.
 419
 420 The various designs in yosys-bigsim are a good place to look for examples
 421 of what is within the capabilities of Yosys.
 422
 423 \section{Conclusion}
 424
 425 Yosys is a feature-rich Verilog-2005 synthesis tool. It has many uses, but
 426 one is to provide an easy gateway from high-level Verilog code to low-level
 427 logic circuits.
 428
 429 The command line option {\tt -S} can be used to quickly synthesize Verilog
 430 code to BLIF files without a hassle.
 431
 432 With custom synthesis scripts it becomes possible to easily perform high-level
 433 optimizations, such as re-encoding FSMs. In some extreme cases, such as the
 434 Amber23 ARMv2 CPU, the more advanced Yosys features can be used to change a
 435 design to fit a certain need without actually touching the RTL code.
 436
 437 \begin{thebibliography}{9}
 438
 439 \bibitem{yosys}
 440 Clifford Wolf. The Yosys Open SYnthesis Suite. \\
 441 \url{http://www.clifford.at/yosys/}
 442
 443 \bibitem{bigsim}
 444 yosys-bigsim, a collection of real-world Verilog designs for regression testing purposes. \\
 445 \url{https://github.com/cliffordwolf/yosys-bigsim}
 446
 447 \bibitem{navre}
 448 Sebastien Bourdeauducq. Navr\'e AVR clone (8-bit RISC). \\
 449 \url{http://opencores.org/project,navre}
 450
 451 \bibitem{amber}
 452 Conor Santifort. Amber ARM-compatible core. \\
 453 \url{http://opencores.org/project,amber}
 454
 455 \bibitem{ABC}
 456 Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification. \\
 457 \url{http://www.eecs.berkeley.edu/~alanmi/abc/}
 458
 459 \bibitem{blif}
 460 Berkeley Logic Interchange Format (BLIF) \\
 461 \url{http://vlsi.colorado.edu/~vis/blif.ps}
 462
 463 \end{thebibliography}
 464
 465
 466 \end{document}