```
yosys -- Yosys Open SYnthesis Suite
-Copyright (C) 2012 - 2016 Clifford Wolf <clifford@clifford.at>
+Copyright (C) 2012 - 2018 Clifford Wolf <clifford@clifford.at>
Permission to use, copy, modify, and/or distribute this software for any
purpose with or without fee is hereby granted, provided that the above
or the 2-clause BSD license).
-Web Site
-========
+Web Site and Other Resources
+============================
More information and documentation can be found on the Yosys web site:
-http://www.clifford.at/yosys/
+- http://www.clifford.at/yosys/
+The "Documentation" page on the web site contains links to more resources,
+including a manual that even describes some of the Yosys internals:
+- http://www.clifford.at/yosys/documentation.html
-Getting Started
-===============
+The file `CodingReadme` in this directory contains additional information
+for people interested in using the Yosys C++ APIs.
+
+Users interested in formal verification might want to use the formal verification
+front-end for Yosys, SymbiYosys:
+- https://symbiyosys.readthedocs.io/en/latest/
+- https://github.com/YosysHQ/SymbiYosys
+
+
+Setup
+======
You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
-TCL, readline and libffi are optional (see ENABLE_* settings in Makefile).
+TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile).
Xdot (graphviz) is used by the ``show`` command in yosys to display schematics.
+
For example on Ubuntu Linux 16.04 LTS the following commands will install all
prerequisites for building yosys:
$ sudo apt-get install build-essential clang bison flex \
- libreadline-dev gawk tcl-dev libffi-dev git mercurial \
- graphviz xdot pkg-config python3
+ libreadline-dev gawk tcl-dev libffi-dev git \
+ graphviz xdot pkg-config python3 libboost-system-dev \
+ libboost-python-dev libboost-filesystem-dev
+
+Similarily, on Mac OS X MacPorts or Homebrew can be used to install dependencies:
+
+ $ brew tap Homebrew/bundle && brew bundle
+ $ sudo port install bison flex readline gawk libffi \
+ git graphviz pkgconfig python36 boost
+
+On FreeBSD use the following command to install all prerequisites:
+
+ # pkg install bison flex readline gawk libffi\
+ git graphviz pkgconfig python3 python36 tcl-wrapper boost-libs
+
+On FreeBSD system use gmake instead of make. To run tests use:
+ % MAKE=gmake CC=cc gmake test
+
+For Cygwin use the following command to install all prerequisites, or select these additional packages:
+
+ setup-x86_64.exe -q --packages=bison,flex,gcc-core,gcc-g++,git,libffi-devel,libreadline-devel,make,pkg-config,python3,tcl-devel,boost-build
There are also pre-compiled Yosys binary packages for Ubuntu and Win32 as well
as a source distribution for Visual Studio. Visit the Yosys download page for
To build Yosys simply type 'make' in this directory.
$ make
- $ make test
$ sudo make install
Note that this also downloads, builds and installs ABC (using yosys-abc
as executable name).
+Tests are located in the tests subdirectory and can be executed using the test target. Note that you need gawk as well as a recent version of iverilog (i.e. build from git). Then, execute tests via:
+
+ $ make test
+
+Getting Started
+===============
+
Yosys can be used with the interactive command shell, with
synthesis scripts or with command line arguments. Let's perform
a simple synthesis job using the interactive command shell:
yosys> read_verilog tests/simple/fiedler-cooley.v
-writing the design to the console in yosys's internal format:
+writing the design to the console in Yosys's internal format:
yosys> write_ilang
techmap; opt
If ABC is enabled in the Yosys build configuration and a cell library is given
-in the liberty file ``mycells.lib``, the following synthesis script will synthesize
-for the given cell library:
+in the liberty file ``mycells.lib``, the following synthesis script will
+synthesize for the given cell library:
# the high-level stuff
hierarchy; proc; fsm; opt; memory; opt
- http://www.vlsitechnology.org/html/libraries.html
- http://www.vlsitechnology.org/synopsys/vsclib013.lib
-The command ``synth`` provides a good default synthesis script (see ``help synth``).
-If possible a synthesis script should borrow from ``synth``. For example:
+The command ``synth`` provides a good default synthesis script (see
+``help synth``). If possible a synthesis script should borrow from ``synth``.
+For example:
# the high-level stuff
hierarchy
=================================
The following Verilog-2005 features are not supported by
-yosys and there are currently no plans to add support
+Yosys and there are currently no plans to add support
for them:
- Non-synthesizable language features as defined in
IEC 62142(E):2005 / IEEE Std. 1364.1(E):2002
-- The ``tri``, ``triand``, ``trior``, ``wand`` and ``wor`` net types
-
-- The ``config`` keyword and library map files
+- The ``tri``, ``triand`` and ``trior`` net types
-- The ``disable``, ``primitive`` and ``specify`` statements
-
-- Latched logic (is synthesized as logic with feedback loops)
+- The ``config`` and ``disable`` keywords and library map files
Verilog Attributes and non-standard features
storage element. The register itself will always have all bits set
to 'x' (undefined). The variable may only be used as blocking assigned
temporary variable within an always block. This is mostly used internally
- by yosys to synthesize Verilog functions and access arrays.
+ by Yosys to synthesize Verilog functions and access arrays.
-- The ``onehot`` attribute on wires mark them as onehot state register. This
+- The ``onehot`` attribute on wires mark them as one-hot state register. This
is used for example for memory port sharing and set by the fsm_map pass.
- The ``blackbox`` attribute on modules is used to mark empty stub modules
that have the same ports as the real thing but do not contain information
on the internal configuration. This modules are only used by the synthesis
passes to identify input and output ports of cells. The Verilog backend
- also does not output blackbox modules on default.
+ also does not output blackbox modules on default. ``read_verilog``, unless
+ called with ``-noblackbox`` will automatically set the blackbox attribute
+ on any empty module it reads.
+
+- The ``noblackbox`` attribute set on an empty module prevents ``read_verilog``
+ from automatically setting the blackbox attribute on the module.
+
+- The ``whitebox`` attribute on modules triggers the same behavior as
+ ``blackbox``, but is for whitebox modules, i.e. library modules that
+ contain a behavioral model of the cell type.
+
+- The ``lib_whitebox`` attribute overwrites ``whitebox`` when ``read_verilog``
+ is run in `-lib` mode. Otherwise it's automatically removed.
+
+- The ``dynports`` attribute is used by the Verilog front-end to mark modules
+ that have ports with a width that depends on a parameter.
+
+- The ``hdlname`` attribute is used by some passes to document the original
+ (HDL) name of a module when renaming a module.
- The ``keep`` attribute on cells and wires is used to mark objects that should
never be removed by the optimizer. This is used for example for cells that
command from flattening the indicated cells and modules.
- The ``init`` attribute on wires is set by the frontend when a register is
- initialized "FPGA-style" with ``reg foo = val``. It can be used during synthesis
- to add the necessary reset logic.
+ initialized "FPGA-style" with ``reg foo = val``. It can be used during
+ synthesis to add the necessary reset logic.
- The ``top`` attribute on a module marks this module as the top of the
design hierarchy. The ``hierarchy`` command sets this attribute when called
through the synthesis. When entities are combined, a new |-separated
string is created that contains all the string from the original entities.
-- In addition to the ``(* ... *)`` attribute syntax, yosys supports
+- In addition to the ``(* ... *)`` attribute syntax, Yosys supports
the non-standard ``{* ... *}`` attribute syntax to set default attributes
for everything that comes after the ``{* ... *}`` statement. (Reset
by adding an empty ``{* *}`` statement.)
- In module parameter and port declarations, and cell port and parameter
- lists, a trailing comma is ignored. This simplifies writing verilog code
+ lists, a trailing comma is ignored. This simplifies writing Verilog code
generators a bit in some cases.
- Modules can be declared with ``module mod_name(...);`` (with three dots
- When defining a macro with `define, all text between triple double quotes
is interpreted as macro body, even if it contains unescaped newlines. The
- tipple double quotes are removed from the macro body. For example:
+ triple double quotes are removed from the macro body. For example:
`define MY_MACRO(a, b) """
assign a = 23;
$ yosys -p 'plugin -a foo -i /lib/libm.so; read_verilog dpitest.v'
- Sized constants (the syntax ``<size>'s?[bodh]<value>``) support constant
- expressions as <size>. If the expression is not a simple identifier, it
+ expressions as ``<size>``. If the expression is not a simple identifier, it
must be put in parentheses. Examples: ``WIDTH'd42``, ``(4+2)'b101010``
-- The system tasks ``$finish`` and ``$display`` are supported in initial blocks
- in an unconditional context (only if/case statements on parameters
- and constant values). The intended use for this is synthesis-time DRC.
+- The system tasks ``$finish``, ``$stop`` and ``$display`` are supported in
+ initial blocks in an unconditional context (only if/case statements on
+ expressions over parameters and constant values are allowed). The intended
+ use for this is synthesis-time DRC.
+
+- There is limited support for converting specify .. endspecify statements to
+ special ``$specify2``, ``$specify3``, and ``$specrule`` cells, for use in
+ blackboxes and whiteboxes. Use ``read_verilog -specify`` to enable this
+ functionality. (By default specify .. endspecify blocks are ignored.)
Non-standard or SystemVerilog features for formal verification
==============================================================
-- Support for ``assert``, ``assume``, and ``restrict`` is enabled when
- ``read_verilog`` is called with ``-formal``.
+- Support for ``assert``, ``assume``, ``restrict``, and ``cover`` is enabled
+ when ``read_verilog`` is called with ``-formal``.
- The system task ``$initstate`` evaluates to 1 in the initial state and
to 0 otherwise.
-- The system task ``$anyconst`` evaluates to any constant value.
+- The system function ``$anyconst`` evaluates to any constant value. This is
+ equivalent to declaring a reg as ``rand const``, but also works outside
+ of checkers. (Yosys also supports ``rand const`` outside checkers.)
+
+- The system function ``$anyseq`` evaluates to any value, possibly a different
+ value in each cycle. This is equivalent to declaring a reg as ``rand``,
+ but also works outside of checkers. (Yosys also supports ``rand``
+ variables outside checkers.)
-- The system task ``$anyseq`` evaluates to any value, possibly a different
- value in each cycle.
+- The system functions ``$allconst`` and ``$allseq`` can be used to construct
+ formal exist-forall problems. Assumptions only hold if the trace satisfies
+ the assumption for all ``$allconst/$allseq`` values. For assertions and cover
+ statements it is sufficient if just one ``$allconst/$allseq`` value triggers
+ the property (similar to ``$anyconst/$anyseq``).
-- The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are supported
- in any clocked block.
+- Wires/registers declared using the ``anyconst/anyseq/allconst/allseq`` attribute
+ (for example ``(* anyconst *) reg [7:0] foobar;``) will behave as if driven
+ by a ``$anyconst/$anyseq/$allconst/$allseq`` function.
+
+- The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
+ supported in any clocked block.
- The syntax ``@($global_clock)`` can be used to create FFs that have no
- explicit clock input ($ff cells).
+ explicit clock input (``$ff`` cells). The same can be achieved by using
+ ``@(posedge <netname>)`` or ``@(negedge <netname>)`` when ``<netname>``
+ is marked with the ``(* gclk *)`` Verilog attribute.
Supported features from SystemVerilog
- The ``assert`` statement from SystemVerilog is supported in its most basic
form. In module context: ``assert property (<expression>);`` and within an
- always block: ``assert(<expression>);``. It is transformed to a $assert cell.
+ always block: ``assert(<expression>);``. It is transformed to an ``$assert`` cell.
+
+- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
+ also supported. The same limitations as with the ``assert`` statement apply.
-- The ``assume`` and ``restrict`` statements from SystemVerilog are also
- supported. The same limitations as with the ``assert`` statement apply.
+- The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
+ and ``bit`` are supported.
-- The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic`` and
- ``bit`` are supported.
+- Declaring free variables with ``rand`` and ``rand const`` is supported.
+
+- Checkers without a port list that do not need to be instantiated (but instead
+ behave like a named block) are supported.
- SystemVerilog packages are supported. Once a SystemVerilog file is read
into a design with ``read_verilog``, all its packages are available to
SystemVerilog files being read into the same design afterwards.
+- SystemVerilog interfaces (SVIs) are supported. Modports for specifying whether
+ ports are inputs or outputs are supported.
+
Building the documentation
==========================
Notes:
-- To run `make manual` you need to have installed yosys with `make install`,
+- To run `make manual` you need to have installed Yosys with `make install`,
otherwise it will fail on finding `kernel/yosys.h` while building
`PRESENTATION_Prog`.
projects / yosys.git / blobdiff