Use pkg-config for linking tcl-tk

Both MacPorts and Homebrew have a pkg-config file for TCL. So lets use it.

.gitignore

@@ -1,6 +1,7 @@
 *.o
 *.d
 .*.swp
+*.gch
 /.cproject
 /.project
 /.settings
@@ -27,3 +28,5 @@
 /yosys-win32-vcxsrc-*
 /yosysjs-*
 /libyosys.so
+/tests/unit/bintest/
+/tests/unit/objtest/

CodingReadme

@@ -411,3 +411,72 @@ Updating the website:
 	git commit -am update
 	make push
 
+How to add unit test
+====================
+
+Unit test brings some advantages, briefly, we can list some of them (reference
+[1](https://en.wikipedia.org/wiki/Unit_testing)):
+
+* Tests reduce bugs in new features;
+* Tests reduce bugs in existing features;
+* Tests are good documentation;
+* Tests reduce the cost of change;
+* Tests allow refactoring;
+
+With those advantages in mind, it was required to choose a framework which fits
+well with C/C++ code.  Hence, it was chosen (google test)
+[https://github.com/google/googletest], because it is largely used and it is
+relatively easy learn.
+
+Install and configure google test (manually)
+--------------------------------------------
+
+In this section, you will see a brief description of how to install google
+test. However, it is strongly recommended that you take a look to the official
+repository (https://github.com/google/googletest) and refers to that if you
+have any problem to install it. Follow the steps below:
+
+* Install: cmake and pthread
+* Clone google test project from: https://github.com/google/googletest and
+  enter in the project directory
+* Inside project directory, type:
+
+```
+cmake -DBUILD_SHARED_LIBS=ON .
+make
+```
+
+* After compilation, copy all "*.so" inside directory "googlemock" and
+  "googlemock/gtest" to "/usr/lib/"
+* Done! Now you can compile your tests.
+
+If you have any problem, go to the official repository to find help.
+
+Ps.: Some distros already have googletest packed. If your distro supports it,
+you can use it instead of compile.
+
+Create new unit test
+--------------------
+
+If you want to add new unit tests for Yosys, just follow the steps below:
+
+* Go to directory "yosys/test/unit/"
+* In this directory you can find something similar Yosys's directory structure.
+  To create your unit test file you have to follow this pattern:
+  fileNameToImplementUnitTest + Test.cc. E.g.: if you want to implement the
+  unit test for kernel/celledges.cc, you will need to create a file like this:
+  tests/unit/kernel/celledgesTest.cc;
+* Implement your unit test
+
+Run unit test
+-------------
+
+To compile and run all unit tests, just go to yosys root directory and type:
+```
+make unit-test
+```
+
+If you want to remove all unit test files, type:
+```
+make clean-unit-test
+```

Makefile

@@ -18,6 +18,7 @@ ENABLE_LIBYOSYS := 0
 # other configuration flags
 ENABLE_GPROF := 0
 ENABLE_NDEBUG := 0
+LINK_CURSES := 0
 
 # clang sanitizers
 SANITIZER =
@@ -44,6 +45,9 @@ TARGETS = yosys$(EXE) yosys-config
 PRETTY = 1
 SMALL = 0
 
+# Unit test
+UNITESTPATH := tests/unit
+
 all: top-all
 
 YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST)))
@@ -53,26 +57,42 @@ CXXFLAGS += -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(PRE
 LDFLAGS += -L$(LIBDIR)
 LDLIBS = -lstdc++ -lm
 
-PKG_CONFIG = pkg-config
-SED = sed
-BISON = bison
+PKG_CONFIG ?= pkg-config
+SED ?= sed
+BISON ?= bison
 
 ifeq (Darwin,$(findstring Darwin,$(shell uname)))
-	# add macports/homebrew include and library path to search directories, don't use '-rdynamic' and '-lrt':
-	CXXFLAGS += -I/opt/local/include -I/usr/local/opt/readline/include
-	LDFLAGS += -L/opt/local/lib -L/usr/local/opt/readline/lib
-	# add homebrew's libffi include and library path
-	CXXFLAGS += $(shell PKG_CONFIG_PATH=$$(brew list libffi | grep pkgconfig | xargs dirname) pkg-config --silence-errors --cflags libffi)
-	LDFLAGS += $(shell PKG_CONFIG_PATH=$$(brew list libffi | grep pkgconfig | xargs dirname) pkg-config --silence-errors --libs libffi)
-	# use bison installed by homebrew if available
-	BISON = $(shell (brew list bison | grep -m1 "bin/bison") || echo bison)
-	SED = sed
-else
-	LDFLAGS += -rdynamic
-	LDLIBS += -lrt
+
+# homebrew search paths
+ifneq ($(shell which brew),)
+BREW_PREFIX := $(shell brew --prefix)/opt
+
+CXXFLAGS += -I$(BREW_PREFIX)/readline/include
+LDFLAGS += -L$(BREW_PREFIX)/readline/lib
+
+PKG_CONFIG_PATH := $(BREW_PREFIX)/libffi/lib/pkgconfig:$(PKG_CONFIG_PATH)
+PKG_CONFIG_PATH := $(BREW_PREFIX)/tcl-tk/lib/pkgconfig:$(PKG_CONFIG_PATH)
+
+export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX)/flex/bin:$(PATH)
+
+# macports search paths
+else ifneq ($(shell which port),)
+PORT_PREFIX := $(patsubst %/bin/port,%,$(shell which port))
+
+CXXFLAGS += -I$(PORT_PREFIX)/include
+LDFLAGS += -L$(PORT_PREFIX)/lib
+
+PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH)
+
+export PATH := $(PORT_PREFIX)/bin:$(PATH)
 endif
 
-YOSYS_VER := 0.7
+else
+LDFLAGS += -rdynamic
+LDLIBS += -lrt
+endif
+
+YOSYS_VER := 0.7+$(shell cd $(YOSYS_SRC) && test -e .git && { git log --author=clifford@clifford.at --oneline 61f6811.. | wc -l; })
 GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
 OBJS = kernel/version_$(GIT_REV).o
 
@@ -82,7 +102,7 @@ OBJS = kernel/version_$(GIT_REV).o
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = eb6eca6807cc
+ABCREV = f8cadfe3861f
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"
@@ -170,7 +190,7 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -x c++ -fpermissive -w"
+ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
 ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1 CC="$(CXX)" CXX="$(CXX)"
 EXE = .exe
 
@@ -181,7 +201,7 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -x c++ -fpermissive -w"
+ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
 ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0 CC="$(CXX)" CXX="$(CXX)"
 EXE = .exe
 
@@ -196,21 +216,26 @@ endif
 ifeq ($(ENABLE_READLINE),1)
 CXXFLAGS += -DYOSYS_ENABLE_READLINE
 LDLIBS += -lreadline
+ifeq ($(LINK_CURSES),1)
+LDLIBS += -lcurses
+ABCMKARGS += "ABC_READLINE_LIBRARIES=-lcurses -lreadline"
+endif
 ifeq ($(CONFIG),mxe)
 LDLIBS += -lpdcurses
 endif
 endif
 
 ifeq ($(ENABLE_PLUGINS),1)
-CXXFLAGS += -DYOSYS_ENABLE_PLUGINS $(shell $(PKG_CONFIG) --silence-errors --cflags libffi)
-LDLIBS += $(shell $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) -ldl
+CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags libffi) -DYOSYS_ENABLE_PLUGINS
+LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) -ldl
 endif
 
 ifeq ($(ENABLE_TCL),1)
 TCL_VERSION ?= tcl$(shell bash -c "tclsh <(echo 'puts [info tclversion]')")
 TCL_INCLUDE ?= /usr/include/$(TCL_VERSION)
-CXXFLAGS += -I$(TCL_INCLUDE) -DYOSYS_ENABLE_TCL
-LDLIBS += -l$(TCL_VERSION)
+
+CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags tcl || echo -I$(TCL_INCLUDE)) -DYOSYS_ENABLE_TCL
+LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo -l$(TCL_VERSION))
 endif
 
 ifeq ($(ENABLE_GPROF),1)
@@ -442,6 +467,14 @@ vloghtb: $(TARGETS) $(EXTRA_TARGETS)
 	@echo "  Passed \"make vloghtb\"."
 	@echo ""
 
+# Unit test
+unit-test: libyosys.so
+	@$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \
+		CXXFLAGS="$(CXXFLAGS)" LDLIBS="$(LDLIBS)" ROOTPATH="$(CURDIR)"
+
+clean-unit-test:
+	@$(MAKE) -C $(UNITESTPATH) clean
+
 install: $(TARGETS) $(EXTRA_TARGETS)
 	$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR)
 	$(INSTALL_SUDO) install $(TARGETS) $(DESTDIR)$(BINDIR)

README.md

@@ -1,26 +1,23 @@
-
- /-----------------------------------------------------------------------------\
- |                                                                             |
- |  yosys -- Yosys Open SYnthesis Suite                                        |
- |                                                                             |
- |  Copyright (C) 2012 - 2016  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     |
- |  copyright notice and this permission notice appear in all copies.          |
- |                                                                             |
- |  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES   |
- |  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF           |
- |  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR    |
- |  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES     |
- |  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN      |
- |  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF    |
- |  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.             |
- |                                                                             |
- \-----------------------------------------------------------------------------/
-
-
+```
 yosys -- Yosys Open SYnthesis Suite
+
+Copyright (C) 2012 - 2016  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
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+```
+
+
+yosys – Yosys Open SYnthesis Suite
 ===================================
 
 This is a framework for RTL synthesis tools. It currently has
@@ -41,17 +38,16 @@ Web Site
 ========
 
 More information and documentation can be found on the Yosys web site:
+http://www.clifford.at/yosys/
 
-	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.
+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:
 
@@ -59,11 +55,16 @@ prerequisites for building yosys:
 		libreadline-dev gawk tcl-dev libffi-dev git mercurial \
 		graphviz xdot pkg-config python3
 
+Similarily, on Mac OS X MacPorts or Homebrew can be used to install dependencies:
+
+	$ brew install bison flex gawk libffi \
+		git mercurial graphviz pkg-config python3
+	$ sudo port install bison flex readline gawk libffi \
+		git mercurial graphviz pkgconfig python36
+
 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
+more information: http://www.clifford.at/yosys/download.html
 
 To configure the build system to use a specific compiler, use one of
 
@@ -74,7 +75,7 @@ For other compilers and build configurations it might be
 necessary to make some changes to the config section of the
 Makefile.
 
-	$ vi Makefile             ..or..
+	$ vi Makefile            # ..or..
 	$ vi Makefile.conf
 
 To build Yosys simply type 'make' in this directory.
@@ -86,6 +87,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:
@@ -93,8 +97,8 @@ a simple synthesis job using the interactive command shell:
 	$ ./yosys
 	yosys>
 
-the command "help" can be used to print a list of all available
-commands and "help <command>" to print details on the specified command:
+the command ``help`` can be used to print a list of all available
+commands and ``help <command>`` to print details on the specified command:
 
 	yosys> help help
 
@@ -110,16 +114,16 @@ elaborate design hierarchy:
 
 	yosys> hierarchy
 
-convert processes ("always" blocks) to netlist elements and perform
+convert processes (``always`` blocks) to netlist elements and perform
 some simple optimizations:
 
 	yosys> proc; opt
 
-display design netlist using xdot:
+display design netlist using ``xdot``:
 
 	yosys> show
 
-the same thing using 'gv' as postscript viewer:
+the same thing using ``gv`` as postscript viewer:
 
 	yosys> show -format ps -viewer gv
 
@@ -171,8 +175,8 @@ The following very basic synthesis script should work well with all designs:
 	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
@@ -190,16 +194,17 @@ for the given cell library:
 	clean
 
 If you do not have a liberty file but want to test this synthesis script,
-you can use the file examples/cmos/cmos_cells.lib from the yosys sources.
+you can use the file ``examples/cmos/cmos_cells.lib`` from the yosys sources.
 
 Liberty file downloads for and information about free and open ASIC standard
 cell libraries can be found here:
 
-	http://www.vlsitechnology.org/html/libraries.html
-	http://www.vlsitechnology.org/synopsys/vsclib013.lib
+- 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
@@ -224,11 +229,11 @@ 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 ``tri``, ``triand``, ``trior``, ``wand`` and ``wor`` net types
 
-- The "config" keyword and library map files
+- The ``config`` keyword and library map files
 
-- The "disable", "primitive" and "specify" statements
+- The ``disable``, ``primitive`` and ``specify`` statements
 
 - Latched logic (is synthesized as logic with feedback loops)
 
@@ -236,83 +241,83 @@ for them:
 Verilog Attributes and non-standard features
 ============================================
 
-- The 'full_case' attribute on case statements is supported
-  (also the non-standard "// synopsys full_case" directive)
+- The ``full_case`` attribute on case statements is supported
+  (also the non-standard ``// synopsys full_case`` directive)
 
-- The 'parallel_case' attribute on case statements is supported
-  (also the non-standard "// synopsys parallel_case" directive)
+- The ``parallel_case`` attribute on case statements is supported
+  (also the non-standard ``// synopsys parallel_case`` directive)
 
-- The "// synopsys translate_off" and "// synopsys translate_on"
-  directives are also supported (but the use of `ifdef .. `endif
+- The ``// synopsys translate_off`` and ``// synopsys translate_on``
+  directives are also supported (but the use of ``` `ifdef .. `endif ```
   is strongly recommended instead).
 
-- The "nomem2reg" attribute on modules or arrays prohibits the
+- The ``nomem2reg`` attribute on modules or arrays prohibits the
   automatic early conversion of arrays to separate registers. This
   is potentially dangerous. Usually the front-end has good reasons
   for converting an array to a list of registers. Prohibiting this
   step will likely result in incorrect synthesis results.
 
-- The "mem2reg" attribute on modules or arrays forces the early
+- The ``mem2reg`` attribute on modules or arrays forces the early
   conversion of arrays to separate registers.
 
-- The "nomeminit" attribute on modules or arrays prohibits the
-  creation of initialized memories. This effectively puts "mem2reg"
-  on all memories that are written to in an "initial" block and
+- The ``nomeminit`` attribute on modules or arrays prohibits the
+  creation of initialized memories. This effectively puts ``mem2reg``
+  on all memories that are written to in an ``initial`` block and
   are not ROMs.
 
-- The "nolatches" attribute on modules or always-blocks
+- The ``nolatches`` attribute on modules or always-blocks
   prohibits the generation of logic-loops for latches. Instead
   all not explicitly assigned values default to x-bits. This does
   not affect clocked storage elements such as flip-flops.
 
-- The "nosync" attribute on registers prohibits the generation of a
+- The ``nosync`` attribute on registers prohibits the generation of a
   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.
 
-- The "onehot" attribute on wires mark them as onehot state register. This
+- The ``onehot`` attribute on wires mark them as onehot 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
+- 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.
 
-- The "keep" attribute on cells and wires is used to mark objects that should
+- 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
   have hidden connections that are not part of the netlist, such as IO pads.
-  Setting the "keep" attribute on a module has the same effect as setting it
+  Setting the ``keep`` attribute on a module has the same effect as setting it
   on all instances of the module.
 
-- The "keep_hierarchy" attribute on cells and modules keeps the "flatten"
+- The ``keep_hierarchy`` attribute on cells and modules keeps the ``flatten``
   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.
+- 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.
 
-- The "top" attribute on a module marks this module as the top of the
-  design hierarchy. The "hierarchy" command sets this attribute when called
-  with "-top". Other commands, such as "flatten" and various backends
+- The ``top`` attribute on a module marks this module as the top of the
+  design hierarchy. The ``hierarchy`` command sets this attribute when called
+  with ``-top``. Other commands, such as ``flatten`` and various backends
   use this attribute to determine the top module.
 
-- The "src" attribute is set on cells and wires created by to the string
-  "<hdl-file-name>:<line-number>" by the HDL front-end and is then carried
+- The ``src`` attribute is set on cells and wires created by to the string
+  ``<hdl-file-name>:<line-number>`` by the HDL front-end and is then carried
   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
-  the non-standard {* ... *} attribute syntax to set default attributes
-  for everything that comes after the {* ... *} statement. (Reset
-  by adding an empty {* *} statement.)
+- 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
   generators a bit in some cases.
 
-- Modules can be declared with "module mod_name(...);" (with three dots
+- Modules can be declared with ``module mod_name(...);`` (with three dots
   instead of a list of module ports). With this syntax it is sufficient
   to simply declare a module port as 'input' or 'output' in the module
   body.
@@ -326,7 +331,7 @@ Verilog Attributes and non-standard features
          assign b = 42;
       """
 
-- The attribute "via_celltype" can be used to implement a Verilog task or
+- The attribute ``via_celltype`` can be used to implement a Verilog task or
   function by instantiating the specified cell type. The value is the name
   of the cell type to use. For functions the name of the output port can
   be specified by appending it to the cell type separated by a whitespace.
@@ -354,9 +359,9 @@ Verilog Attributes and non-standard features
       endmodule
 
 - A limited subset of DPI-C functions is supported. The plugin mechanism
-  (see "help plugin") can be used to load .so files with implementations
+  (see ``help plugin``) can be used to load .so files with implementations
   of DPI-C routines. As a non-standard extension it is possible to specify
-  a plugin alias using the "<alias>:" syntax. for example:
+  a plugin alias using the ``<alias>:`` syntax. For example:
 
       module dpitest;
         import "DPI-C" function foo:round = real my_round (real);
@@ -365,11 +370,11 @@ Verilog Attributes and non-standard features
 
       $ yosys -p 'plugin -a foo -i /lib/libm.so; read_verilog dpitest.v'
 
-- Sized constants (the syntax <size>'s?[bodh]<value>) support constant
+- Sized constants (the syntax ``<size>'s?[bodh]<value>``) support constant
   expressions as <size>. If the expression is not a simple identifier, it
-  must be put in parentheses. Examples: WIDTH'd42, (4+2)'b101010
+  must be put in parentheses. Examples: ``WIDTH'd42``, ``(4+2)'b101010``
 
-- The system tasks $finish and $display are supported in initial blocks
+- 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.
 
@@ -377,42 +382,42 @@ Verilog Attributes and non-standard features
 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``, and ``restrict`` is enabled when
+  ``read_verilog`` is called with ``-formal``.
 
-- The system task $initstate evaluates to 1 in the initial state and
+- 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 task ``$anyconst`` evaluates to any constant value.
 
-- The system task $anyseq evaluates to any value, possibly a different
+- The system task ``$anyseq`` evaluates to any value, possibly a different
   value in each cycle.
 
-- The SystemVerilog tasks $past, $stable, $rose and $fell are supported
-  in any clocked block.
+- 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
+- The syntax ``@($global_clock)`` can be used to create FFs that have no
   explicit clock input ($ff cells).
 
 
 Supported features from SystemVerilog
 =====================================
 
-When read_verilog is called with -sv, it accepts some language features
+When ``read_verilog`` is called with ``-sv``, it accepts some language 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.
+- 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.
 
-- The "assume" and "restrict" 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.
 
 - SystemVerilog packages are supported. Once a SystemVerilog file is read
-  into a design with "read_verilog", all its packages are available to
+  into a design with ``read_verilog``, all its packages are available to
   SystemVerilog files being read into the same design afterwards.
 
 
@@ -448,4 +453,3 @@ Notes:
 - 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`.
-

backends/aiger/Makefile.inc

@@ -0,0 +1,3 @@
+
+OBJS += backends/aiger/aiger.o
+

backends/aiger/aiger.cc

@@ -0,0 +1,552 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  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
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+void aiger_encode(std::ostream &f, int x)
+{
+	log_assert(x >= 0);
+
+	while (x & ~0x7f) {
+		f.put((x & 0x7f) | 0x80);
+		x = x >> 7;
+	}
+
+	f.put(x);
+}
+
+struct AigerWriter
+{
+	Module *module;
+	bool zinit_mode;
+	SigMap sigmap;
+
+	dict<SigBit, bool> init_map;
+	pool<SigBit> input_bits, output_bits;
+	dict<SigBit, SigBit> not_map, ff_map;
+	dict<SigBit, pair<SigBit, SigBit>> and_map;
+	vector<pair<SigBit, SigBit>> asserts, assumes;
+	pool<SigBit> initstate_bits;
+
+	vector<pair<int, int>> aig_gates;
+	vector<int> aig_latchin, aig_latchinit, aig_outputs;
+	int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0, aig_b = 0, aig_c = 0;
+
+	dict<SigBit, int> aig_map;
+	dict<SigBit, int> ordered_outputs;
+	dict<SigBit, int> ordered_latches;
+
+	dict<SigBit, int> init_inputs;
+	int initstate_ff = 0;
+
+	int mkgate(int a0, int a1)
+	{
+		aig_m++, aig_a++;
+		aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0));
+		return 2*aig_m;
+	}
+
+	int bit2aig(SigBit bit)
+	{
+		if (aig_map.count(bit) == 0)
+		{
+			aig_map[bit] = -1;
+
+			if (initstate_bits.count(bit)) {
+				log_assert(initstate_ff > 0);
+				aig_map[bit] = initstate_ff;
+			} else
+			if (not_map.count(bit)) {
+				int a = bit2aig(not_map.at(bit)) ^ 1;
+				aig_map[bit] = a;
+			} else
+			if (and_map.count(bit)) {
+				auto args = and_map.at(bit);
+				int a0 = bit2aig(args.first);
+				int a1 = bit2aig(args.second);
+				aig_map[bit] = mkgate(a0, a1);
+			}
+		}
+
+		log_assert(aig_map.at(bit) >= 0);
+		return aig_map.at(bit);
+	}
+
+	AigerWriter(Module *module, bool zinit_mode) : module(module), zinit_mode(zinit_mode), sigmap(module)
+	{
+		for (auto wire : module->wires())
+		{
+			if (wire->attributes.count("\\init")) {
+				SigSpec initsig = sigmap(wire);
+				Const initval = wire->attributes.at("\\init");
+				for (int i = 0; i < GetSize(wire) && i < GetSize(initval); i++)
+					if (initval[i] == State::S0 || initval[i] == State::S1)
+						init_map[initsig[i]] = initval[i] == State::S1;
+			}
+
+			if (wire->port_input)
+				for (auto bit : sigmap(wire))
+					input_bits.insert(bit);
+
+			if (wire->port_output)
+				for (auto bit : sigmap(wire))
+					output_bits.insert(bit);
+		}
+
+		for (auto cell : module->cells())
+		{
+			if (cell->type == "$_NOT_")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				not_map[Y] = A;
+				continue;
+			}
+
+			if (cell->type.in("$_FF_", "$_DFF_N_", "$_DFF_P_"))
+			{
+				SigBit D = sigmap(cell->getPort("\\D").as_bit());
+				SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
+				ff_map[Q] = D;
+				continue;
+			}
+
+			if (cell->type == "$_AND_")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit B = sigmap(cell->getPort("\\B").as_bit());
+				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				and_map[Y] = make_pair(A, B);
+				continue;
+			}
+
+			if (cell->type == "$initstate")
+			{
+				SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
+				initstate_bits.insert(Y);
+				continue;
+			}
+
+			if (cell->type == "$assert")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				asserts.push_back(make_pair(A, EN));
+				continue;
+			}
+
+			if (cell->type == "$assume")
+			{
+				SigBit A = sigmap(cell->getPort("\\A").as_bit());
+				SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
+				assumes.push_back(make_pair(A, EN));
+				continue;
+			}
+
+			if (cell->type == "$anyconst")
+			{
+				for (auto bit : sigmap(cell->getPort("\\Y")))
+					ff_map[bit] = bit;
+				continue;
+			}
+
+			log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
+		}
+
+		init_map.sort();
+		input_bits.sort();
+		output_bits.sort();
+		not_map.sort();
+		ff_map.sort();
+		and_map.sort();
+
+		aig_map[State::S0] = 0;
+		aig_map[State::S1] = 1;
+
+		for (auto bit : input_bits) {
+			aig_m++, aig_i++;
+			aig_map[bit] = 2*aig_m;
+		}
+
+		if (zinit_mode)
+		{
+			for (auto it : ff_map) {
+				if (init_map.count(it.first))
+					continue;
+				aig_m++, aig_i++;
+				init_inputs[it.first] = 2*aig_m;
+			}
+		}
+
+		for (auto it : ff_map) {
+			aig_m++, aig_l++;
+			aig_map[it.first] = 2*aig_m;
+			ordered_latches[it.first] = aig_l-1;
+			if (init_map.count(it.first) == 0)
+				aig_latchinit.push_back(2);
+			else
+				aig_latchinit.push_back(init_map.at(it.first) ? 1 : 0);
+		}
+
+		if (!initstate_bits.empty() || !init_inputs.empty()) {
+			aig_m++, aig_l++;
+			initstate_ff = 2*aig_m+1;
+			aig_latchinit.push_back(0);
+		}
+
+		if (zinit_mode)
+		{
+			for (auto it : ff_map)
+			{
+				int l = ordered_latches[it.first];
+
+				if (aig_latchinit.at(l) == 1)
+					aig_map[it.first] ^= 1;
+
+				if (aig_latchinit.at(l) == 2)
+				{
+					int gated_ffout = mkgate(aig_map[it.first], initstate_ff^1);
+					int gated_initin = mkgate(init_inputs[it.first], initstate_ff);
+					aig_map[it.first] = mkgate(gated_ffout^1, gated_initin^1)^1;
+				}
+			}
+		}
+
+		for (auto it : ff_map) {
+			int a = bit2aig(it.second);
+			int l = ordered_latches[it.first];
+			if (zinit_mode && aig_latchinit.at(l) == 1)
+				aig_latchin.push_back(a ^ 1);
+			else
+				aig_latchin.push_back(a);
+		}
+
+		if (!initstate_bits.empty() || !init_inputs.empty())
+			aig_latchin.push_back(1);
+
+		for (auto bit : output_bits) {
+			aig_o++;
+			ordered_outputs[bit] = aig_o-1;
+			aig_outputs.push_back(bit2aig(bit));
+		}
+
+		for (auto it : asserts) {
+			aig_b++;
+			int bit_a = bit2aig(it.first);
+			int bit_en = bit2aig(it.second);
+			aig_outputs.push_back(mkgate(bit_a^1, bit_en));
+		}
+
+		for (auto it : assumes) {
+			aig_c++;
+			int bit_a = bit2aig(it.first);
+			int bit_en = bit2aig(it.second);
+			aig_outputs.push_back(mkgate(bit_a^1, bit_en)^1);
+		}
+	}
+
+	void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode, bool symbols_mode)
+	{
+		log_assert(aig_m == aig_i + aig_l + aig_a);
+		log_assert(aig_l == GetSize(aig_latchin));
+		log_assert(aig_l == GetSize(aig_latchinit));
+		log_assert((aig_o + aig_b + aig_c) == GetSize(aig_outputs));
+
+		if (miter_mode) {
+			if (aig_b || aig_c)
+				log_error("Running AIGER back-end in -miter mode, but design contains $assert and/or $assume cells!\n");
+			f << stringf("%s %d %d %d 0 %d %d\n", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_a, aig_o);
+		} else {
+			f << stringf("%s %d %d %d %d %d", ascii_mode ? "aag" : "aig", aig_m, aig_i, aig_l, aig_o, aig_a);
+			if (aig_b || aig_c)
+				f << stringf(" %d %d", aig_b, aig_c);
+			f << stringf("\n");
+		}
+
+		if (ascii_mode)
+		{
+			for (int i = 0; i < aig_i; i++)
+				f << stringf("%d\n", 2*i+2);
+
+			for (int i = 0; i < aig_l; i++) {
+				if (zinit_mode || aig_latchinit.at(i) == 0)
+					f << stringf("%d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i));
+				else if (aig_latchinit.at(i) == 1)
+					f << stringf("%d %d 1\n", 2*(aig_i+i)+2, aig_latchin.at(i));
+				else if (aig_latchinit.at(i) == 2)
+					f << stringf("%d %d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i), 2*(aig_i+i)+2);
+			}
+
+			for (int i = 0; i < aig_o + aig_b + aig_c; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = 0; i < aig_a; i++)
+				f << stringf("%d %d %d\n", 2*(aig_i+aig_l+i)+2, aig_gates.at(i).first, aig_gates.at(i).second);
+		}
+		else
+		{
+			for (int i = 0; i < aig_l; i++) {
+				if (zinit_mode || aig_latchinit.at(i) == 0)
+					f << stringf("%d\n", aig_latchin.at(i));
+				else if (aig_latchinit.at(i) == 1)
+					f << stringf("%d 1\n", aig_latchin.at(i));
+				else if (aig_latchinit.at(i) == 2)
+					f << stringf("%d %d\n", aig_latchin.at(i), 2*(aig_i+i)+2);
+			}
+
+			for (int i = 0; i < aig_o + aig_b + aig_c; i++)
+				f << stringf("%d\n", aig_outputs.at(i));
+
+			for (int i = 0; i < aig_a; i++) {
+				int lhs = 2*(aig_i+aig_l+i)+2;
+				int rhs0 = aig_gates.at(i).first;
+				int rhs1 = aig_gates.at(i).second;
+				int delta0 = lhs - rhs0;
+				int delta1 = rhs0 - rhs1;
+				aiger_encode(f, delta0);
+				aiger_encode(f, delta1);
+			}
+		}
+
+		if (symbols_mode)
+		{
+			for (auto wire : module->wires())
+			{
+				if (wire->name[0] == '$')
+					continue;
+
+				SigSpec sig = sigmap(wire);
+
+				for (int i = 0; i < GetSize(wire); i++)
+				{
+					if (wire->port_input) {
+						int a = aig_map.at(sig[i]);
+						log_assert((a & 1) == 0);
+						if (GetSize(wire) != 1)
+							f << stringf("i%d %s[%d]\n", (a >> 1)-1, log_id(wire), i);
+						else
+							f << stringf("i%d %s\n", (a >> 1)-1, log_id(wire));
+					}
+
+					if (wire->port_output) {
+						int o = ordered_outputs.at(sig[i]);
+						if (GetSize(wire) != 1)
+							f << stringf("%c%d %s[%d]\n", miter_mode ? 'b' : 'o', o, log_id(wire), i);
+						else
+							f << stringf("%c%d %s\n", miter_mode ? 'b' : 'o', o, log_id(wire));
+					}
+
+					if (init_inputs.count(sig[i])) {
+						int a = init_inputs.at(sig[i]);
+						log_assert((a & 1) == 0);
+						if (GetSize(wire) != 1)
+							f << stringf("i%d init:%s[%d]\n", (a >> 1)-1, log_id(wire), i);
+						else
+							f << stringf("i%d init:%s\n", (a >> 1)-1, log_id(wire));
+					}
+
+					if (ordered_latches.count(sig[i])) {
+						int l = ordered_latches.at(sig[i]);
+						const char *p = (zinit_mode && (aig_latchinit.at(l) == 1)) ? "!" : "";
+						if (GetSize(wire) != 1)
+							f << stringf("l%d %s%s[%d]\n", l, p, log_id(wire), i);
+						else
+							f << stringf("l%d %s%s\n", l, p, log_id(wire));
+					}
+				}
+			}
+		}
+
+		f << stringf("c\nGenerated by %s\n", yosys_version_str);
+	}
+
+	void write_map(std::ostream &f, bool verbose_map)
+	{
+		dict<int, string> input_lines;
+		dict<int, string> init_lines;
+		dict<int, string> output_lines;
+		dict<int, string> latch_lines;
+		dict<int, string> wire_lines;
+
+		for (auto wire : module->wires())
+		{
+			if (!verbose_map && wire->name[0] == '$')
+				continue;
+
+			SigSpec sig = sigmap(wire);
+
+			for (int i = 0; i < GetSize(wire); i++)
+			{
+				if (aig_map.count(sig[i]) == 0)
+					continue;
+
+				int a = aig_map.at(sig[i]);
+
+				if (verbose_map)
+					wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire));
+
+				if (wire->port_input) {
+					log_assert((a & 1) == 0);
+					input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire));
+				}
+
+				if (wire->port_output) {
+					int o = ordered_outputs.at(sig[i]);
+					output_lines[o] += stringf("output %d %d %s\n", o, i, log_id(wire));
+				}
+
+				if (init_inputs.count(sig[i])) {
+					int a = init_inputs.at(sig[i]);
+					log_assert((a & 1) == 0);
+					init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, i, log_id(wire));
+				}
+
+				if (ordered_latches.count(sig[i])) {
+					int l = ordered_latches.at(sig[i]);
+					if (zinit_mode && (aig_latchinit.at(l) == 1))
+						latch_lines[l] += stringf("invlatch %d %d %s\n", l, i, log_id(wire));
+					else
+						latch_lines[l] += stringf("latch %d %d %s\n", l, i, log_id(wire));
+				}
+			}
+		}
+
+		input_lines.sort();
+		for (auto &it : input_lines)
+			f << it.second;
+
+		init_lines.sort();
+		for (auto &it : init_lines)
+			f << it.second;
+
+		output_lines.sort();
+		for (auto &it : output_lines)
+			f << it.second;
+
+		latch_lines.sort();
+		for (auto &it : latch_lines)
+			f << it.second;
+
+		wire_lines.sort();
+		for (auto &it : wire_lines)
+			f << it.second;
+	}
+};
+
+struct AigerBackend : public Backend {
+	AigerBackend() : Backend("aiger", "write design to AIGER file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_aiger [options] [filename]\n");
+		log("\n");
+		log("Write the current design to an AIGER file. The design must be flattened and\n");
+		log("must not contain any cell types except $_AND_, $_NOT_, simple FF types,\n");
+		log("$assert and $assume cells, and $initstate cells.\n");
+		log("\n");
+		log("$assert and $assume cells are converted to AIGER bad state properties and\n");
+		log("invariant constraints.\n");
+		log("\n");
+		log("    -ascii\n");
+		log("        write ASCII version of AGIER format\n");
+		log("\n");
+		log("    -zinit\n");
+		log("        convert FFs to zero-initialized FFs, adding additional inputs for\n");
+		log("        uninitialized FFs.\n");
+		log("\n");
+		log("    -miter\n");
+		log("        design outputs are AIGER bad state properties\n");
+		log("\n");
+		log("    -symbols\n");
+		log("        include a symbol table in the generated AIGER file\n");
+		log("\n");
+		log("    -map <filename>\n");
+		log("        write an extra file with port and latch symbols\n");
+		log("\n");
+		log("    -vmap <filename>\n");
+		log("        like -map, but more verbose\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		bool ascii_mode = false;
+		bool zinit_mode = false;
+		bool miter_mode = false;
+		bool symbols_mode = false;
+		bool verbose_map = false;
+		std::string map_filename;
+
+		log_header(design, "Executing AIGER backend.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-ascii") {
+				ascii_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-zinit") {
+				zinit_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-miter") {
+				miter_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-symbols") {
+				symbols_mode = true;
+				continue;
+			}
+			if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) {
+				map_filename = args[++argidx];
+				continue;
+			}
+			if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) {
+				map_filename = args[++argidx];
+				verbose_map = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		Module *top_module = design->top_module();
+
+		if (top_module == nullptr)
+			log_error("Can't find top module in current design!\n");
+
+		AigerWriter writer(top_module, zinit_mode);
+		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
+
+		if (!map_filename.empty()) {
+			std::ofstream mapf;
+			mapf.open(map_filename.c_str(), std::ofstream::trunc);
+			if (mapf.fail())
+				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
+			writer.write_map(mapf, verbose_map);
+		}
+	}
+} AigerBackend;
+
+PRIVATE_NAMESPACE_END

backends/blif/blif.cc

@@ -112,7 +112,7 @@ struct BlifDumper
 				str[i] = '?';
 
 		if (sig.wire->width != 1)
-			str += stringf("[%d]", sig.offset);
+			str += stringf("[%d]", sig.wire->upto ? sig.wire->start_offset+sig.wire->width-sig.offset-1 : sig.wire->start_offset+sig.offset);
 
 		cstr_buf.push_back(str);
 		return cstr_buf.back().c_str();

backends/firrtl/.gitignore

@@ -0,0 +1,2 @@
+test.fir
+test_out.v

backends/firrtl/Makefile.inc

@@ -0,0 +1,3 @@
+
+OBJS += backends/firrtl/firrtl.o
+

backends/firrtl/firrtl.cc

@@ -0,0 +1,470 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  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
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include <string>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+pool<string> used_names;
+dict<IdString, string> namecache;
+int autoid_counter;
+
+string next_id()
+{
+	string new_id;
+
+	while (1) {
+		new_id = stringf("_%d", autoid_counter++);
+		if (used_names.count(new_id) == 0) break;
+	}
+
+	used_names.insert(new_id);
+	return new_id;
+}
+
+const char *make_id(IdString id)
+{
+	if (namecache.count(id) != 0)
+		return namecache.at(id).c_str();
+
+	string new_id = log_id(id);
+
+	for (int i = 0; i < GetSize(new_id); i++)
+	{
+		char &ch = new_id[i];
+		if ('a' <= ch && ch <= 'z') continue;
+		if ('A' <= ch && ch <= 'Z') continue;
+		if ('0' <= ch && ch <= '9' && i != 0) continue;
+		if ('_' == ch) continue;
+		ch = '_';
+	}
+
+	while (used_names.count(new_id) != 0)
+		new_id += '_';
+
+	namecache[id] = new_id;
+	used_names.insert(new_id);
+	return namecache.at(id).c_str();
+}
+
+struct FirrtlWorker
+{
+	Module *module;
+	std::ostream &f;
+
+	dict<SigBit, pair<string, int>> reverse_wire_map;
+	string unconn_id;
+
+	void register_reverse_wire_map(string id, SigSpec sig)
+	{
+		for (int i = 0; i < GetSize(sig); i++)
+			reverse_wire_map[sig[i]] = make_pair(id, i);
+	}
+
+	FirrtlWorker(Module *module, std::ostream &f) : module(module), f(f)
+	{
+	}
+
+	string make_expr(SigSpec sig)
+	{
+		string expr;
+
+		for (auto chunk : sig.chunks())
+		{
+			string new_expr;
+
+			if (chunk.wire == nullptr)
+			{
+				std::vector<RTLIL::State> bits = chunk.data;
+				new_expr = stringf("UInt<%d>(\"h", GetSize(bits));
+
+				while (GetSize(bits) % 4 != 0)
+					bits.push_back(State::S0);
+
+				for (int i = GetSize(bits)-4; i >= 0; i -= 4)
+				{
+					int val = 0;
+					if (bits[i+0] == State::S1) val += 1;
+					if (bits[i+1] == State::S1) val += 2;
+					if (bits[i+2] == State::S1) val += 4;
+					if (bits[i+3] == State::S1) val += 8;
+					new_expr.push_back(val < 10 ? '0' + val : 'a' + val - 10);
+				}
+
+				new_expr += "\")";
+			}
+			else if (chunk.offset == 0 && chunk.width == chunk.wire->width)
+			{
+				new_expr = make_id(chunk.wire->name);
+			}
+			else
+			{
+				string wire_id = make_id(chunk.wire->name);
+				new_expr = stringf("bits(%s, %d, %d)", wire_id.c_str(), chunk.offset + chunk.width - 1, chunk.offset);
+			}
+
+			if (expr.empty())
+				expr = new_expr;
+			else
+				expr = "cat(" + new_expr + ", " + expr + ")";
+		}
+
+		return expr;
+	}
+
+	void run()
+	{
+		f << stringf("  module %s:\n", make_id(module->name));
+		vector<string> port_decls, wire_decls, cell_exprs, wire_exprs;
+
+		for (auto wire : module->wires())
+		{
+			if (wire->port_id)
+			{
+				if (wire->port_input && wire->port_output)
+					log_error("Module port %s.%s is inout!\n", log_id(module), log_id(wire));
+				port_decls.push_back(stringf("    %s %s: UInt<%d>\n", wire->port_input ? "input" : "output",
+						make_id(wire->name), wire->width));
+			}
+			else
+			{
+				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", make_id(wire->name), wire->width));
+			}
+		}
+
+		for (auto cell : module->cells())
+		{
+			if (cell->type.in("$add", "$sub", "$xor"))
+			{
+				string y_id = make_id(cell->name);
+				bool is_signed = cell->parameters.at("\\A_SIGNED").as_bool();
+				int y_width =  cell->parameters.at("\\Y_WIDTH").as_int();
+				string a_expr = make_expr(cell->getPort("\\A"));
+				string b_expr = make_expr(cell->getPort("\\B"));
+				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+
+				if (is_signed) {
+					a_expr = "asSInt(" + a_expr + ")";
+					b_expr = "asSInt(" + b_expr + ")";
+				}
+
+				a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+				b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
+
+				string primop;
+				if (cell->type == "$add") primop = "add";
+				if (cell->type == "$sub") primop = "sub";
+				if (cell->type == "$xor") primop = "xor";
+
+				string expr = stringf("%s(%s, %s)", primop.c_str(), a_expr.c_str(), b_expr.c_str());
+
+				if ((is_signed && !cell->type.in("$xor")) || cell->type.in("$sub"))
+					expr = stringf("asUInt(%s)", expr.c_str());
+
+				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
+				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+
+				continue;
+			}
+
+			if (cell->type.in("$mux"))
+			{
+				string y_id = make_id(cell->name);
+				int width = cell->parameters.at("\\WIDTH").as_int();
+				string a_expr = make_expr(cell->getPort("\\A"));
+				string b_expr = make_expr(cell->getPort("\\B"));
+				string s_expr = make_expr(cell->getPort("\\S"));
+				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), width));
+
+				string expr = stringf("mux(%s, %s, %s)", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
+
+				cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
+				register_reverse_wire_map(y_id, cell->getPort("\\Y"));
+
+				continue;
+			}
+
+			if (cell->type.in("$mem"))
+			{
+				string mem_id = make_id(cell->name);
+				int abits = cell->parameters.at("\\ABITS").as_int();
+				int width = cell->parameters.at("\\WIDTH").as_int();
+				int size = cell->parameters.at("\\SIZE").as_int();
+				int rd_ports = cell->parameters.at("\\RD_PORTS").as_int();
+				int wr_ports = cell->parameters.at("\\WR_PORTS").as_int();
+
+				Const initdata = cell->parameters.at("\\INIT");
+				for (State bit : initdata.bits)
+					if (bit != State::Sx)
+						log_error("Memory with initialization data: %s.%s\n", log_id(module), log_id(cell));
+
+				Const rd_clk_enable = cell->parameters.at("\\RD_CLK_ENABLE");
+				Const wr_clk_enable = cell->parameters.at("\\WR_CLK_ENABLE");
+				Const wr_clk_polarity = cell->parameters.at("\\WR_CLK_POLARITY");
+
+				int offset = cell->parameters.at("\\OFFSET").as_int();
+				if (offset != 0)
+					log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
+
+				cell_exprs.push_back(stringf("    mem %s:\n", mem_id.c_str()));
+				cell_exprs.push_back(stringf("      data-type => UInt<%d>\n", width));
+				cell_exprs.push_back(stringf("      depth => %d\n", size));
+
+				for (int i = 0; i < rd_ports; i++)
+					cell_exprs.push_back(stringf("      reader => r%d\n", i));
+
+				for (int i = 0; i < wr_ports; i++)
+					cell_exprs.push_back(stringf("      writer => w%d\n", i));
+
+				cell_exprs.push_back(stringf("      read-latency => 0\n"));
+				cell_exprs.push_back(stringf("      write-latency => 1\n"));
+				cell_exprs.push_back(stringf("      read-under-write => undefined\n"));
+
+				for (int i = 0; i < rd_ports; i++)
+				{
+					if (rd_clk_enable[i] != State::S0)
+						log_error("Clocked read port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
+
+					SigSpec data_sig = cell->getPort("\\RD_DATA").extract(i*width, width);
+					string addr_expr = make_expr(cell->getPort("\\RD_ADDR").extract(i*abits, abits));
+
+					cell_exprs.push_back(stringf("    %s.r%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
+					cell_exprs.push_back(stringf("    %s.r%d.en <= UInt<1>(1)\n", mem_id.c_str(), i));
+					cell_exprs.push_back(stringf("    %s.r%d.clk <= asClock(UInt<1>(0))\n", mem_id.c_str(), i));
+
+					register_reverse_wire_map(stringf("%s.r%d.data", mem_id.c_str(), i), data_sig);
+				}
+
+				for (int i = 0; i < wr_ports; i++)
+				{
+					if (wr_clk_enable[i] != State::S1)
+						log_error("Unclocked write port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
+
+					if (wr_clk_polarity[i] != State::S1)
+						log_error("Negedge write port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
+
+					string addr_expr = make_expr(cell->getPort("\\WR_ADDR").extract(i*abits, abits));
+					string data_expr = make_expr(cell->getPort("\\WR_DATA").extract(i*width, width));
+					string clk_expr = make_expr(cell->getPort("\\WR_CLK").extract(i));
+
+					SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
+					string wen_expr = make_expr(wen_sig[0]);
+
+					for (int i = 1; i < GetSize(wen_sig); i++)
+						if (wen_sig[0] != wen_sig[i])
+							log_error("Complex write enable on port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
+
+					cell_exprs.push_back(stringf("    %s.w%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
+					cell_exprs.push_back(stringf("    %s.w%d.data <= %s\n", mem_id.c_str(), i, data_expr.c_str()));
+					cell_exprs.push_back(stringf("    %s.w%d.en <= %s\n", mem_id.c_str(), i, wen_expr.c_str()));
+					cell_exprs.push_back(stringf("    %s.w%d.mask <= UInt<1>(1)\n", mem_id.c_str(), i));
+					cell_exprs.push_back(stringf("    %s.w%d.clk <= asClock(%s)\n", mem_id.c_str(), i, clk_expr.c_str()));
+				}
+
+				continue;
+			}
+
+			if (cell->type.in("$dff"))
+			{
+				bool clkpol = cell->parameters.at("\\CLK_POLARITY").as_bool();
+				if (clkpol == false)
+					log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
+
+				string q_id = make_id(cell->name);
+				int width = cell->parameters.at("\\WIDTH").as_int();
+				string expr = make_expr(cell->getPort("\\D"));
+				string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
+
+				wire_decls.push_back(stringf("    reg %s: UInt<%d>, %s\n", q_id.c_str(), width, clk_expr.c_str()));
+
+				cell_exprs.push_back(stringf("    %s <= %s\n", q_id.c_str(), expr.c_str()));
+				register_reverse_wire_map(q_id, cell->getPort("\\Q"));
+
+				continue;
+			}
+
+			log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
+		}
+
+		for (auto conn : module->connections())
+		{
+			string y_id = next_id();
+			int y_width =  GetSize(conn.first);
+			string expr = make_expr(conn.second);
+
+			wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", y_id.c_str(), y_width));
+			cell_exprs.push_back(stringf("    %s <= %s\n", y_id.c_str(), expr.c_str()));
+			register_reverse_wire_map(y_id, conn.first);
+		}
+
+		for (auto wire : module->wires())
+		{
+			string expr;
+
+			if (wire->port_input)
+				continue;
+
+			int cursor = 0;
+			bool is_valid = false;
+			bool make_unconn_id = false;
+
+			while (cursor < wire->width)
+			{
+				int chunk_width = 1;
+				string new_expr;
+
+				SigBit start_bit(wire, cursor);
+
+				if (reverse_wire_map.count(start_bit))
+				{
+					pair<string, int> start_map = reverse_wire_map.at(start_bit);
+
+					while (cursor+chunk_width < wire->width)
+					{
+						SigBit stop_bit(wire, cursor+chunk_width);
+
+						if (reverse_wire_map.count(stop_bit) == 0)
+							break;
+
+						pair<string, int> stop_map = reverse_wire_map.at(stop_bit);
+						stop_map.second -= chunk_width;
+
+						if (start_map != stop_map)
+							break;
+
+						chunk_width++;
+					}
+
+					new_expr = stringf("bits(%s, %d, %d)", start_map.first.c_str(),
+							start_map.second + chunk_width - 1, start_map.second);
+					is_valid = true;
+				}
+				else
+				{
+					if (unconn_id.empty()) {
+						unconn_id = next_id();
+						make_unconn_id = true;
+					}
+					new_expr = unconn_id;
+				}
+
+				if (expr.empty())
+					expr = new_expr;
+				else
+					expr = "cat(" + new_expr + ", " + expr + ")";
+
+				cursor += chunk_width;
+			}
+
+			if (is_valid) {
+				if (make_unconn_id) {
+					wire_decls.push_back(stringf("    wire %s: UInt<1>\n", unconn_id.c_str()));
+					cell_exprs.push_back(stringf("    %s is invalid\n", unconn_id.c_str()));
+				}
+				wire_exprs.push_back(stringf("    %s <= %s\n", make_id(wire->name), expr.c_str()));
+			} else {
+				if (make_unconn_id) {
+					unconn_id.clear();
+				}
+				wire_exprs.push_back(stringf("    %s is invalid\n", make_id(wire->name)));
+			}
+		}
+
+		for (auto str : port_decls)
+			f << str;
+
+		f << stringf("\n");
+
+		for (auto str : wire_decls)
+			f << str;
+
+		f << stringf("\n");
+
+		for (auto str : cell_exprs)
+			f << str;
+
+		f << stringf("\n");
+
+		for (auto str : wire_exprs)
+			f << str;
+	}
+};
+
+struct FirrtlBackend : public Backend {
+	FirrtlBackend() : Backend("firrtl", "write design to a FIRRTL file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_firrtl [options] [filename]\n");
+		log("\n");
+		log("Write a FIRRTL netlist of the current design.\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			// if (args[argidx] == "-aig") {
+			// 	aig_mode = true;
+			// 	continue;
+			// }
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		log_header(design, "Executing FIRRTL backend.\n");
+
+		Module *top = design->top_module();
+
+		if (top == nullptr)
+			log_error("No top module found!\n");
+
+		namecache.clear();
+		autoid_counter = 0;
+
+		for (auto module : design->modules()) {
+			make_id(module->name);
+			for (auto wire : module->wires())
+				if (wire->port_id)
+					make_id(wire->name);
+		}
+
+		*f << stringf("circuit %s:\n", make_id(top->name));
+
+		for (auto module : design->modules())
+		{
+			FirrtlWorker worker(module, *f);
+			worker.run();
+		}
+
+		namecache.clear();
+		autoid_counter = 0;
+	}
+} FirrtlBackend;
+
+PRIVATE_NAMESPACE_END

backends/firrtl/test.sh

@@ -0,0 +1,22 @@
+#!/bin/bash
+set -ex
+
+../../yosys -p 'prep -nordff; write_firrtl test.fir' test.v
+
+firrtl -i test.fir -o test_out.v
+
+../../yosys -p '
+	read_verilog test.v
+	rename test gold
+
+	read_verilog test_out.v
+	rename test gate
+
+	prep
+	memory_map
+	miter -equiv -flatten gold gate miter
+	hierarchy -top miter
+
+	sat -verify -prove trigger 0 -set-init-zero -seq 10 miter
+'
+

backends/firrtl/test.v

@@ -0,0 +1,24 @@
+module test(
+	input clk, wen,
+	input [4:0] waddr, raddr,
+	input [31:0] wdata,
+	output reg [31:0] rdata,
+	signed input [7:0] a, b, x,
+	output [15:0] s, d, y, z, u, q
+);
+	reg [31:0] memory [0:31];
+
+	always @(posedge clk) begin
+		rdata <= memory[raddr];
+		if (wen) memory[waddr] <= wdata;
+	end
+
+	assign s = a+{b[6:2], 2'b1};
+	assign d = a-b;
+	assign y = x;
+	assign z[7:0] = s+d;
+	assign z[15:8] = s-d;
+
+	always @(posedge clk)
+		q <= s ^ d ^ x;
+endmodule

backends/json/json.cc

@@ -333,6 +333,10 @@ struct JsonBackend : public Backend {
 		log("connected to a constant driver are denoted as string \"0\" or \"1\" instead of\n");
 		log("a number.\n");
 		log("\n");
+		log("Numeric parameter and attribute values up to 32 bits are written as decimal\n");
+		log("values. Numbers larger than that are written as string holding the binary\n");
+		log("representation of the value.\n");
+		log("\n");
 		log("For example the following Verilog code:\n");
 		log("\n");
 		log("    module test(input x, y);\n");

backends/smt2/smt2.cc

@@ -639,12 +639,24 @@ struct Smt2Worker
 			if (wire->attributes.count("\\init")) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				Const val = wire->attributes.at("\\init");
-				val.bits.resize(GetSize(sig));
+				val.bits.resize(GetSize(sig), State::Sx);
 				if (bvmode && GetSize(sig) > 1) {
-					init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
+					Const mask(State::S1, GetSize(sig));
+					bool use_mask = false;
+					for (int i = 0; i < GetSize(sig); i++)
+						if (val[i] != State::S0 && val[i] != State::S1) {
+							val[i] = State::S0;
+							mask[i] = State::S0;
+							use_mask = true;
+						}
+					if (use_mask)
+						init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire)));
+					else
+						init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire)));
 				} else {
 					for (int i = 0; i < GetSize(sig); i++)
-						init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire)));
+						if (val[i] == State::S0 || val[i] == State::S1)
+							init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire)));
 				}
 			}
 
@@ -749,6 +761,10 @@ struct Smt2Worker
 
 		if (verbose) log("=> export logic driving hierarchical cells\n");
 
+		for (auto cell : module->cells())
+			if (module->design->module(cell->type) != nullptr)
+				export_cell(cell);
+
 		while (!hiercells_queue.empty())
 		{
 			std::set<RTLIL::Cell*> queue;

backends/smt2/smtbmc.py

@@ -22,11 +22,16 @@ import os, sys, getopt, re
 from smtio import SmtIo, SmtOpts, MkVcd
 from collections import defaultdict
 
+got_topt = False
 skip_steps = 0
 step_size = 1
 num_steps = 20
+append_steps = 0
 vcdfile = None
 cexfile = None
+aimfile = None
+aiwfile = None
+aigheader = True
 vlogtbfile = None
 inconstr = list()
 outconstr = None
@@ -65,6 +70,19 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --cex <cex_filename>
         read cex file as written by ABC's "write_cex -n"
 
+    --aig <prefix>
+        read AIGER map file (as written by Yosys' "write_aiger -map")
+        and AIGER witness file. The file names are <prefix>.aim for
+        the map file and <prefix>.aiw for the witness file.
+
+    --aig <aim_filename>:<aiw_filename>
+        like above, but for map files and witness files that do not
+        share a filename prefix (or use differen file extensions).
+
+    --aig-noheader
+        the AIGER witness file does not include the status and
+        properties lines.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -92,18 +110,25 @@ yosys-smtbmc [options] <yosys_smt2_output>
         when using -g or -i, create a dump file for each
         step. The character '%' is replaces in all dump
         filenames with the step number.
+
+    --append <num_steps>
+        add <num_steps> time steps at the end of the trace
+        when creating a counter example (this additional time
+        steps will still be constrained by assumtions)
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
+             "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="])
 except:
     usage()
 
 for o, a in opts:
     if o == "-t":
+        got_topt = True
         a = a.split(":")
         if len(a) == 1:
             num_steps = int(a[0])
@@ -115,7 +140,7 @@ for o, a in opts:
             step_size = int(a[1])
             num_steps = int(a[2])
         else:
-            assert 0
+            assert False
     elif o == "--assume-skipped":
         assume_skipped = int(a)
     elif o == "--final-only":
@@ -124,6 +149,14 @@ for o, a in opts:
         inconstr.append(a)
     elif o == "--cex":
         cexfile = a
+    elif o == "--aig":
+        if ":" in a:
+            aimfile, aiwfile = a.split(":")
+        else:
+            aimfile = a + ".aim"
+            aiwfile = a + ".aiw"
+    elif o == "--aig-noheader":
+        aigheader = False
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -134,6 +167,8 @@ for o, a in opts:
         dumpall = True
     elif o == "--noinfo":
         noinfo = True
+    elif o == "--append":
+        append_steps = int(a)
     elif o == "-i":
         tempind = True
     elif o == "-g":
@@ -182,12 +217,11 @@ for fn in inconstr:
                     current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
                     constr_final_start = 0
                 elif len(tokens) == 2:
-                    i = int(tokens[1])
-                    assert i < 0
-                    current_states = set(["final-%d" % i for i in range(-i, num_steps+1)])
-                    constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i)
+                    arg = abs(int(tokens[1]))
+                    current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
+                    constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
                 else:
-                    assert 0
+                    assert False
                 continue
 
             if tokens[0] == "state":
@@ -206,18 +240,17 @@ for fn in inconstr:
                             for i in range(lower, upper+1):
                                 current_states.add(i)
                         else:
-                            assert 0
+                            assert False
                 continue
 
             if tokens[0] == "always":
                 if len(tokens) == 1:
                     current_states = set(range(0, num_steps+1))
                 elif len(tokens) == 2:
-                    i = int(tokens[1])
-                    assert i < 0
-                    current_states = set(range(-i, num_steps+1))
+                    arg = abs(int(tokens[1]))
+                    current_states = set(range(arg, num_steps+1))
                 else:
-                    assert 0
+                    assert False
                 continue
 
             if tokens[0] == "assert":
@@ -244,7 +277,7 @@ for fn in inconstr:
                 so.logic = " ".join(tokens[1:])
                 continue
 
-            assert 0
+            assert False
 
 
 def get_constr_expr(db, state, final=False, getvalues=False):
@@ -318,6 +351,11 @@ assert topmod is not None
 assert topmod in smt.modinfo
 
 if cexfile is not None:
+    if not got_topt:
+        assume_skipped = 0
+        skip_steps = 0
+        num_steps = 0
+
     with open(cexfile, "r") as f:
         cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
         for entry in f.read().split():
@@ -349,6 +387,144 @@ if cexfile is not None:
             # print("cex@%d: %s" % (step, smtexpr))
             constr_assumes[step].append((cexfile, smtexpr))
 
+            if not got_topt:
+                skip_steps = max(skip_steps, step)
+                num_steps = max(num_steps, step+1)
+
+if aimfile is not None:
+    input_map = dict()
+    init_map = dict()
+    latch_map = dict()
+
+    if not got_topt:
+        assume_skipped = 0
+        skip_steps = 0
+        num_steps = 0
+
+    with open(aimfile, "r") as f:
+        for entry in f.read().splitlines():
+            entry = entry.split()
+
+            if entry[0] == "input":
+                input_map[int(entry[1])] = (entry[3], int(entry[2]))
+                continue
+
+            if entry[0] == "init":
+                init_map[int(entry[1])] = (entry[3], int(entry[2]))
+                continue
+
+            if entry[0] in ["latch", "invlatch"]:
+                latch_map[int(entry[1])] = (entry[3], int(entry[2]), entry[0] == "invlatch")
+                continue
+
+            if entry[0] in ["output", "wire"]:
+                continue
+
+            assert False
+
+    with open(aiwfile, "r") as f:
+        got_state = False
+        got_ffinit = False
+        step = 0
+
+        if not aigheader:
+            got_state = True
+
+        for entry in f.read().splitlines():
+            if len(entry) == 0 or entry[0] in "bcjfu.":
+                continue
+
+            if not got_state:
+                got_state = True
+                assert entry == "1"
+                continue
+
+            if not got_ffinit:
+                got_ffinit = True
+                if len(init_map) == 0:
+                    for i in range(len(entry)):
+                        if entry[i] == "x":
+                            continue
+
+                        if i in latch_map:
+                            value = int(entry[i])
+                            name = latch_map[i][0]
+                            bitidx = latch_map[i][1]
+                            invert = latch_map[i][2]
+
+                            if invert:
+                                value = 1 - value
+
+                            path = smt.get_path(topmod, name)
+                            width = smt.net_width(topmod, path)
+
+                            if width == 1:
+                                assert bitidx == 0
+                                smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                            else:
+                                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+
+                            constr_assumes[0].append((cexfile, smtexpr))
+                continue
+
+            for i in range(len(entry)):
+                if entry[i] == "x":
+                    continue
+
+                if (step == 0) and (i in init_map):
+                    value = int(entry[i])
+                    name = init_map[i][0]
+                    bitidx = init_map[i][1]
+
+                    path = smt.get_path(topmod, name)
+
+                    if not smt.net_exists(topmod, path):
+                        match = re.match(r"(.*)\[(\d+)\]$", path[-1])
+                        if match:
+                            path[-1] = match.group(1)
+                            addr = int(match.group(2))
+
+                        if not match or not smt.mem_exists(topmod, path):
+                            print_msg("Ignoring init value for unknown net: %s" % (name))
+                            continue
+
+                        meminfo = smt.mem_info(topmod, path)
+                        smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
+                        width = meminfo[1]
+
+                    else:
+                        smtexpr = "[%s]" % name
+                        width = smt.net_width(topmod, path)
+
+                    if width == 1:
+                        assert bitidx == 0
+                        smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
+                    else:
+                        smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
+
+                    constr_assumes[0].append((cexfile, smtexpr))
+
+                if i in input_map:
+                    value = int(entry[i])
+                    name = input_map[i][0]
+                    bitidx = input_map[i][1]
+
+                    path = smt.get_path(topmod, name)
+                    width = smt.net_width(topmod, path)
+
+                    if width == 1:
+                        assert bitidx == 0
+                        smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                    else:
+                        smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+
+                    constr_assumes[step].append((cexfile, smtexpr))
+
+            if not got_topt:
+                skip_steps = max(skip_steps, step)
+                num_steps = max(num_steps, step+1)
+            step += 1
+
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
     print_msg("Writing trace to VCD file: %s" % (filename))
@@ -429,7 +605,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
@@ -490,7 +666,7 @@ def write_constr_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
@@ -649,6 +825,7 @@ else:  # not tempind
         for i in range(1, step_size):
             if step+i < num_steps:
                 smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod))
+                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i))
                 smt.write("(assert (|%s_u| s%d))" % (topmod, step+i))
                 smt.write("(assert (|%s_h| s%d))" % (topmod, step+i))
                 smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i))
@@ -668,10 +845,21 @@ else:  # not tempind
 
                 if smt.check_sat() == "sat":
                     print("%s BMC failed!" % smt.timestamp())
+                    if append_steps > 0:
+                        for i in range(last_check_step+1, last_check_step+1+append_steps):
+                            print_msg("Appending additional step %d." % i)
+                            smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod))
+                            smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i))
+                            smt.write("(assert (|%s_u| s%d))" % (topmod, i))
+                            smt.write("(assert (|%s_h| s%d))" % (topmod, i))
+                            smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i))
+                            smt.write("(assert %s)" % get_constr_expr(constr_assumes, i))
+                        print_msg("Re-solving with appended steps..")
+                        assert smt.check_sat() == "sat"
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
-                    write_trace(0, last_check_step+1, '%')
+                    write_trace(0, last_check_step+1+append_steps, '%')
                     retstatus = False
                     break
 

backends/smt2/smtio.py

@@ -1,4 +1,3 @@
-#!/usr/bin/env python3
 #
 # yosys -- Yosys Open SYnthesis Suite
 #
@@ -17,7 +16,7 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import sys, subprocess, re
+import sys, subprocess, re, os
 from copy import deepcopy
 from select import select
 from time import time
@@ -74,7 +73,7 @@ class SmtIo:
             self.debug_print = False
             self.debug_file = None
             self.dummy_file = None
-            self.timeinfo = True
+            self.timeinfo = os.name != "nt"
             self.unroll = False
             self.noincr = False
             self.info_stmts = list()
@@ -568,6 +567,26 @@ class SmtIo:
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
+    def net_exists(self, mod, net_path):
+        for i in range(len(net_path)-1):
+            if mod not in self.modinfo: return False
+            if net_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[net_path[i]]
+
+        if mod not in self.modinfo: return False
+        if net_path[-1] not in self.modinfo[mod].wsize: return False
+        return True
+
+    def mem_exists(self, mod, mem_path):
+        for i in range(len(mem_path)-1):
+            if mod not in self.modinfo: return False
+            if mem_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[mem_path[i]]
+
+        if mod not in self.modinfo: return False
+        if mem_path[-1] not in self.modinfo[mod].memories: return False
+        return True
+
     def mem_expr(self, mod, base, path, portidx=None, infomode=False):
         if len(path) == 1:
             assert mod in self.modinfo
@@ -583,8 +602,8 @@ class SmtIo:
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
         return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
 
-    def mem_info(self, mod, base, path):
-        return self.mem_expr(mod, base, path, infomode=True)
+    def mem_info(self, mod, path):
+        return self.mem_expr(mod, "", path, infomode=True)
 
     def get_net(self, mod_name, net_path, state_name):
         return self.get(self.net_expr(mod_name, state_name, net_path))
@@ -619,7 +638,7 @@ class SmtOpts:
         self.dummy_file = None
         self.unroll = False
         self.noincr = False
-        self.timeinfo = True
+        self.timeinfo = os.name != "nt"
         self.logic = None
         self.info_stmts = list()
         self.nocomments = False
@@ -634,7 +653,7 @@ class SmtOpts:
         elif o == "--noincr":
             self.noincr = True
         elif o == "--noprogress":
-            self.timeinfo = True
+            self.timeinfo = False
         elif o == "--dump-smt2":
             self.debug_file = open(a, "w")
         elif o == "--logic":
@@ -674,6 +693,7 @@ class SmtOpts:
 
     --noprogress
         disable timer display during solving
+        (this option is set implicitly on Windows)
 
     --dump-smt2 <filename>
         write smt2 statements to file

backends/verilog/verilog_backend.cc

@@ -33,13 +33,15 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nostr, defparam;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam;
 int auto_name_counter, auto_name_offset, auto_name_digits;
 std::map<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires, reg_ct;
 std::string auto_prefix;
 
 RTLIL::Module *active_module;
+dict<RTLIL::SigBit, RTLIL::State> active_initdata;
+SigMap active_sigmap;
 
 void reset_auto_counter_id(RTLIL::IdString id, bool may_rename)
 {
@@ -159,14 +161,14 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 	if (width < 0)
 		width = data.bits.size() - offset;
 	if (nostr)
-		goto dump_bits;
+		goto dump_hex;
 	if ((data.flags & RTLIL::CONST_FLAG_STRING) == 0 || width != (int)data.bits.size()) {
 		if (width == 32 && !no_decimal && !nodec) {
 			int32_t val = 0;
 			for (int i = offset+width-1; i >= offset; i--) {
 				log_assert(i < (int)data.bits.size());
 				if (data.bits[i] != RTLIL::S0 && data.bits[i] != RTLIL::S1)
-					goto dump_bits;
+					goto dump_hex;
 				if (data.bits[i] == RTLIL::S1)
 					val |= 1 << (i - offset);
 			}
@@ -175,7 +177,55 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 			else
 				f << stringf("32'%sd%u", set_signed ? "s" : "", val);
 		} else {
-	dump_bits:
+	dump_hex:
+			if (nohex)
+				goto dump_bin;
+			vector<char> bin_digits, hex_digits;
+			for (int i = offset; i < offset+width; i++) {
+				log_assert(i < (int)data.bits.size());
+				switch (data.bits[i]) {
+				case RTLIL::S0: bin_digits.push_back('0'); break;
+				case RTLIL::S1: bin_digits.push_back('1'); break;
+				case RTLIL::Sx: bin_digits.push_back('x'); break;
+				case RTLIL::Sz: bin_digits.push_back('z'); break;
+				case RTLIL::Sa: bin_digits.push_back('z'); break;
+				case RTLIL::Sm: log_error("Found marker state in final netlist.");
+				}
+			}
+			if (GetSize(bin_digits) == 0)
+				goto dump_bin;
+			while (GetSize(bin_digits) % 4 != 0)
+				if (bin_digits.back() == '1')
+					bin_digits.push_back('0');
+				else
+					bin_digits.push_back(bin_digits.back());
+			for (int i = 0; i < GetSize(bin_digits); i += 4)
+			{
+				char bit_3 = bin_digits[i+3];
+				char bit_2 = bin_digits[i+2];
+				char bit_1 = bin_digits[i+1];
+				char bit_0 = bin_digits[i+0];
+				if (bit_3 == 'x' || bit_2 == 'x' || bit_1 == 'x' || bit_0 == 'x') {
+					if (bit_3 != 'x' || bit_2 != 'x' || bit_1 != 'x' || bit_0 != 'x')
+						goto dump_bin;
+					hex_digits.push_back('x');
+					continue;
+				}
+				if (bit_3 == 'z' || bit_2 == 'z' || bit_1 == 'z' || bit_0 == 'z') {
+					if (bit_3 != 'z' || bit_2 != 'z' || bit_1 != 'z' || bit_0 != 'z')
+						goto dump_bin;
+					hex_digits.push_back('z');
+					continue;
+				}
+				int val = 8*(bit_3 - '0') + 4*(bit_2 - '0') + 2*(bit_1 - '0') + (bit_0 - '0');
+				hex_digits.push_back(val < 10 ? '0' + val : 'a' + val - 10);
+			}
+			f << stringf("%d'%sh", width, set_signed ? "s" : "");
+			for (int i = GetSize(hex_digits)-1; i >= 0; i--)
+				f << hex_digits[i];
+		}
+		if (0) {
+	dump_bin:
 			f << stringf("%d'%sb", width, set_signed ? "s" : "");
 			if (width == 0)
 				f << stringf("0");
@@ -214,6 +264,26 @@ void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int o
 	}
 }
 
+void dump_reg_init(std::ostream &f, SigSpec sig)
+{
+	Const initval;
+	bool gotinit = false;
+
+	for (auto bit : active_sigmap(sig)) {
+		if (active_initdata.count(bit)) {
+			initval.bits.push_back(active_initdata.at(bit));
+			gotinit = true;
+		} else {
+			initval.bits.push_back(State::Sx);
+		}
+	}
+
+	if (gotinit) {
+		f << " = ";
+		dump_const(f, initval);
+	}
+}
+
 void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool no_decimal = false)
 {
 	if (chunk.wire == NULL) {
@@ -302,12 +372,12 @@ void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
 	if (wire->port_input && wire->port_output)
 		f << stringf("%s" "inout%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
 	if (reg_wires.count(wire->name)) {
-		f << stringf("%s" "reg%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
+		f << stringf("%s" "reg%s %s", indent.c_str(), range.c_str(), id(wire->name).c_str());
 		if (wire->attributes.count("\\init")) {
-			f << stringf("%s" "initial %s = ", indent.c_str(), id(wire->name).c_str());
+			f << stringf(" = ");
 			dump_const(f, wire->attributes.at("\\init"));
-			f << stringf(";\n");
 		}
+		f << stringf(";\n");
 	} else if (!wire->port_input && !wire->port_output)
 		f << stringf("%s" "wire%s %s;\n", indent.c_str(), range.c_str(), id(wire->name).c_str());
 #endif
@@ -474,8 +544,11 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
 
-		if (!out_is_reg_wire)
-			f << stringf("%s" "reg %s;\n", indent.c_str(), reg_name.c_str());
+		if (!out_is_reg_wire) {
+			f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str());
+			dump_reg_init(f, cell->getPort("\\Q"));
+			f << ";\n";
+		}
 
 		dump_attributes(f, indent, cell->attributes);
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), cell->type[6] == 'P' ? "pos" : "neg");
@@ -514,8 +587,11 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
 
-		if (!out_is_reg_wire)
-			f << stringf("%s" "reg %s;\n", indent.c_str(), reg_name.c_str());
+		if (!out_is_reg_wire) {
+			f << stringf("%s" "reg %s", indent.c_str(), reg_name.c_str());
+			dump_reg_init(f, cell->getPort("\\Q"));
+			f << ";\n";
+		}
 
 		dump_attributes(f, indent, cell->attributes);
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_c == 'P' ? "pos" : "neg");
@@ -698,8 +774,11 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(sig_q, reg_name);
 
-		if (!out_is_reg_wire)
-			f << stringf("%s" "reg [%d:0] %s;\n", indent.c_str(), width-1, reg_name.c_str());
+		if (!out_is_reg_wire) {
+			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), width-1, reg_name.c_str());
+			dump_reg_init(f, sig_q);
+			f << ";\n";
+		}
 
 		for (int i = 0; i < width; i++) {
 			f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_clk ? "pos" : "neg");
@@ -754,8 +833,11 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		std::string reg_name = cellname(cell);
 		bool out_is_reg_wire = is_reg_wire(cell->getPort("\\Q"), reg_name);
 
-		if (!out_is_reg_wire)
-			f << stringf("%s" "reg [%d:0] %s;\n", indent.c_str(), cell->parameters["\\WIDTH"].as_int()-1, reg_name.c_str());
+		if (!out_is_reg_wire) {
+			f << stringf("%s" "reg [%d:0] %s", indent.c_str(), cell->parameters["\\WIDTH"].as_int()-1, reg_name.c_str());
+			dump_reg_init(f, cell->getPort("\\Q"));
+			f << ";\n";
+		}
 
 		f << stringf("%s" "always @(%sedge ", indent.c_str(), pol_clk ? "pos" : "neg");
 		dump_sigspec(f, sig_clk);
@@ -806,7 +888,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		// for memory block make something like:
 		//  reg [7:0] memid [3:0];
 		//  initial begin
-		//    memid[0] <= ...
+		//    memid[0] = ...
 		//  end
 		f << stringf("%s" "reg [%d:%d] %s [%d:%d];\n", indent.c_str(), width-1, 0, mem_id.c_str(), size-1, 0);
 		if (use_init)
@@ -814,7 +896,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			f << stringf("%s" "initial begin\n", indent.c_str());
 			for (int i=0; i<size; i++)
 			{
-				f << stringf("%s" "  %s[%d] <= ", indent.c_str(), mem_id.c_str(), i);
+				f << stringf("%s" "  %s[%d] = ", indent.c_str(), mem_id.c_str(), i);
 				dump_const(f, cell->parameters["\\INIT"].extract(i*width, width));
 				f << stringf(";\n");
 			}
@@ -912,7 +994,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		int nwrite_ports = cell->parameters["\\WR_PORTS"].as_int();
 		RTLIL::SigSpec sig_wr_clk, sig_wr_data, sig_wr_addr, sig_wr_en;
 		bool wr_clk_posedge;
-		SigMap sigmap(active_module);
+
 		// write ports
 		for (int i=0; i < nwrite_ports; i++)
 		{
@@ -937,7 +1019,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 				int start_i = i, width = 1;
 				SigBit wen_bit = sig_wr_en[i];
 
-				while (i+1 < GetSize(sig_wr_en) && sigmap(sig_wr_en[i+1]) == sigmap(wen_bit))
+				while (i+1 < GetSize(sig_wr_en) && active_sigmap(sig_wr_en[i+1]) == active_sigmap(wen_bit))
 					i++, width++;
 
 				if (wen_bit == State::S0)
@@ -1251,6 +1333,16 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	reg_wires.clear();
 	reset_auto_counter(module);
 	active_module = module;
+	active_sigmap.set(module);
+	active_initdata.clear();
+
+	for (auto wire : module->wires())
+		if (wire->attributes.count("\\init")) {
+			SigSpec sig = active_sigmap(wire);
+			Const val = wire->attributes.at("\\init");
+			for (int i = 0; i < GetSize(sig) && i < GetSize(val); i++)
+				active_initdata[sig[i]] = val.bits.at(i);
+		}
 
 	if (!module->processes.empty())
 		log_warning("Module %s contains unmapped RTLIL proccesses. RTLIL processes\n"
@@ -1327,6 +1419,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 
 	f << stringf("%s" "endmodule\n", indent.c_str());
 	active_module = NULL;
+	active_sigmap.clear();
+	active_initdata.clear();
 }
 
 struct VerilogBackend : public Backend {
@@ -1362,6 +1456,11 @@ struct VerilogBackend : public Backend {
 		log("        not bit pattern. This option decativates this feature and instead\n");
 		log("        will write out all constants in binary.\n");
 		log("\n");
+		log("    -nohex\n");
+		log("        constant values that are compatible with hex output are usually\n");
+		log("        dumped as hex values. This option decativates this feature and\n");
+		log("        instead will write out all constants in binary.\n");
+		log("\n");
 		log("    -nostr\n");
 		log("        Parameters and attributes that are specified as strings in the\n");
 		log("        original input will be output as strings by this back-end. This\n");
@@ -1401,6 +1500,7 @@ struct VerilogBackend : public Backend {
 		attr2comment = false;
 		noexpr = false;
 		nodec = false;
+		nohex = false;
 		nostr = false;
 		defparam = false;
 		auto_prefix = "";
@@ -1461,6 +1561,10 @@ struct VerilogBackend : public Backend {
 				nodec = true;
 				continue;
 			}
+			if (arg == "-nohex") {
+				nohex = true;
+				continue;
+			}
 			if (arg == "-nostr") {
 				nostr = true;
 				continue;

examples/aiger/.gitignore

@@ -0,0 +1,5 @@
+demo.aig
+demo.aim
+demo.aiw
+demo.smt2
+demo.vcd

examples/aiger/README

@@ -0,0 +1,22 @@
+AIGER is a format for And-Inverter Graphs (AIGs).
+See http://fmv.jku.at/aiger/ for details.
+
+AIGER is used in the Hardware Model Checking Competition (HWMCC),
+therefore all solvers competing in the competition have to support
+the format.
+
+The example in this directory is using super_prove as solver. Check
+http://downloads.bvsrc.org/super_prove/ for the lates release. (See
+https://bitbucket.org/sterin/super_prove_build for sources.)
+
+The "demo.sh" script in this directory expects a "super_prove" executable
+in the PATH. E.g. extract the release to /usr/local/libexec/super_prove
+and then create a /usr/local/bin/super_prove file with the following
+contents (and "chmod +x" that file):
+
+	#!/bin/bash
+	exec /usr/local/libexec/super_prove/bin/super_prove.sh "$@"
+
+The "demo.sh" script also expects the "z3" SMT2 solver in the PATH for
+converting the witness file generated by super_prove to VCD using
+yosys-smtbmc. See https://github.com/Z3Prover/z3 for install notes.

examples/aiger/demo.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+set -ex
+yosys -p '
+	read_verilog -formal demo.v
+	prep -flatten -nordff -top demo
+	write_smt2 -wires demo.smt2
+	flatten demo; delete -output
+	memory_map; opt -full
+	techmap; opt -fast
+	abc -fast -g AND; opt_clean
+	write_aiger -map demo.aim demo.aig
+'
+super_prove demo.aig > demo.aiw
+yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2

examples/aiger/demo.v

@@ -0,0 +1,12 @@
+module demo(input clk, reset, ctrl);
+  localparam NBITS = 10;
+  reg [NBITS-1:0] counter;
+  initial counter[NBITS-2] = 0;
+  initial counter[0] = 1;
+  always @(posedge clk) begin
+    counter <= reset ? 1 : ctrl ? counter + 1 : counter - 1;
+    assume(counter != 0);
+    assume(counter != 1 << (NBITS-1));
+    assert(counter != (1 << NBITS)-1);
+  end
+endmodule

examples/gowin/.gitignore

@@ -0,0 +1,8 @@
+demo.bit
+demo.out
+demo.rpt
+demo_syn.v
+demo_out.v
+demo_tr.html
+testbench
+testbench.vcd

examples/gowin/README

@@ -0,0 +1,17 @@
+Simple test project for Gowinsemi GW2A-55K Eval Board Mini.
+
+Follow the install instructions for the Gowinsemi tools below,
+then run "bash run.sh" in this directory.
+
+
+Install instructions for gowinTool_linux
+----------------------------------------
+
+1.) extract gowinTool_linux.zip
+
+2.) set GOWIN_HOME env variable to the full path to the
+gowinTool_linux directory
+
+3.) edit gowinTool_linux/bin/gwlicense.ini. Set lic="..." to
+the full path to the license file.
+

examples/gowin/demo.cst

@@ -0,0 +1,41 @@
+// 50 MHz Clock
+IO_LOC "clk" D11;
+
+// LEDs
+IO_LOC "leds[0]"  D22;
+IO_LOC "leds[1]"  E22;
+IO_LOC "leds[2]"  G22;
+IO_LOC "leds[3]"  J22;
+IO_LOC "leds[4]"  L22;
+IO_LOC "leds[5]"  L19;
+IO_LOC "leds[6]"  L20;
+IO_LOC "leds[7]"  M21;
+IO_LOC "leds[8]"  N19;
+IO_LOC "leds[9]"  R19;
+IO_LOC "leds[10]" T18;
+IO_LOC "leds[11]" AA22;
+IO_LOC "leds[12]" U18;
+IO_LOC "leds[13]" V20;
+IO_LOC "leds[14]" AA21;
+IO_LOC "leds[15]" AB21;
+
+
+// 7-Segment Display
+IO_LOC "seg7dig[0]" E20;
+IO_LOC "seg7dig[1]" G18;
+IO_LOC "seg7dig[2]" G20;
+IO_LOC "seg7dig[3]" F21;
+IO_LOC "seg7dig[4]" J20;
+IO_LOC "seg7dig[5]" H21;
+IO_LOC "seg7dig[6]" H18;
+IO_LOC "seg7dig[7]" D20;
+IO_LOC "seg7sel[0]" C19;
+IO_LOC "seg7sel[1]" B22;
+IO_LOC "seg7sel[2]" C20;
+IO_LOC "seg7sel[3]" C21;
+
+// Switches
+IO_LOC "sw[0]" AB20;
+IO_LOC "sw[1]" AB19;
+IO_LOC "sw[2]" AB18;
+IO_LOC "sw[3]" AB17;

examples/gowin/demo.sdc

@@ -0,0 +1 @@
+create_clock -name clk -period 20 -waveform {0 10} [get_ports {clk}]

examples/gowin/demo.v

@@ -0,0 +1,12 @@
+module demo (
+	input clk,
+	input [3:0] sw,
+	output [15:0] leds,
+	output [7:0] seg7dig,
+	output [3:0] seg7sel
+);
+	localparam PRESCALE = 20;
+	reg [PRESCALE+3:0] counter = 0;
+	always @(posedge clk) counter <= counter + 1;
+	assign leds = 1 << counter[PRESCALE +: 4];
+endmodule

examples/gowin/run.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+set -ex
+yosys -p "synth_gowin -top demo -vout demo_syn.v" demo.v
+$GOWIN_HOME/bin/gowin -d demo_syn.v -cst demo.cst -sdc demo.sdc -p GW2A55-PBGA484-6 \
+		-warning_all -out demo_out.v -rpt demo.rpt -tr demo_tr.html -bit demo.bit
+
+# post place&route simulation (icarus verilog)
+if false; then
+	iverilog -D POST_IMPL -o testbench -s testbench testbench.v \
+			demo_out.v $(yosys-config --datdir/gowin/cells_sim.v)
+	vvp -N testbench
+fi

examples/gowin/testbench.v

@@ -0,0 +1,40 @@
+module testbench;
+	reg clk;
+
+	initial begin
+		#5 clk = 0;
+		forever #5 clk = ~clk;
+	end
+
+	wire [15:0] leds;
+
+	initial begin
+		// $dumpfile("testbench.vcd");
+		// $dumpvars(0, testbench);
+		$monitor("%b", leds);
+	end
+
+	demo uut (
+		.clk  (clk  ),
+`ifdef POST_IMPL
+		.\leds[0]  (leds[0]),
+		.\leds[1]  (leds[1]),
+		.\leds[2]  (leds[2]),
+		.\leds[3]  (leds[3]),
+		.\leds[4]  (leds[4]),
+		.\leds[5]  (leds[5]),
+		.\leds[6]  (leds[6]),
+		.\leds[7]  (leds[7]),
+		.\leds[8]  (leds[8]),
+		.\leds[9]  (leds[9]),
+		.\leds[10] (leds[10]),
+		.\leds[11] (leds[11]),
+		.\leds[12] (leds[12]),
+		.\leds[13] (leds[13]),
+		.\leds[14] (leds[14]),
+		.\leds[15] (leds[15])
+`else
+		.leds(leds)
+`endif
+	);
+endmodule

frontends/ast/ast.cc

@@ -1016,14 +1016,12 @@ void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump
 	flag_icells = icells;
 	flag_autowire = autowire;
 
-	std::vector<AstNode*> global_decls;
-
 	log_assert(current_ast->type == AST_DESIGN);
 	for (auto it = current_ast->children.begin(); it != current_ast->children.end(); it++)
 	{
 		if ((*it)->type == AST_MODULE)
 		{
-			for (auto n : global_decls)
+			for (auto n : design->verilog_globals)
 				(*it)->children.push_back(n->clone());
 
 			for (auto n : design->verilog_packages){
@@ -1054,7 +1052,7 @@ void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump
 		else if ((*it)->type == AST_PACKAGE)
 			design->verilog_packages.push_back((*it)->clone());
 		else
-			global_decls.push_back(*it);
+			design->verilog_globals.push_back((*it)->clone());
 	}
 }
 
@@ -1115,8 +1113,13 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict<RTLIL::IdString, R
 			goto rewrite_parameter;
 		}
 	}
-	if (parameters.size() > 0)
-		log_error("Requested parameter `%s' does not exist in module `%s'!\n", parameters.begin()->first.c_str(), stripped_name.c_str());
+
+	for (auto param : parameters) {
+		AstNode *defparam = new AstNode(AST_DEFPARAM, new AstNode(AST_IDENTIFIER));
+		defparam->children[0]->str = param.first.str();
+		defparam->children.push_back(AstNode::mkconst_bits(param.second.bits, (param.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0));
+		new_ast->children.push_back(defparam);
+	}
 
 	std::string modname;
 

frontends/ast/simplify.cc

@@ -685,19 +685,40 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		current_scope.clear();
 
 	// convert defparam nodes to cell parameters
-	if (type == AST_DEFPARAM && !str.empty()) {
-		size_t pos = str.rfind('.');
+	if (type == AST_DEFPARAM && !children.empty())
+	{
+		if (children[0]->type != AST_IDENTIFIER)
+			log_error("Module name in defparam at %s:%d contains non-constant expressions!\n", filename.c_str(), linenum);
+
+		string modname, paramname = children[0]->str;
+
+		size_t pos = paramname.rfind('.');
+
+		while (pos != 0 && pos != std::string::npos)
+		{
+			modname = paramname.substr(0, pos);
+
+			if (current_scope.count(modname))
+				break;
+
+			pos = paramname.rfind('.', pos - 1);
+		}
+
 		if (pos == std::string::npos)
-			log_error("Defparam `%s' does not contain a dot (module/parameter separator) at %s:%d!\n",
-					RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum);
-		std::string modname = str.substr(0, pos), paraname = "\\" + str.substr(pos+1);
-		if (current_scope.count(modname) == 0 || current_scope.at(modname)->type != AST_CELL)
-			log_error("Can't find cell for defparam `%s . %s` at %s:%d!\n", RTLIL::unescape_id(modname).c_str(), RTLIL::unescape_id(paraname).c_str(), filename.c_str(), linenum);
-		AstNode *cell = current_scope.at(modname), *paraset = clone();
+			log_error("Can't find object for defparam `%s` at %s:%d!\n", RTLIL::unescape_id(paramname).c_str(), filename.c_str(), linenum);
+
+		paramname = "\\" + paramname.substr(pos+1);
+
+		if (current_scope.at(modname)->type != AST_CELL)
+			log_error("Defparam argument `%s . %s` does not match a cell at %s:%d!\n",
+					RTLIL::unescape_id(modname).c_str(), RTLIL::unescape_id(paramname).c_str(), filename.c_str(), linenum);
+
+		AstNode *paraset = new AstNode(AST_PARASET, children[1]->clone(), GetSize(children) > 2 ? children[2]->clone() : NULL);
+		paraset->str = paramname;
+
+		AstNode *cell = current_scope.at(modname);
 		cell->children.insert(cell->children.begin() + 1, paraset);
-		paraset->type = AST_PARASET;
-		paraset->str = paraname;
-		str.clear();
+		delete_children();
 	}
 
 	// resolve constant prefixes
@@ -1062,6 +1083,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		did_something = true;
 	}
 
+	// check for local objects in unnamed block
+	if (type == AST_BLOCK && str.empty())
+	{
+		for (size_t i = 0; i < children.size(); i++)
+			if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM)
+				log_error("Local declaration in unnamed block at %s:%d is an unsupported SystemVerilog feature!\n",
+						children[i]->filename.c_str(), children[i]->linenum);
+	}
+
 	// transform block with name
 	if (type == AST_BLOCK && !str.empty())
 	{
@@ -1070,7 +1100,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 
 		std::vector<AstNode*> new_children;
 		for (size_t i = 0; i < children.size(); i++)
-			if (children[i]->type == AST_WIRE || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
+			if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
 				children[i]->simplify(false, false, false, stage, -1, false, false);
 				current_ast_mod->children.push_back(children[i]);
 				current_scope[children[i]->str] = children[i];
@@ -1843,7 +1873,8 @@ skip_dynamic_range_lvalue_expansion:;
 			if (str == "\\$ln" || str == "\\$log10" || str == "\\$exp" || str == "\\$sqrt" || str == "\\$pow" ||
 					str == "\\$floor" || str == "\\$ceil" || str == "\\$sin" || str == "\\$cos" || str == "\\$tan" ||
 					str == "\\$asin" || str == "\\$acos" || str == "\\$atan" || str == "\\$atan2" || str == "\\$hypot" ||
-					str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh")
+					str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh" ||
+					str == "\\$rtoi" || str == "\\$itor")
 			{
 				bool func_with_two_arguments = str == "\\$pow" || str == "\\$atan2" || str == "\\$hypot";
 				double x = 0, y = 0;
@@ -1880,29 +1911,34 @@ skip_dynamic_range_lvalue_expansion:;
 					y = children[1]->asReal(child_sign_hint);
 				}
 
-				newNode = new AstNode(AST_REALVALUE);
-				if (str == "\\$ln")         newNode->realvalue = ::log(x);
-				else if (str == "\\$log10") newNode->realvalue = ::log10(x);
-				else if (str == "\\$exp")   newNode->realvalue = ::exp(x);
-				else if (str == "\\$sqrt")  newNode->realvalue = ::sqrt(x);
-				else if (str == "\\$pow")   newNode->realvalue = ::pow(x, y);
-				else if (str == "\\$floor") newNode->realvalue = ::floor(x);
-				else if (str == "\\$ceil")  newNode->realvalue = ::ceil(x);
-				else if (str == "\\$sin")   newNode->realvalue = ::sin(x);
-				else if (str == "\\$cos")   newNode->realvalue = ::cos(x);
-				else if (str == "\\$tan")   newNode->realvalue = ::tan(x);
-				else if (str == "\\$asin")  newNode->realvalue = ::asin(x);
-				else if (str == "\\$acos")  newNode->realvalue = ::acos(x);
-				else if (str == "\\$atan")  newNode->realvalue = ::atan(x);
-				else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
-				else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
-				else if (str == "\\$sinh")  newNode->realvalue = ::sinh(x);
-				else if (str == "\\$cosh")  newNode->realvalue = ::cosh(x);
-				else if (str == "\\$tanh")  newNode->realvalue = ::tanh(x);
-				else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
-				else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
-				else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
-				else log_abort();
+				if (str == "\\$rtoi") {
+					newNode = AstNode::mkconst_int(x, true);
+				} else {
+					newNode = new AstNode(AST_REALVALUE);
+					if (str == "\\$ln")         newNode->realvalue = ::log(x);
+					else if (str == "\\$log10") newNode->realvalue = ::log10(x);
+					else if (str == "\\$exp")   newNode->realvalue = ::exp(x);
+					else if (str == "\\$sqrt")  newNode->realvalue = ::sqrt(x);
+					else if (str == "\\$pow")   newNode->realvalue = ::pow(x, y);
+					else if (str == "\\$floor") newNode->realvalue = ::floor(x);
+					else if (str == "\\$ceil")  newNode->realvalue = ::ceil(x);
+					else if (str == "\\$sin")   newNode->realvalue = ::sin(x);
+					else if (str == "\\$cos")   newNode->realvalue = ::cos(x);
+					else if (str == "\\$tan")   newNode->realvalue = ::tan(x);
+					else if (str == "\\$asin")  newNode->realvalue = ::asin(x);
+					else if (str == "\\$acos")  newNode->realvalue = ::acos(x);
+					else if (str == "\\$atan")  newNode->realvalue = ::atan(x);
+					else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
+					else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
+					else if (str == "\\$sinh")  newNode->realvalue = ::sinh(x);
+					else if (str == "\\$cosh")  newNode->realvalue = ::cosh(x);
+					else if (str == "\\$tanh")  newNode->realvalue = ::tanh(x);
+					else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
+					else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
+					else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
+					else if (str == "\\$itor")  newNode->realvalue = x;
+					else log_abort();
+				}
 				goto apply_newNode;
 			}
 
@@ -2137,7 +2173,7 @@ skip_dynamic_range_lvalue_expansion:;
 		}
 
 		for (auto child : decl->children)
-			if (child->type == AST_WIRE || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
+			if (child->type == AST_WIRE || child->type == AST_MEMORY || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
 			{
 				AstNode *wire = nullptr;
 
@@ -2197,7 +2233,7 @@ skip_dynamic_range_lvalue_expansion:;
 		}
 
 		for (auto child : decl->children)
-			if (child->type != AST_WIRE && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
+			if (child->type != AST_WIRE && child->type != AST_MEMORY && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
 			{
 				AstNode *stmt = child->clone();
 				stmt->replace_ids(prefix, replace_rules);
@@ -2660,7 +2696,7 @@ void AstNode::expand_genblock(std::string index_var, std::string prefix, std::ma
 			std::string new_name = prefix[0] == '\\' ? prefix.substr(1) : prefix;
 			size_t pos = child->str.rfind('.');
 			if (pos == std::string::npos)
-				pos = child->str[0] == '\\' ? 1 : 0;
+				pos = child->str[0] == '\\' && prefix[0] == '\\' ? 1 : 0;
 			else
 				pos = pos + 1;
 			new_name = child->str.substr(0, pos) + new_name + child->str.substr(pos);
@@ -3043,6 +3079,8 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 
 		if (bit_part_sel)
 			children.push_back(bit_part_sel);
+
+		did_something = true;
 	}
 
 	log_assert(id2ast == NULL || mem2reg_set.count(id2ast) == 0);

frontends/verilog/preproc.cc

@@ -210,7 +210,8 @@ static void input_file(std::istream &f, std::string filename)
 	input_buffer.insert(it, "\n`file_pop\n");
 }
 
-std::string frontend_verilog_preproc(std::istream &f, std::string filename, const std::map<std::string, std::string> pre_defines_map, const std::list<std::string> include_dirs)
+std::string frontend_verilog_preproc(std::istream &f, std::string filename, const std::map<std::string, std::string> &pre_defines_map,
+		dict<std::string, std::pair<std::string, bool>> &global_defines_cache, const std::list<std::string> &include_dirs)
 {
 	std::set<std::string> defines_with_args;
 	std::map<std::string, std::string> defines_map(pre_defines_map);
@@ -222,9 +223,19 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
 	input_buffer_charp = 0;
 
 	input_file(f, filename);
+
 	defines_map["YOSYS"] = "1";
 	defines_map[formal_mode ? "FORMAL" : "SYNTHESIS"] = "1";
 
+	for (auto &it : pre_defines_map)
+		defines_map[it.first] = it.second;
+
+	for (auto &it : global_defines_cache) {
+		if (it.second.second)
+			defines_with_args.insert(it.first);
+		defines_map[it.first] = it.second.first;
+	}
+
 	while (!input_buffer.empty())
 	{
 		std::string tok = next_token();
@@ -281,6 +292,8 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
 		if (tok == "`include") {
 			skip_spaces();
 			std::string fn = next_token(true);
+			while (fn.size() > 1 && fn[0] == '`' && defines_map.count(fn.substr(1)) > 0)
+				fn = defines_map.at(fn.substr(1));
 			while (1) {
 				size_t pos = fn.find('"');
 				if (pos == std::string::npos)
@@ -379,6 +392,7 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
 				defines_with_args.insert(name);
 			else
 				defines_with_args.erase(name);
+			global_defines_cache[name] = std::pair<std::string, bool>(value, state == 2);
 			continue;
 		}
 
@@ -389,6 +403,7 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
 			// printf("undef: >>%s<<\n", name.c_str());
 			defines_map.erase(name);
 			defines_with_args.erase(name);
+			global_defines_cache.erase(name);
 			continue;
 		}
 

frontends/verilog/verilog_frontend.cc

@@ -303,10 +303,10 @@ struct VerilogFrontend : public Frontend {
 			}
 			if (arg == "-D" && argidx+1 < args.size()) {
 				std::string name = args[++argidx], value;
-				size_t equal = name.find('=', 2);
+				size_t equal = name.find('=');
 				if (equal != std::string::npos) {
-					value = arg.substr(equal+1);
-					name = arg.substr(0, equal);
+					value = name.substr(equal+1);
+					name = name.substr(0, equal);
 				}
 				defines_map[name] = value;
 				continue;
@@ -345,7 +345,7 @@ struct VerilogFrontend : public Frontend {
 		std::string code_after_preproc;
 
 		if (!flag_nopp) {
-			code_after_preproc = frontend_verilog_preproc(*f, filename, defines_map, include_dirs);
+			code_after_preproc = frontend_verilog_preproc(*f, filename, defines_map, design->verilog_defines, include_dirs);
 			if (flag_ppdump)
 				log("-- Verilog code after preprocessor --\n%s-- END OF DUMP --\n", code_after_preproc.c_str());
 			lexin = new std::istringstream(code_after_preproc);
@@ -436,6 +436,66 @@ struct VerilogDefaults : public Pass {
 	}
 } VerilogDefaults;
 
+struct VerilogDefines : public Pass {
+	VerilogDefines() : Pass("verilog_defines", "define and undefine verilog defines") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    verilog_defines [options]\n");
+		log("\n");
+		log("Define and undefine verilog preprocessor macros.\n");
+		log("\n");
+		log("    -Dname[=definition]\n");
+		log("        define the preprocessor symbol 'name' and set its optional value\n");
+		log("        'definition'\n");
+		log("\n");
+		log("    -Uname[=definition]\n");
+		log("        undefine the preprocessor symbol 'name'\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			std::string arg = args[argidx];
+			if (arg == "-D" && argidx+1 < args.size()) {
+				std::string name = args[++argidx], value;
+				size_t equal = name.find('=');
+				if (equal != std::string::npos) {
+					value = name.substr(equal+1);
+					name = name.substr(0, equal);
+				}
+				design->verilog_defines[name] = std::pair<std::string, bool>(value, false);
+				continue;
+			}
+			if (arg.compare(0, 2, "-D") == 0) {
+				size_t equal = arg.find('=', 2);
+				std::string name = arg.substr(2, equal-2);
+				std::string value;
+				if (equal != std::string::npos)
+					value = arg.substr(equal+1);
+				design->verilog_defines[name] = std::pair<std::string, bool>(value, false);
+				continue;
+			}
+			if (arg == "-U" && argidx+1 < args.size()) {
+				std::string name = args[++argidx];
+				design->verilog_defines.erase(name);
+				continue;
+			}
+			if (arg.compare(0, 2, "-U") == 0) {
+				std::string name = arg.substr(2);
+				design->verilog_defines.erase(name);
+				continue;
+			}
+			break;
+		}
+
+		if (args.size() != argidx)
+			cmd_error(args, argidx, "Extra argument.");
+	}
+} VerilogDefines;
+
 YOSYS_NAMESPACE_END
 
 // the yyerror function used by bison to report parser errors

frontends/verilog/verilog_frontend.h

@@ -68,7 +68,8 @@ namespace VERILOG_FRONTEND
 }
 
 // the pre-processor
-std::string frontend_verilog_preproc(std::istream &f, std::string filename, const std::map<std::string, std::string> pre_defines_map, const std::list<std::string> include_dirs);
+std::string frontend_verilog_preproc(std::istream &f, std::string filename, const std::map<std::string, std::string> &pre_defines_map,
+		dict<std::string, std::pair<std::string, bool>> &global_defines_cache, const std::list<std::string> &include_dirs);
 
 YOSYS_NAMESPACE_END
 

frontends/verilog/verilog_lexer.l

@@ -192,6 +192,9 @@ YOSYS_NAMESPACE_END
 "genvar"  { return TOK_GENVAR; }
 "real"    { return TOK_REAL; }
 
+"enum"    { SV_KEYWORD(TOK_ENUM); }
+"typedef" { SV_KEYWORD(TOK_TYPEDEF); }
+
 [0-9][0-9_]* {
 	frontend_verilog_yylval.string = new std::string(yytext);
 	return TOK_CONST;

frontends/verilog/verilog_parser.y

@@ -114,7 +114,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
@@ -666,14 +666,13 @@ defparam_decl_list:
 	single_defparam_decl | defparam_decl_list ',' single_defparam_decl;
 
 single_defparam_decl:
-	range hierarchical_id '=' expr {
+	range rvalue '=' expr {
 		AstNode *node = new AstNode(AST_DEFPARAM);
-		node->str = *$2;
+		node->children.push_back($2);
 		node->children.push_back($4);
 		if ($1 != NULL)
 			node->children.push_back($1);
 		ast_stack.back()->children.push_back(node);
-		delete $2;
 	};
 
 wire_decl:

kernel/driver.cc

@@ -218,6 +218,9 @@ int main(int argc, char **argv)
 		printf("        yosys_dump_<header_id>.il is used as filename if none is specified.\n");
 		printf("        Use 'ALL' as <header_id> to dump at every header.\n");
 		printf("\n");
+		printf("    -W regex\n");
+		printf("        print a warning for all log messages matching the regex \n");
+		printf("\n");
 		printf("    -V\n");
 		printf("        print version information and exit\n");
 		printf("\n");
@@ -238,7 +241,7 @@ int main(int argc, char **argv)
 	}
 
 	int opt;
-	while ((opt = getopt(argc, argv, "MXAQTVSm:f:Hh:b:o:p:l:L:qv:tds:c:D:")) != -1)
+	while ((opt = getopt(argc, argv, "MXAQTVSm:f:Hh:b:o:p:l:L:qv:tds:c:W:D:")) != -1)
 	{
 		switch (opt)
 		{
@@ -320,6 +323,12 @@ int main(int argc, char **argv)
 			scriptfile = optarg;
 			scriptfile_tcl = true;
 			break;
+		case 'W':
+			log_warn_regexes.push_back(std::regex(optarg,
+					std::regex_constants::nosubs |
+					std::regex_constants::optimize |
+					std::regex_constants::egrep));
+			break;
 		case 'D':
 			{
 				auto args = split_tokens(optarg, ":");

kernel/log.cc

@@ -41,6 +41,7 @@ YOSYS_NAMESPACE_BEGIN
 std::vector<FILE*> log_files;
 std::vector<std::ostream*> log_streams;
 std::map<std::string, std::set<std::string>> log_hdump;
+std::vector<std::regex> log_warn_regexes;
 bool log_hdump_all = false;
 FILE *log_errfile = NULL;
 SHA1 *log_hasher = NULL;
@@ -136,6 +137,32 @@ void logv(const char *format, va_list ap)
 
 	for (auto f : log_streams)
 		*f << str;
+
+	static std::string linebuffer;
+	static bool log_warn_regex_recusion_guard = false;
+
+	if (!log_warn_regex_recusion_guard)
+	{
+		log_warn_regex_recusion_guard = true;
+
+		if (log_warn_regexes.empty())
+		{
+			linebuffer.clear();
+		}
+		else
+		{
+			linebuffer += str;
+
+			if (!linebuffer.empty() && linebuffer.back() == '\n') {
+				for (auto &re : log_warn_regexes)
+					if (std::regex_search(linebuffer, re))
+						log_warning("Found log message matching -W regex:\n%s", str.c_str());
+				linebuffer.clear();
+			}
+		}
+
+		log_warn_regex_recusion_guard = false;
+	}
 }
 
 void logv_header(RTLIL::Design *design, const char *format, va_list ap)
@@ -262,8 +289,8 @@ void log_cmd_error(const char *format, ...)
 
 void log_spacer()
 {
-	while (log_newline_count < 2)
-		log("\n");
+	if (log_newline_count < 2) log("\n");
+	if (log_newline_count < 2) log("\n");
 }
 
 void log_push()

kernel/log.h

@@ -23,6 +23,7 @@
 #define LOG_H
 
 #include <time.h>
+#include <regex>
 
 #ifndef _WIN32
 #  include <sys/time.h>
@@ -48,6 +49,7 @@ struct log_cmd_error_exception { };
 extern std::vector<FILE*> log_files;
 extern std::vector<std::ostream*> log_streams;
 extern std::map<std::string, std::set<std::string>> log_hdump;
+extern std::vector<std::regex> log_warn_regexes;
 extern bool log_hdump_all;
 extern FILE *log_errfile;
 extern SHA1 *log_hasher;

kernel/register.cc

@@ -173,7 +173,7 @@ void Pass::call(RTLIL::Design *design, std::string command)
 	}
 
 	while (!tok.empty()) {
-		if (tok == "#") {
+		if (tok[0] == '#') {
 			int stop;
 			for (stop = 0; stop < GetSize(cmd_buf); stop++)
 				if (cmd_buf[stop] == '\r' || cmd_buf[stop] == '\n')

kernel/rtlil.cc

@@ -306,6 +306,8 @@ RTLIL::Design::~Design()
 		delete it->second;
 	for (auto n : verilog_packages)
 		delete n;
+	for (auto n : verilog_globals)
+		delete n;
 }
 
 RTLIL::ObjRange<RTLIL::Module*> RTLIL::Design::modules()
@@ -2048,6 +2050,7 @@ RTLIL::Memory::Memory()
 	hashidx_ = hashidx_count;
 
 	width = 1;
+	start_offset = 0;
 	size = 0;
 }
 
@@ -2764,10 +2767,11 @@ void RTLIL::SigSpec::remove2(const RTLIL::SigSpec &pattern, RTLIL::SigSpec *othe
 		other->unpack();
 	}
 
-	for (int i = GetSize(bits_) - 1; i >= 0; i--) {
+	for (int i = GetSize(bits_) - 1; i >= 0; i--)
+	{
 		if (bits_[i].wire == NULL) continue;
 
-		for (auto &pattern_chunk : pattern.chunks()) {
+		for (auto &pattern_chunk : pattern.chunks())
 			if (bits_[i].wire == pattern_chunk.wire &&
 				bits_[i].offset >= pattern_chunk.offset &&
 				bits_[i].offset < pattern_chunk.offset + pattern_chunk.width) {
@@ -2777,8 +2781,8 @@ void RTLIL::SigSpec::remove2(const RTLIL::SigSpec &pattern, RTLIL::SigSpec *othe
 					other->bits_.erase(other->bits_.begin() + i);
 					other->width_--;
 				}
+				break;
 			}
-		}
 	}
 
 	check();

kernel/rtlil.h

@@ -793,7 +793,8 @@ struct RTLIL::Design
 
 	int refcount_modules_;
 	dict<RTLIL::IdString, RTLIL::Module*> modules_;
-	std::vector<AST::AstNode*> verilog_packages;
+	std::vector<AST::AstNode*> verilog_packages, verilog_globals;
+	dict<std::string, std::pair<std::string, bool>> verilog_defines;
 
 	std::vector<RTLIL::Selection> selection_stack;
 	dict<RTLIL::IdString, RTLIL::Selection> selection_vars;

kernel/yosys.cc

@@ -903,6 +903,8 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
 			command = "verilog";
 		else if (filename.size() > 3 && filename.substr(filename.size()-3) == ".il")
 			command = "ilang";
+		else if (filename.size() > 4 && filename.substr(filename.size()-4) == ".aig")
+			command = "aiger";
 		else if (filename.size() > 5 && filename.substr(filename.size()-5) == ".blif")
 			command = "blif";
 		else if (filename.size() > 5 && filename.substr(filename.size()-5) == ".edif")

passes/cmds/check.cc

@@ -44,6 +44,9 @@ struct CheckPass : public Pass {
 		log("When called with -noinit then this command also checks for wires which have\n");
 		log("the 'init' attribute set.\n");
 		log("\n");
+		log("When called with -initdrv then this command also checks for wires which have\n");
+		log("the 'init' attribute set and aren't driven by a FF cell type.\n");
+		log("\n");
 		log("When called with -assert then the command will produce an error if any\n");
 		log("problems are found in the current design.\n");
 		log("\n");
@@ -52,6 +55,7 @@ struct CheckPass : public Pass {
 	{
 		int counter = 0;
 		bool noinit = false;
+		bool initdrv = false;
 		bool assert_mode = false;
 
 		size_t argidx;
@@ -60,6 +64,10 @@ struct CheckPass : public Pass {
 				noinit = true;
 				continue;
 			}
+			if (args[argidx] == "-initdrv") {
+				initdrv = true;
+				continue;
+			}
 			if (args[argidx] == "-assert") {
 				assert_mode = true;
 				continue;
@@ -70,6 +78,49 @@ struct CheckPass : public Pass {
 
 		log_header(design, "Executing CHECK pass (checking for obvious problems).\n");
 
+		pool<IdString> fftypes;
+		fftypes.insert("$sr");
+		fftypes.insert("$ff");
+		fftypes.insert("$dff");
+		fftypes.insert("$dffe");
+		fftypes.insert("$dffsr");
+		fftypes.insert("$adff");
+		fftypes.insert("$dlatch");
+		fftypes.insert("$dlatchsr");
+		fftypes.insert("$_DFFE_NN_");
+		fftypes.insert("$_DFFE_NP_");
+		fftypes.insert("$_DFFE_PN_");
+		fftypes.insert("$_DFFE_PP_");
+		fftypes.insert("$_DFFSR_NNN_");
+		fftypes.insert("$_DFFSR_NNP_");
+		fftypes.insert("$_DFFSR_NPN_");
+		fftypes.insert("$_DFFSR_NPP_");
+		fftypes.insert("$_DFFSR_PNN_");
+		fftypes.insert("$_DFFSR_PNP_");
+		fftypes.insert("$_DFFSR_PPN_");
+		fftypes.insert("$_DFFSR_PPP_");
+		fftypes.insert("$_DFF_NN0_");
+		fftypes.insert("$_DFF_NN1_");
+		fftypes.insert("$_DFF_NP0_");
+		fftypes.insert("$_DFF_NP1_");
+		fftypes.insert("$_DFF_N_");
+		fftypes.insert("$_DFF_PN0_");
+		fftypes.insert("$_DFF_PN1_");
+		fftypes.insert("$_DFF_PP0_");
+		fftypes.insert("$_DFF_PP1_");
+		fftypes.insert("$_DFF_P_");
+		fftypes.insert("$_DLATCHSR_NNN_");
+		fftypes.insert("$_DLATCHSR_NNP_");
+		fftypes.insert("$_DLATCHSR_NPN_");
+		fftypes.insert("$_DLATCHSR_NPP_");
+		fftypes.insert("$_DLATCHSR_PNN_");
+		fftypes.insert("$_DLATCHSR_PNP_");
+		fftypes.insert("$_DLATCHSR_PPN_");
+		fftypes.insert("$_DLATCHSR_PPP_");
+		fftypes.insert("$_DLATCH_N_");
+		fftypes.insert("$_DLATCH_P_");
+		fftypes.insert("$_FF_");
+
 		for (auto module : design->selected_whole_modules_warn())
 		{
 			if (module->has_processes_warn())
@@ -109,6 +160,8 @@ struct CheckPass : public Pass {
 						if (bit.wire) wire_drivers_count[bit]++;
 			}
 
+			pool<SigBit> init_bits;
+
 			for (auto wire : module->wires()) {
 				if (wire->port_input) {
 					SigSpec sig = sigmap(wire);
@@ -121,9 +174,15 @@ struct CheckPass : public Pass {
 				if (wire->port_input && !wire->port_output)
 					for (auto bit : sigmap(wire))
 						if (bit.wire) wire_drivers_count[bit]++;
-				if (noinit && wire->attributes.count("\\init")) {
-					log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
-					counter++;
+				if (wire->attributes.count("\\init")) {
+					Const initval = wire->attributes.at("\\init");
+					for (int i = 0; i < GetSize(initval) && i < GetSize(wire); i++)
+						if (initval[i] == State::S0 || initval[i] == State::S1)
+							init_bits.insert(sigmap(SigBit(wire, i)));
+					if (noinit) {
+						log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
+						counter++;
+					}
 				}
 			}
 
@@ -150,6 +209,26 @@ struct CheckPass : public Pass {
 				log_warning("%s", message.c_str());
 				counter++;
 			}
+
+			if (initdrv)
+			{
+				for (auto cell : module->cells())
+				{
+					if (fftypes.count(cell->type) == 0)
+						continue;
+
+					for (auto bit : sigmap(cell->getPort("\\Q")))
+						init_bits.erase(bit);
+				}
+
+				SigSpec init_sig(init_bits);
+				init_sig.sort_and_unify();
+
+				for (auto chunk : init_sig.chunks()) {
+					log_warning("Wire %s.%s has 'init' attribute and is not driven by an FF cell.\n", log_id(module), log_signal(chunk));
+					counter++;
+				}
+			}
 		}
 
 		log("found and reported %d problems.\n", counter);

passes/cmds/design.cc

@@ -17,10 +17,8 @@
  *
  */
 
-#include "kernel/register.h"
-#include "kernel/celltypes.h"
-#include "kernel/rtlil.h"
-#include "kernel/log.h"
+#include "kernel/yosys.h"
+#include "frontends/ast/ast.h"
 
 YOSYS_NAMESPACE_BEGIN
 
@@ -82,11 +80,18 @@ struct DesignPass : public Pass {
 		log("\n");
 		log("Copy modules from the current design into the specified one.\n");
 		log("\n");
+		log("\n");
+		log("    design -reset-vlog\n");
+		log("\n");
+		log("The Verilog front-end remembers defined macros and top-level declarations\n");
+		log("between calls to 'read_verilog'. This command resets this memory.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool got_mode = false;
 		bool reset_mode = false;
+		bool reset_vlog_mode = false;
 		bool push_mode = false;
 		bool pop_mode = false;
 		RTLIL::Design *copy_from_design = NULL, *copy_to_design = NULL;
@@ -102,6 +107,11 @@ struct DesignPass : public Pass {
 				reset_mode = true;
 				continue;
 			}
+			if (!got_mode && args[argidx] == "-reset-vlog") {
+				got_mode = true;
+				reset_vlog_mode = true;
+				continue;
+			}
 			if (!got_mode && args[argidx] == "-push") {
 				got_mode = true;
 				push_mode = true;
@@ -235,19 +245,34 @@ struct DesignPass : public Pass {
 			design->selection_stack.push_back(RTLIL::Selection());
 		}
 
+		if (reset_mode || reset_vlog_mode || !load_name.empty() || push_mode || pop_mode)
+		{
+			for (auto node : design->verilog_packages)
+				delete node;
+			design->verilog_packages.clear();
+
+			for (auto node : design->verilog_globals)
+				delete node;
+			design->verilog_globals.clear();
+
+			design->verilog_defines.clear();
+		}
+
 		if (!load_name.empty() || pop_mode)
 		{
 			RTLIL::Design *saved_design = pop_mode ? pushed_designs.back() : saved_designs.at(load_name);
 
-			if (pop_mode)
-				pushed_designs.pop_back();
-
 			for (auto &it : saved_design->modules_)
 				design->add(it.second->clone());
 
 			design->selection_stack = saved_design->selection_stack;
 			design->selection_vars = saved_design->selection_vars;
 			design->selected_active_module = saved_design->selected_active_module;
+
+			if (pop_mode) {
+				delete saved_design;
+				pushed_designs.pop_back();
+			}
 		}
 	}
 } DesignPass;

passes/cmds/scc.cc

@@ -163,16 +163,8 @@ struct SccWorker
 		}
 
 		for (auto cell : workQueue)
-			cellToNextCell[cell] = sigToNextCells.find(cellToNextSig[cell]);
-
-		labelCounter = 0;
-		cellLabels.clear();
-
-		while (workQueue.size() > 0)
 		{
-			RTLIL::Cell *cell = *workQueue.begin();
-			log_assert(cellStack.size() == 0);
-			cellDepth.clear();
+			cellToNextCell[cell] = sigToNextCells.find(cellToNextSig[cell]);
 
 			if (!nofeedbackMode && cellToNextCell[cell].count(cell)) {
 				log("Found an SCC:");
@@ -183,6 +175,16 @@ struct SccWorker
 				sccList.push_back(scc);
 				log("\n");
 			}
+		}
+
+		labelCounter = 0;
+		cellLabels.clear();
+
+		while (!workQueue.empty())
+		{
+			RTLIL::Cell *cell = *workQueue.begin();
+			log_assert(cellStack.size() == 0);
+			cellDepth.clear();
 
 			run(cell, 0, maxDepth);
 		}
@@ -244,11 +246,9 @@ struct SccPass : public Pass {
 		log("        are assumed to be bidirectional 'inout' ports.\n");
 		log("\n");
 		log("    -set_attr <name> <value>\n");
-		log("    -set_cell_attr <name> <value>\n");
-		log("    -set_wire_attr <name> <value>\n");
-		log("        set the specified attribute on all cells and/or wires that are part of\n");
-		log("        a logic loop. the special token {} in the value is replaced with a\n");
-		log("        unique identifier for the logic loop.\n");
+		log("        set the specified attribute on all cells that are part of a logic\n");
+		log("        loop. the special token {} in the value is replaced with a unique\n");
+		log("        identifier for the logic loop.\n");
 		log("\n");
 		log("    -select\n");
 		log("        replace the current selection with a selection of all cells and wires\n");
@@ -257,7 +257,7 @@ struct SccPass : public Pass {
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
-		std::map<std::string, std::string> setCellAttr, setWireAttr;
+		std::map<std::string, std::string> setAttr;
 		bool allCellTypes = false;
 		bool selectMode = false;
 		bool nofeedbackMode = false;
@@ -285,18 +285,7 @@ struct SccPass : public Pass {
 				continue;
 			}
 			if (args[argidx] == "-set_attr" && argidx+2 < args.size()) {
-				setCellAttr[args[argidx+1]] = args[argidx+2];
-				setWireAttr[args[argidx+1]] = args[argidx+2];
-				argidx += 2;
-				continue;
-			}
-			if (args[argidx] == "-set_cell_attr" && argidx+2 < args.size()) {
-				setCellAttr[args[argidx+1]] = args[argidx+2];
-				argidx += 2;
-				continue;
-			}
-			if (args[argidx] == "-set_wire_attr" && argidx+2 < args.size()) {
-				setWireAttr[args[argidx+1]] = args[argidx+2];
+				setAttr[args[argidx+1]] = args[argidx+2];
 				argidx += 2;
 				continue;
 			}
@@ -309,9 +298,6 @@ struct SccPass : public Pass {
 		int origSelectPos = design->selection_stack.size() - 1;
 		extra_args(args, argidx, design);
 
-		if (setCellAttr.size() > 0 || setWireAttr.size() > 0)
-			log_cmd_error("The -set*_attr options are not implemented at the moment!\n");
-
 		RTLIL::Selection newSelection(false);
 		int scc_counter = 0;
 
@@ -319,7 +305,33 @@ struct SccPass : public Pass {
 			if (design->selected(mod_it.second))
 			{
 				SccWorker worker(design, mod_it.second, nofeedbackMode, allCellTypes, maxDepth);
-				scc_counter += GetSize(worker.sccList);
+
+				if (!setAttr.empty())
+				{
+					for (const auto &cells : worker.sccList)
+					{
+						for (auto attr : setAttr)
+						{
+							IdString attr_name(RTLIL::escape_id(attr.first));
+							string attr_valstr = attr.second;
+							string index = stringf("%d", scc_counter);
+
+							for (size_t pos = 0; (pos = attr_valstr.find("{}", pos)) != string::npos; pos += index.size())
+								attr_valstr.replace(pos, 2, index);
+
+							Const attr_value(attr_valstr);
+
+							for (auto cell : cells)
+								cell->attributes[attr_name] = attr_value;
+						}
+
+						scc_counter++;
+					}
+				}
+				else
+				{
+					scc_counter += GetSize(worker.sccList);
+				}
 
 				if (selectMode)
 					worker.select(newSelection);

passes/cmds/setundef.cc

@@ -90,6 +90,8 @@ struct SetundefPass : public Pass {
 		bool init_mode = false;
 		SetundefWorker worker;
 
+		log_header(design, "Executing SETUNDEF pass (replace undef values with defined constants).\n");
+
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
@@ -137,8 +139,11 @@ struct SetundefPass : public Pass {
 				SigPool undriven_signals;
 
 				for (auto &it : module->wires_)
-					if (!it.second->port_input)
-						undriven_signals.add(sigmap(it.second));
+					undriven_signals.add(sigmap(it.second));
+
+				for (auto &it : module->wires_)
+					if (it.second->port_input)
+						undriven_signals.del(sigmap(it.second));
 
 				CellTypes ct(design);
 				for (auto &it : module->cells_)

passes/cmds/splitnets.cc

@@ -37,14 +37,20 @@ struct SplitnetsWorker
 			new_wire_name += format.substr(0, 1);
 
 		if (width > 1) {
-			new_wire_name += stringf("%d", offset+width-1);
+			if (wire->upto)
+				new_wire_name += stringf("%d", wire->start_offset+wire->width-(offset+width)-1);
+			else
+				new_wire_name += stringf("%d", wire->start_offset+offset+width-1);
 			if (format.size() > 2)
 				new_wire_name += format.substr(2, 1);
 			else
 				new_wire_name += ":";
 		}
 
-		new_wire_name += stringf("%d", offset);
+		if (wire->upto)
+			new_wire_name += stringf("%d", wire->start_offset+wire->width-offset-1);
+		else
+			new_wire_name += stringf("%d", wire->start_offset+offset);
 
 		if (format.size() > 1)
 			new_wire_name += format.substr(1, 1);

passes/equiv/equiv_purge.cc

@@ -80,7 +80,7 @@ struct EquivPurgeWorker
 			Wire *wire = module->addWire(name, GetSize(sig));
 			wire->port_input = true;
 			module->connect(sig, wire);
-			log("  Module input: %s\n", log_signal(wire));
+			log("  Module input: %s (%s)\n", log_signal(wire), log_signal(sig));
 			return module->addWire(NEW_ID, GetSize(sig));
 		}
 	}

passes/equiv/equiv_simple.cc

@@ -59,7 +59,7 @@ struct EquivSimpleWorker
 		for (auto &conn : cell->connections())
 			if (yosys_celltypes.cell_input(cell->type, conn.first))
 				for (auto bit : sigmap(conn.second)) {
-					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) {
+					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) {
 						if (!conn.first.in("\\CLK", "\\C"))
 							next_seed.insert(bit);
 					} else
@@ -329,7 +329,7 @@ struct EquivSimplePass : public Pass {
 					unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));
 
 			for (auto cell : module->cells()) {
-				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
 					continue;
 				for (auto &conn : cell->connections())
 					if (yosys_celltypes.cell_output(cell->type, conn.first))

passes/fsm/fsm_expand.cc

@@ -54,13 +54,27 @@ struct FsmExpand
 			if (cell->getPort("\\A").size() < 2)
 				return true;
 
+		int in_bits = 0;
 		RTLIL::SigSpec new_signals;
-		if (cell->hasPort("\\A"))
+
+		if (cell->hasPort("\\A")) {
+			in_bits += GetSize(cell->getPort("\\A"));
 			new_signals.append(assign_map(cell->getPort("\\A")));
-		if (cell->hasPort("\\B"))
+		}
+
+		if (cell->hasPort("\\B")) {
+			in_bits += GetSize(cell->getPort("\\B"));
 			new_signals.append(assign_map(cell->getPort("\\B")));
-		if (cell->hasPort("\\S"))
+		}
+
+		if (cell->hasPort("\\S")) {
+			in_bits += GetSize(cell->getPort("\\S"));
 			new_signals.append(assign_map(cell->getPort("\\S")));
+		}
+
+		if (in_bits > 8)
+			return false;
+
 		if (cell->hasPort("\\Y"))
 			new_signals.append(assign_map(cell->getPort("\\Y")));
 
@@ -173,6 +187,16 @@ struct FsmExpand
 		new_ctrl_out.append(output_sig);
 		fsm_cell->setPort("\\CTRL_OUT", new_ctrl_out);
 
+		if (GetSize(input_sig) > 10)
+			log_warning("Cell %s.%s (%s) has %d input bits, merging into FSM %s.%s might be problematic.\n",
+					log_id(cell->module), log_id(cell), log_id(cell->type),
+					GetSize(input_sig), log_id(fsm_cell->module), log_id(fsm_cell));
+
+		if (GetSize(fsm_data.transition_table) > 10000)
+			log_warning("Transition table for FSM %s.%s already has %d rows, merging more cells "
+					"into this FSM might be problematic.\n", log_id(fsm_cell->module), log_id(fsm_cell),
+					GetSize(fsm_data.transition_table));
+
 		std::vector<FsmData::transition_t> new_transition_table;
 		for (auto &tr : fsm_data.transition_table) {
 			for (int i = 0; i < (1 << input_sig.size()); i++) {

passes/hierarchy/hierarchy.cc

@@ -175,16 +175,12 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 			{
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "verilog");
 					goto loaded_module;
 				}
 
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "ilang");
 					goto loaded_module;
 				}
@@ -213,7 +209,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 					log_error("Module `%s' referenced in module `%s' in cell `%s' does not have a port named '%s'.\n",
 							log_id(cell->type), log_id(module), log_id(cell), log_id(conn.first));
 			for (auto &param : cell->parameters)
-				if (mod->avail_parameters.count(param.first) == 0 && param.first[0] != '$')
+				if (mod->avail_parameters.count(param.first) == 0 && param.first[0] != '$' && strchr(param.first.c_str(), '.') == NULL)
 					log_error("Module `%s' referenced in module `%s' in cell `%s' does not have a parameter named '%s'.\n",
 							log_id(cell->type), log_id(module), log_id(cell), log_id(param.first));
 		}
@@ -367,6 +363,11 @@ struct HierarchyPass : public Pass {
 		log("        per default this pass also converts positional arguments in cells\n");
 		log("        to arguments using port names. this option disables this behavior.\n");
 		log("\n");
+		log("    -keep_portwidths\n");
+		log("        per default this pass adjusts the port width on cells that are\n");
+		log("        module instances when the width does not match the module port. this\n");
+		log("        option disables this behavior.\n");
+		log("\n");
 		log("    -nokeep_asserts\n");
 		log("        per default this pass sets the \"keep\" attribute on all modules\n");
 		log("        that directly or indirectly contain one or more $assert cells. this\n");
@@ -412,6 +413,7 @@ struct HierarchyPass : public Pass {
 		bool auto_top_mode = false;
 		bool generate_mode = false;
 		bool keep_positionals = false;
+		bool keep_portwidths = false;
 		bool nokeep_asserts = false;
 		std::vector<std::string> generate_cells;
 		std::vector<generate_port_decl_t> generate_ports;
@@ -470,6 +472,10 @@ struct HierarchyPass : public Pass {
 				keep_positionals = true;
 				continue;
 			}
+			if (args[argidx] == "-keep_portwidths") {
+				keep_portwidths = true;
+				continue;
+			}
 			if (args[argidx] == "-nokeep_asserts") {
 				nokeep_asserts = true;
 				continue;
@@ -614,6 +620,52 @@ struct HierarchyPass : public Pass {
 			}
 		}
 
+		if (!keep_portwidths)
+		{
+			for (auto module : design->modules())
+			for (auto cell : module->cells())
+			{
+				Module *m = design->module(cell->type);
+
+				if (m == nullptr)
+					continue;
+
+				for (auto &conn : cell->connections())
+				{
+					Wire *w = m->wire(conn.first);
+
+					if (w == nullptr || w->port_id == 0)
+						continue;
+
+					if (GetSize(w) == GetSize(conn.second))
+						continue;
+
+					SigSpec sig = conn.second;
+
+					if (GetSize(w) < GetSize(conn.second))
+					{
+						int n = GetSize(conn.second) - GetSize(w);
+						if (!w->port_input && w->port_output)
+							module->connect(sig.extract(GetSize(w), n), Const(0, n));
+						sig.remove(GetSize(w), n);
+					}
+					else
+					{
+						int n = GetSize(w) - GetSize(conn.second);
+						if (w->port_input && !w->port_output)
+							sig.append(Const(0, n));
+						else
+							sig.append(module->addWire(NEW_ID, n));
+					}
+
+					if (!conn.second.is_fully_const() || !w->port_input || w->port_output)
+						log_warning("Resizing cell port %s.%s.%s from %d bits to %d bits.\n", log_id(module), log_id(cell),
+								log_id(conn.first), GetSize(conn.second), GetSize(sig));
+					cell->setPort(conn.first, sig);
+				}
+			}
+		}
+
 		log_pop();
 	}
 } HierarchyPass;

passes/hierarchy/submod.cc

@@ -169,6 +169,7 @@ struct SubmodWorker
 		}
 
 		new_mod->fixup_ports();
+		ct.setup_module(new_mod);
 
 		for (RTLIL::Cell *cell : submod.cells) {
 			RTLIL::Cell *new_cell = new_mod->addCell(cell->name, cell);

passes/opt/opt_rmdff.cc

@@ -41,9 +41,27 @@ void remove_init_attr(SigSpec sig)
 
 bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 {
-	SigSpec sig_e = dlatch->getPort("\\EN");
+	SigSpec sig_e;
+	State on_state, off_state;
 
-	if (sig_e == State::S0)
+	if (dlatch->type == "$dlatch") {
+		sig_e = assign_map(dlatch->getPort("\\EN"));
+		on_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S1 : State::S0;
+		off_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S0 : State::S1;
+	} else
+	if (dlatch->type == "$_DLATCH_P_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S1;
+		off_state = State::S0;
+	} else
+	if (dlatch->type == "$_DLATCH_N_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S0;
+		off_state = State::S1;
+	} else
+		log_abort();
+
+	if (sig_e == off_state)
 	{
 		RTLIL::Const val_init;
 		for (auto bit : dff_init_map(dlatch->getPort("\\Q")))
@@ -52,7 +70,7 @@ bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 		goto delete_dlatch;
 	}
 
-	if (sig_e == State::S1)
+	if (sig_e == on_state)
 	{
 		mod->connect(dlatch->getPort("\\Q"), dlatch->getPort("\\D"));
 		goto delete_dlatch;
@@ -268,7 +286,7 @@ struct OptRmdffPass : public Pass {
 						"$ff", "$dff", "$adff"))
 					dff_list.push_back(cell->name);
 
-				if (cell->type == "$dlatch")
+				if (cell->type.in("$dlatch", "$_DLATCH_P_", "$_DLATCH_N_"))
 					dlatch_list.push_back(cell->name);
 			}
 

passes/techmap/abc.cc

@@ -29,17 +29,17 @@
 // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025
 // http://en.wikipedia.org/wiki/Topological_sorting
 
-#define ABC_COMMAND_LIB "strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; map {D}"
-#define ABC_COMMAND_CTR "strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
-#define ABC_COMMAND_LUT "strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs"
-#define ABC_COMMAND_SOP "strash; dc2; scorr; ifraig; retime -o; strash; dch -f; cover {I} {P}"
-#define ABC_COMMAND_DFL "strash; dc2; scorr; ifraig; retime -o; strash; dch -f; map"
+#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}"
+#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2"
+#define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}"
+#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map"
 
-#define ABC_FAST_COMMAND_LIB "retime -o {D}; map {D}"
-#define ABC_FAST_COMMAND_CTR "retime -o {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
-#define ABC_FAST_COMMAND_LUT "retime -o; if"
-#define ABC_FAST_COMMAND_SOP "retime -o; cover -I {I} -P {P}"
-#define ABC_FAST_COMMAND_DFL "retime -o; map"
+#define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}"
+#define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_FAST_COMMAND_LUT "strash; dretime; if"
+#define ABC_FAST_COMMAND_SOP "strash; dretime; cover -I {I} -P {P}"
+#define ABC_FAST_COMMAND_DFL "strash; dretime; map"
 
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -595,7 +595,7 @@ struct abc_output_filter
 
 void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
 		std::string liberty_file, std::string constr_file, bool cleanup, vector<int> lut_costs, bool dff_mode, std::string clk_str,
-		bool keepff, std::string delay_target, std::string sop_inputs, std::string sop_products, bool fast_mode,
+		bool keepff, std::string delay_target, std::string sop_inputs, std::string sop_products, std::string lutin_shared, bool fast_mode,
 		const std::vector<RTLIL::Cell*> &cells, bool show_tempdir, bool sop_mode)
 {
 	module = current_module;
@@ -652,7 +652,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 				all_luts_cost_same = false;
 		abc_script += fast_mode ? ABC_FAST_COMMAND_LUT : ABC_COMMAND_LUT;
 		if (all_luts_cost_same && !fast_mode)
-			abc_script += "; lutpack";
+			abc_script += "; lutpack {S}";
 	} else if (!liberty_file.empty())
 		abc_script += constr_file.empty() ? (fast_mode ? ABC_FAST_COMMAND_LIB : ABC_COMMAND_LIB) : (fast_mode ? ABC_FAST_COMMAND_CTR : ABC_COMMAND_CTR);
 	else if (sop_mode)
@@ -660,6 +660,10 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	else
 		abc_script += fast_mode ? ABC_FAST_COMMAND_DFL : ABC_COMMAND_DFL;
 
+	if (script_file.empty() && !delay_target.empty())
+		for (size_t pos = abc_script.find("dretime;"); pos != std::string::npos; pos = abc_script.find("dretime;", pos+1))
+			abc_script = abc_script.substr(0, pos) + "dretime; retime -o {D};" + abc_script.substr(pos+8);
+
 	for (size_t pos = abc_script.find("{D}"); pos != std::string::npos; pos = abc_script.find("{D}", pos))
 		abc_script = abc_script.substr(0, pos) + delay_target + abc_script.substr(pos+3);
 
@@ -669,6 +673,9 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	for (size_t pos = abc_script.find("{P}"); pos != std::string::npos; pos = abc_script.find("{D}", pos))
 		abc_script = abc_script.substr(0, pos) + sop_products + abc_script.substr(pos+3);
 
+	for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
+		abc_script = abc_script.substr(0, pos) + lutin_shared + abc_script.substr(pos+3);
+
 	abc_script += stringf("; write_blif %s/output.blif", tempdir_name.c_str());
 	abc_script = add_echos_to_abc_cmd(abc_script);
 
@@ -1205,7 +1212,7 @@ struct AbcPass : public Pass {
 		log("%s\n", fold_abc_cmd(ABC_COMMAND_CTR).c_str());
 		log("\n");
 		log("        for -lut/-luts (only one LUT size):\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT "; lutpack").c_str());
+		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT "; lutpack {S}").c_str());
 		log("\n");
 		log("        for -lut/-luts (different LUT sizes):\n");
 		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT).c_str());
@@ -1253,6 +1260,8 @@ struct AbcPass : public Pass {
 		log("    -D <picoseconds>\n");
 		log("        set delay target. the string {D} in the default scripts above is\n");
 		log("        replaced by this option when used, and an empty string otherwise.\n");
+		log("        this also replaces 'dretime' with 'dretime; retime -o {D}' in the\n");
+		log("        default scripts above.\n");
 		log("\n");
 		log("    -I <num>\n");
 		log("        maximum number of SOP inputs.\n");
@@ -1262,6 +1271,10 @@ struct AbcPass : public Pass {
 		log("        maximum number of SOP products.\n");
 		log("        (replaces {P} in the default scripts above)\n");
 		log("\n");
+		log("    -S <num>\n");
+		log("        maximum number of LUT inputs shared.\n");
+		log("        (replaces {S} in the default scripts above, default: -S 1)\n");
+		log("\n");
 		log("    -lut <width>\n");
 		log("        generate netlist using luts of (max) the specified width.\n");
 		log("\n");
@@ -1333,7 +1346,7 @@ struct AbcPass : public Pass {
 		std::string exe_file = proc_self_dirname() + "yosys-abc";
 #endif
 		std::string script_file, liberty_file, constr_file, clk_str;
-		std::string delay_target, sop_inputs, sop_products;
+		std::string delay_target, sop_inputs, sop_products, lutin_shared = "-S 1";
 		bool fast_mode = false, dff_mode = false, keepff = false, cleanup = true;
 		bool show_tempdir = false, sop_mode = false;
 		vector<int> lut_costs;
@@ -1393,6 +1406,10 @@ struct AbcPass : public Pass {
 				sop_products = "-P " + args[++argidx];
 				continue;
 			}
+			if (arg == "-S" && argidx+1 < args.size()) {
+				lutin_shared = "-S " + args[++argidx];
+				continue;
+			}
 			if (arg == "-lut" && argidx+1 < args.size()) {
 				string arg = args[++argidx];
 				size_t pos = arg.find_first_of(':');
@@ -1505,7 +1522,7 @@ struct AbcPass : public Pass {
 				log("Skipping module %s as it contains processes.\n", log_id(mod));
 			else if (!dff_mode || !clk_str.empty())
 				abc_module(design, mod, script_file, exe_file, liberty_file, constr_file, cleanup, lut_costs, dff_mode, clk_str, keepff,
-						delay_target, sop_inputs, sop_products, fast_mode, mod->selected_cells(), show_tempdir, sop_mode);
+						delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, mod->selected_cells(), show_tempdir, sop_mode);
 			else
 			{
 				assign_map.set(mod);
@@ -1650,7 +1667,7 @@ struct AbcPass : public Pass {
 					en_polarity = std::get<2>(it.first);
 					en_sig = assign_map(std::get<3>(it.first));
 					abc_module(design, mod, script_file, exe_file, liberty_file, constr_file, cleanup, lut_costs, !clk_sig.empty(), "$",
-							keepff, delay_target, sop_inputs, sop_products, fast_mode, it.second, show_tempdir, sop_mode);
+							keepff, delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode);
 					assign_map.set(mod);
 				}
 			}

techlibs/gowin/cells_sim.v

@@ -1,51 +1,59 @@
 module LUT1(output F, input I0);
-  parameter [1:0] INIT = 0;
-  assign F = I0 ? INIT[1] : INIT[0];
+	parameter [1:0] INIT = 0;
+	assign F = I0 ? INIT[1] : INIT[0];
 endmodule
 
 module LUT2(output F, input I0, I1);
-  parameter [3:0] INIT = 0;
-  wire [ 1: 0] s1 = I1 ? INIT[ 3: 2] : INIT[ 1: 0];
-  assign F = I0 ? s1[1] : s1[0];
+	parameter [3:0] INIT = 0;
+	wire [ 1: 0] s1 = I1 ? INIT[ 3: 2] : INIT[ 1: 0];
+	assign F = I0 ? s1[1] : s1[0];
 endmodule
 
 module LUT3(output F, input I0, I1, I2);
-  parameter [7:0] INIT = 0;
-  wire [ 3: 0] s2 = I2 ? INIT[ 7: 4] : INIT[ 3: 0];
-  wire [ 1: 0] s1 = I1 ?   s2[ 3: 2] :   s2[ 1: 0];
-  assign F = I0 ? s1[1] : s1[0];
+	parameter [7:0] INIT = 0;
+	wire [ 3: 0] s2 = I2 ? INIT[ 7: 4] : INIT[ 3: 0];
+	wire [ 1: 0] s1 = I1 ?   s2[ 3: 2] :   s2[ 1: 0];
+	assign F = I0 ? s1[1] : s1[0];
 endmodule
 
 module LUT4(output F, input I0, I1, I2, I3);
-  parameter [15:0] INIT = 0;
-  wire [ 7: 0] s3 = I3 ? INIT[15: 8] : INIT[ 7: 0];
-  wire [ 3: 0] s2 = I2 ?   s3[ 7: 4] :   s3[ 3: 0];
-  wire [ 1: 0] s1 = I1 ?   s2[ 3: 2] :   s2[ 1: 0];
-  assign F = I0 ? s1[1] : s1[0];
+	parameter [15:0] INIT = 0;
+	wire [ 7: 0] s3 = I3 ? INIT[15: 8] : INIT[ 7: 0];
+	wire [ 3: 0] s2 = I2 ?   s3[ 7: 4] :   s3[ 3: 0];
+	wire [ 1: 0] s1 = I1 ?   s2[ 3: 2] :   s2[ 1: 0];
+	assign F = I0 ? s1[1] : s1[0];
 endmodule
 
 module DFF (output reg Q, input CLK, D);
-	always @(posedge C)
+	parameter [0:0] INIT = 1'b0;
+	initial Q = INIT;
+	always @(posedge CLK)
 		Q <= D;
 endmodule
 
 module DFFN (output reg Q, input CLK, D);
-	always @(negedge C)
+	parameter [0:0] INIT = 1'b0;
+	initial Q = INIT;
+	always @(negedge CLK)
 		Q <= D;
 endmodule
 
 module VCC(output V);
-  assign V = 1;
+	assign V = 1;
 endmodule
 
 module GND(output G);
-  assign G = 0;
+	assign G = 0;
 endmodule
 
 module IBUF(output O, input I);
-  assign O = I;
+	assign O = I;
 endmodule
 
 module OBUF(output O, input I);
-  assign O = I;
+	assign O = I;
+endmodule
+
+module GSR (input GSRI);
+	wire GSRO = GSRI;
 endmodule

techlibs/gowin/synth_gowin.cc

@@ -169,7 +169,7 @@ struct SynthGowinPass : public ScriptPass
 		if (check_label("vout"))
 		{
 			if (!vout_file.empty() || help_mode)
-				run(stringf("write_verilog -attr2comment -defparam -renameprefix gen %s",
+				run(stringf("write_verilog -nodec -attr2comment -defparam -renameprefix gen %s",
 						help_mode ? "<file-name>" : vout_file.c_str()));
 		}
 	}

techlibs/greenpak4/Makefile.inc

@@ -3,6 +3,7 @@ OBJS += techlibs/greenpak4/synth_greenpak4.o
 OBJS += techlibs/greenpak4/greenpak4_counters.o
 OBJS += techlibs/greenpak4/greenpak4_dffinv.o
 
+$(eval $(call add_share_file,share/greenpak4,techlibs/greenpak4/cells_latch.v))
 $(eval $(call add_share_file,share/greenpak4,techlibs/greenpak4/cells_map.v))
 $(eval $(call add_share_file,share/greenpak4,techlibs/greenpak4/cells_sim.v))
 $(eval $(call add_share_file,share/greenpak4,techlibs/greenpak4/gp_dff.lib))

techlibs/greenpak4/cells_latch.v

@@ -0,0 +1,15 @@
+module $_DLATCH_P_(input E, input D, output Q);
+	GP_DLATCH _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(!E),
+		.Q(Q)
+		);
+endmodule
+
+module $_DLATCH_N_(input E, input D, output Q);
+	GP_DLATCH _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(E),
+		.Q(Q)
+		);
+endmodule

techlibs/greenpak4/cells_map.v

@@ -50,6 +50,58 @@ module GP_DFFRI(input D, CLK, nRST, output reg nQ);
 	);
 endmodule
 
+module GP_DLATCHS(input D, nCLK, nSET, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	GP_DLATCHSR #(
+		.INIT(INIT),
+		.SRMODE(1'b1),
+	) _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(nCLK),
+		.nSR(nSET),
+		.Q(Q)
+	);
+endmodule
+
+module GP_DLATCHR(input D, nCLK, nRST, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	GP_DLATCHSR #(
+		.INIT(INIT),
+		.SRMODE(1'b0),
+	) _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(nCLK),
+		.nSR(nRST),
+		.Q(Q)
+	);
+endmodule
+
+module GP_DLATCHSI(input D, nCLK, nSET, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	GP_DLATCHSRI #(
+		.INIT(INIT),
+		.SRMODE(1'b1),
+	) _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(nCLK),
+		.nSR(nSET),
+		.nQ(nQ)
+	);
+endmodule
+
+module GP_DLATCHRI(input D, nCLK, nRST, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	GP_DLATCHSRI #(
+		.INIT(INIT),
+		.SRMODE(1'b0),
+	) _TECHMAP_REPLACE_ (
+		.D(D),
+		.nCLK(nCLK),
+		.nSR(nRST),
+		.nQ(nQ)
+	);
+endmodule
+
 module GP_OBUFT(input IN, input OE, output OUT);
 	GP_IOBUF _TECHMAP_REPLACE_ (
 		.IN(IN),

techlibs/greenpak4/cells_sim.v

@@ -19,6 +19,10 @@ module GP_ABUF(input wire IN, output wire OUT);
 
 	assign OUT = IN;
 
+	//must be 1, 5, 20, 50
+	//values >1 only available with Vdd > 2.7V
+	parameter BANDWIDTH_KHZ = 1;
+
 	//cannot simulate mixed signal IP
 
 endmodule
@@ -45,6 +49,10 @@ module GP_BANDGAP(output reg OK);
 
 endmodule
 
+module GP_CLKBUF(input wire IN, output wire OUT);
+	assign OUT = IN;
+endmodule
+
 module GP_COUNT8(input CLK, input wire RST, output reg OUT);
 
 	parameter RESET_MODE 	= "RISING";
@@ -128,6 +136,61 @@ module GP_DAC(input[7:0] DIN, input wire VREF, output reg VOUT);
 
 endmodule
 
+module GP_DCMP(input[7:0] INP, input[7:0] INN, input CLK, input PWRDN, output reg GREATER, output reg EQUAL);
+	parameter PWRDN_SYNC = 1'b0;
+	parameter CLK_EDGE = "RISING";
+	parameter GREATER_OR_EQUAL = 1'b0;
+
+	//TODO implement power-down mode
+
+	initial GREATER = 0;
+	initial EQUAL = 0;
+
+	wire clk_minv = (CLK_EDGE == "RISING") ? CLK : ~CLK;
+	always @(posedge clk_minv) begin
+		if(GREATER_OR_EQUAL)
+			GREATER <= (INP >= INN);
+		else
+			GREATER <= (INP > INN);
+
+		EQUAL <= (INP == INN);
+	end
+
+endmodule
+
+module GP_DCMPREF(output reg[7:0]OUT);
+	parameter[7:0] REF_VAL = 8'h00;
+	initial OUT = REF_VAL;
+endmodule
+
+module GP_DCMPMUX(input[1:0] SEL, input[7:0] IN0, input[7:0] IN1, input[7:0] IN2, input[7:0] IN3, output reg[7:0] OUTA, output reg[7:0] OUTB);
+
+	always @(*) begin
+		case(SEL)
+			2'd00: begin
+				OUTA <= IN0;
+				OUTB <= IN3;
+			end
+
+			2'd01: begin
+				OUTA <= IN1;
+				OUTB <= IN2;
+			end
+
+			2'd02: begin
+				OUTA <= IN2;
+				OUTB <= IN1;
+			end
+
+			2'd03: begin
+				OUTA <= IN3;
+				OUTB <= IN0;
+			end
+
+		endcase
+	end
+endmodule
+
 module GP_DELAY(input IN, output reg OUT);
 
 	parameter DELAY_STEPS = 1;
@@ -240,6 +303,92 @@ module GP_DFFSRI(input D, CLK, nSR, output reg nQ);
 	end
 endmodule
 
+module GP_DLATCH(input D, input nCLK, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	initial Q = INIT;
+	always @(*) begin
+		if(!nCLK)
+			Q <= D;
+	end
+endmodule
+
+module GP_DLATCHI(input D, input nCLK, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	initial nQ = INIT;
+	always @(*) begin
+		if(!nCLK)
+			nQ <= ~D;
+	end
+endmodule
+
+module GP_DLATCHR(input D, input nCLK, input nRST, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	initial Q = INIT;
+	always @(*) begin
+		if(!nRST)
+			Q <= 1'b0;
+		else if(!nCLK)
+			Q <= D;
+	end
+endmodule
+
+module GP_DLATCHRI(input D, input nCLK, input nRST, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	initial nQ = INIT;
+	always @(*) begin
+		if(!nRST)
+			nQ <= 1'b1;
+		else if(!nCLK)
+			nQ <= ~D;
+	end
+endmodule
+
+module GP_DLATCHS(input D, input nCLK, input nSET, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	initial Q = INIT;
+	always @(*) begin
+		if(!nSET)
+			Q <= 1'b1;
+		else if(!nCLK)
+			Q <= D;
+	end
+endmodule
+
+module GP_DLATCHSI(input D, input nCLK, input nSET, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	initial nQ = INIT;
+	always @(*) begin
+		if(!nSET)
+			nQ <= 1'b0;
+		else if(!nCLK)
+			nQ <= ~D;
+	end
+endmodule
+
+module GP_DLATCHSR(input D, input nCLK, input nSR, output reg Q);
+	parameter [0:0] INIT = 1'bx;
+	parameter[0:0] SRMODE = 1'bx;
+	initial Q = INIT;
+	always @(*) begin
+		if(!nSR)
+			Q <= SRMODE;
+		else if(!nCLK)
+			Q <= D;
+	end
+endmodule
+
+module GP_DLATCHSRI(input D, input nCLK, input nSR, output reg nQ);
+	parameter [0:0] INIT = 1'bx;
+	parameter[0:0] SRMODE = 1'bx;
+	initial nQ = INIT;
+	always @(*) begin
+		if(!nSR)
+			nQ <= ~SRMODE;
+		else if(!nCLK)
+			nQ <= ~D;
+	end
+endmodule
+
 module GP_EDGEDET(input IN, output reg OUT);
 
 	parameter EDGE_DIRECTION = "RISING";
@@ -326,6 +475,10 @@ module GP_PGEN(input wire nRST, input wire CLK, output reg OUT);
 
 endmodule
 
+module GP_PWRDET(output reg VDD_LOW);
+	initial VDD_LOW = 0;
+endmodule
+
 module GP_POR(output reg RST_DONE);
 	parameter POR_TIME = 500;
 
@@ -436,6 +589,32 @@ module GP_SHREG(input nRST, input CLK, input IN, output OUTA, output OUTB);
 
 endmodule
 
+module GP_SPI(
+	input SCK,
+	inout SDAT,
+	input CSN,
+	input[7:0] TXD_HIGH,
+	input[7:0] TXD_LOW,
+	output reg[7:0] RXD_HIGH,
+	output reg[7:0] RXD_LOW,
+	output reg INT);
+
+	initial DOUT_HIGH = 0;
+	initial DOUT_LOW = 0;
+	initial INT = 0;
+
+	parameter DATA_WIDTH = 8;		//byte or word width
+	parameter SPI_CPHA = 0;			//SPI clock phase
+	parameter SPI_CPOL = 0;			//SPI clock polarity
+	parameter DIRECTION = "INPUT";	//SPI data direction (either input to chip or output to host)
+	//parallel output to fabric not yet implemented
+
+	//TODO: write sim model
+	//TODO: SPI SDIO control... can we use ADC output while SPI is input??
+	//TODO: clock sync
+
+endmodule
+
 //keep constraint needed to prevent optimization since we have no outputs
 (* keep *)
 module GP_SYSRESET(input RST);

techlibs/greenpak4/greenpak4_dffinv.cc

@@ -26,6 +26,7 @@ PRIVATE_NAMESPACE_BEGIN
 void invert_gp_dff(Cell *cell, bool invert_input)
 {
 	string cell_type = cell->type.str();
+	bool cell_type_latch = cell_type.find("LATCH") != string::npos;
 	bool cell_type_i = cell_type.find('I') != string::npos;
 	bool cell_type_r = cell_type.find('R') != string::npos;
 	bool cell_type_s = cell_type.find('S') != string::npos;
@@ -79,25 +80,28 @@ void invert_gp_dff(Cell *cell, bool invert_input)
 		cell_type_i = true;
 	}
 
-	cell->type = stringf("\\GP_DFF%s%s%s", cell_type_s ? "S" : "", cell_type_r ? "R" : "", cell_type_i ? "I" : "");
+	if(cell_type_latch)
+		cell->type = stringf("\\GP_DLATCH%s%s%s", cell_type_s ? "S" : "", cell_type_r ? "R" : "", cell_type_i ? "I" : "");
+	else
+		cell->type = stringf("\\GP_DFF%s%s%s", cell_type_s ? "S" : "", cell_type_r ? "R" : "", cell_type_i ? "I" : "");
 
 	log("Merged %s inverter into cell %s.%s: %s -> %s\n", invert_input ? "input" : "output",
 			log_id(cell->module), log_id(cell), cell_type.c_str()+1, log_id(cell->type));
 }
 
 struct Greenpak4DffInvPass : public Pass {
-	Greenpak4DffInvPass() : Pass("greenpak4_dffinv", "merge greenpak4 inverters and DFFs") { }
+	Greenpak4DffInvPass() : Pass("greenpak4_dffinv", "merge greenpak4 inverters and DFF/latches") { }
 	virtual void help()
 	{
 		log("\n");
 		log("    greenpak4_dffinv [options] [selection]\n");
 		log("\n");
-		log("Merge GP_INV cells with GP_DFF* cells.\n");
+		log("Merge GP_INV cells with GP_DFF* and GP_DLATCH* cells.\n");
 		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
-		log_header(design, "Executing GREENPAK4_DFFINV pass (merge synchronous set/reset into FF cells).\n");
+		log_header(design, "Executing GREENPAK4_DFFINV pass (merge input/output inverters into FF/latch cells).\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -120,6 +124,15 @@ struct Greenpak4DffInvPass : public Pass {
 		gp_dff_types.insert("\\GP_DFFSR");
 		gp_dff_types.insert("\\GP_DFFSRI");
 
+		gp_dff_types.insert("\\GP_DLATCH");
+		gp_dff_types.insert("\\GP_DLATCHI");
+		gp_dff_types.insert("\\GP_DLATCHR");
+		gp_dff_types.insert("\\GP_DLATCHRI");
+		gp_dff_types.insert("\\GP_DLATCHS");
+		gp_dff_types.insert("\\GP_DLATCHSI");
+		gp_dff_types.insert("\\GP_DLATCHSR");
+		gp_dff_types.insert("\\GP_DLATCHSRI");
+
 		for (auto module : design->selected_modules())
 		{
 			SigMap sigmap(module);

techlibs/greenpak4/synth_greenpak4.cc

@@ -36,6 +36,8 @@ struct SynthGreenPAK4Pass : public ScriptPass
 		log("    synth_greenpak4 [options]\n");
 		log("\n");
 		log("This command runs synthesis for GreenPAK4 FPGAs. This work is experimental.\n");
+		log("It is intended to be used with https://github.com/azonenberg/openfpga as the\n");
+		log("place-and-route.\n");
 		log("\n");
 		log("    -top <module>\n");
 		log("        use the specified module as top module (default='top')\n");
@@ -159,6 +161,7 @@ struct SynthGreenPAK4Pass : public ScriptPass
 			run("memory_map");
 			run("opt -undriven -fine");
 			run("techmap");
+			run("techmap -map +/greenpak4/cells_latch.v");
 			run("dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib");
 			run("opt -fast");
 			if (retime || help_mode)

tests/simple/arraycells.v

@@ -2,7 +2,7 @@
 module array_test001(a, b, c, y);
 	input a;
 	input [31:0] b, c;
-	input [31:0] y;
+	output [31:0] y;
 
 	aoi12 p [31:0] (a, b, c, y);
 endmodule

tests/simple/hierdefparam.v

@@ -0,0 +1,23 @@
+module hierdefparam_top(input [7:0] A, output [7:0] Y);
+  generate begin:foo
+    hierdefparam_a mod_a(.A(A), .Y(Y));
+  end endgenerate
+  defparam foo.mod_a.bar[0].mod_b.addvalue = 42;
+  defparam foo.mod_a.bar[1].mod_b.addvalue = 43;
+endmodule
+
+module hierdefparam_a(input [7:0] A, output [7:0] Y);
+  genvar i;
+  generate
+    for (i = 0; i < 2; i=i+1) begin:bar
+      wire [7:0] a, y;
+      hierdefparam_b mod_b(.A(a), .Y(y));
+    end
+  endgenerate
+  assign bar[0].a = A, bar[1].a = bar[0].y, Y = bar[1].y;
+endmodule
+
+module hierdefparam_b(input [7:0] A, output [7:0] Y);
+  parameter [7:0] addvalue = 44;
+  assign Y = A + addvalue;
+endmodule

tests/unit/Makefile

@@ -0,0 +1,35 @@
+GTESTFLAG := -lgtest -lgtest_main
+RPATH := -Wl,-rpath
+EXTRAFLAGS := -lyosys -pthreads
+
+OBJTEST := objtest
+BINTEST := bintest
+
+ALLTESTFILE := $(shell find -name '*Test.cc' -printf '%P ')
+TESTDIRS := $(sort $(dir $(ALLTESTFILE)))
+TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o)))
+
+# Prevent make from removing our .o files
+.SECONDARY:
+
+all: prepare $(TESTS) run-tests
+
+$(BINTEST)/%: $(OBJTEST)/%.o
+	$(CXX) -L$(ROOTPATH) $(RPATH)=$(ROOTPATH) -o $@ $^ $(LDLIBS) \
+		$(GTESTFLAG) $(EXTRAFLAGS)
+
+$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc
+	$(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $^
+
+.PHONY: prepare run-tests clean
+
+run-tests: $(TESTS)
+	$(subst Test ,Test; ,$^)
+
+prepare:
+	mkdir -p $(addprefix $(BINTEST)/,$(TESTDIRS))
+	mkdir -p $(addprefix $(OBJTEST)/,$(TESTDIRS))
+
+clean:
+	rm -rf $(OBJTEST)
+	rm -rf $(BINTEST)

tests/unit/kernel/logTest.cc

@@ -0,0 +1,14 @@
+#include <gtest/gtest.h>
+
+#include "kernel/yosys.h"
+#include "kernel/log.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+TEST(KernelLogTest, logvValidValues)
+{
+	//TODO: Implement log test
+	EXPECT_EQ(7, 7);
+}
+
+YOSYS_NAMESPACE_END

tests/unit/kernel/rtlilTest.cc

@@ -0,0 +1,14 @@
+#include <gtest/gtest.h>
+
+#include "kernel/yosys.h"
+#include "kernel/rtlil.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+TEST(KernelRtlilTest, getReferenceValid)
+{
+	//TODO: Implement rtlil test
+	EXPECT_EQ(33, 33);
+}
+
+YOSYS_NAMESPACE_END