```
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
More information and documentation can be found on the Yosys web site:
http://www.clifford.at/yosys/
-
-Getting Started
-===============
+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).
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 \
+ libreadline-dev gawk tcl-dev libffi-dev git \
graphviz xdot pkg-config python3
+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
+
+On FreeBSD use the following command to install all prerequisites:
+
+ # pkg install bison flex readline gawk libffi\
+ git graphviz pkgconfig python3 python36 tcl-wrapper
+
+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
+
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
more information: http://www.clifford.at/yosys/download.html
Note that this also downloads, builds and installs ABC (using yosys-abc
as executable name).
+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:
Non-standard or SystemVerilog features for formal verification
==============================================================
-- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
+- 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. This is
- equivalent to declaring a reg as ``const rand``.
+- 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 task ``$anyseq`` evaluates to any value, possibly a different
- value in each cycle. This is equivalent to declaring a reg as ``rand``.
+- 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 functions ``$allconst`` and ``$allseq`` can be used to construct
+ formal exist-forall problems. Assumptions only hold if the trace satisfies
+ the assumtion 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``).
+
+- Wires/registers decalred 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 keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
and ``bit`` are supported.
-- Declaring free variables with ``rand`` and ``const rand`` is 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
==========================
projects / yosys.git / blobdiff