X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=README.md;h=840f2c8b25515f9ea4fd72bf8be3b216fd12c2dd;hb=4b9f619349e6b7452739631635ab3b5a4d94b522;hp=396189d5fff56ac57233d49201d82c597cc23368;hpb=ef4a28e112be10d3d62395f68e53e8b7e42dbf68;p=yosys.git diff --git a/README.md b/README.md index 396189d5f..840f2c8b2 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ``` yosys -- Yosys Open SYnthesis Suite -Copyright (C) 2012 - 2016 Clifford Wolf +Copyright (C) 2012 - 2018 Clifford Wolf Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above @@ -40,21 +40,39 @@ Web Site 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 @@ -80,6 +98,9 @@ To build Yosys simply type 'make' in this directory. 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: @@ -372,23 +393,38 @@ Verilog Attributes and non-standard features 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 )`` or ``@(negedge )`` when ```` + is marked with the ``(* gclk *)`` Verilog attribute. Supported features from SystemVerilog @@ -407,12 +443,18 @@ 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 ==========================