Merge pull request #4 from YosysHQ/master

Merge with official repo

31 files changed, 529 insertions, 107 deletions

diff --git a/.gitignore b/.gitignore
index cd624f233..48ce458c7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,8 @@
 *.d
 .*.swp
 *.gch
+*.gcda
+*.gcno
 /.cproject
 /.project
 /.settings
@@ -10,6 +12,8 @@
 /qtcreator.config
 /qtcreator.creator
 /qtcreator.creator.user
+/coverage.info
+/coverage_html
 /Makefile.conf
 /abc
 /viz.js
@@ -30,3 +34,4 @@
 /libyosys.so
 /tests/unit/bintest/
 /tests/unit/objtest/
+/tests/ystests
diff --git a/.travis.yml b/.travis.yml
index fbb4018af..321c3325f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -28,7 +28,6 @@ matrix:
             - tcl-dev
             - libffi-dev
             - git
-            - mercurial
             - graphviz
             - xdot
             - pkg-config
@@ -53,7 +52,6 @@ matrix:
             - tcl-dev
             - libffi-dev
             - git
-            - mercurial
             - graphviz
             - xdot
             - pkg-config
@@ -78,7 +76,6 @@ matrix:
             - tcl-dev
             - libffi-dev
             - git
-            - mercurial
             - graphviz
             - xdot
             - pkg-config
@@ -104,7 +101,6 @@ matrix:
             - tcl-dev
             - libffi-dev
             - git
-            - mercurial
             - graphviz
             - xdot
             - pkg-config
@@ -129,7 +125,6 @@ matrix:
             - tcl-dev
             - libffi-dev
             - git
-            - mercurial
             - graphviz
             - xdot
             - pkg-config
diff --git a/.travis/setup.sh b/.travis/setup.sh
index 81ff37742..068515786 100755
--- a/.travis/setup.sh
+++ b/.travis/setup.sh
@@ -64,7 +64,7 @@ if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then
 		brew tap Homebrew/bundle
 		brew bundle
 		brew install ccache
-		brew install gcc
+		brew install gcc@7
 		echo
 		echo -en 'travis_fold:end:before_install.brew\\r'
 		echo
diff --git a/Brewfile b/Brewfile
index d7cd05bf1..0c58ce161 100644
--- a/Brewfile
+++ b/Brewfile
@@ -3,7 +3,6 @@ brew "flex"
 brew "gawk"
 brew "libffi"
 brew "git"
-brew "mercurial"
 brew "graphviz"
 brew "pkg-config"
 brew "python3"
diff --git a/CHANGELOG b/CHANGELOG
index 01c78ab3b..5499c309a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -3,9 +3,116 @@ List of major changes and improvements between releases
 =======================================================
 
 
-Yosys 0.7 .. Yosys ???
+Yosys 0.7 .. Yosys 0.8
 ----------------------
 
+ * Various
+    - Many bugfixes and small improvements
+    - Strip debug symbols from installed binary
+    - Replace -ignore_redef with -[no]overwrite in front-ends
+    - Added write_verilog hex dump support, add -nohex option
+    - Added "write_verilog -decimal"
+    - Added "scc -set_attr"
+    - Added "verilog_defines" command
+    - Remeber defines from one read_verilog to next
+    - Added support for hierarchical defparam
+    - Added FIRRTL back-end
+    - Improved ABC default scripts
+    - Added "design -reset-vlog"
+    - Added "yosys -W regex", "yosys -w regex", and "yosys -e regex"
+    - Added Verilog $rtoi and $itor support
+    - Added "check -initdrv"
+    - Added "read_blif -wideports"
+    - Added support for systemVerilog "++" and "--" operators
+    - Added support for SystemVerilog unique, unique0, and priority case
+    - Added "write_edif" options for edif "flavors"
+    - Added support for resetall compiler directive
+    - Added simple C beck-end (bitwise combinatorical only atm)
+    - Added $_ANDNOT_ and $_ORNOT_ cell types
+    - Added cell library aliases to "abc -g"
+    - Added "setundef -anyseq"
+    - Added "chtype" command
+    - Added "design -import"
+    - Added "write_table" command
+    - Added "read_json" command
+    - Added "sim" command
+    - Added "extract_fa" and "extract_reduce" commands
+    - Added "extract_counter" command
+    - Added "opt_demorgan" command
+    - Added support for $size and $bits SystemVerilog functions
+    - Added "blackbox" command
+    - Added "ltp" command
+    - Added support for editline as replacement for readline
+    - Added warnings for driver-driver conflicts between FFs (and other cells) and constants
+    - Added "yosys -E" for creating Makefile dependencies files
+    - Added "synth -noshare"
+    - Added "memory_nordff"
+    - Added "setundef -undef -expose -anyconst"
+    - Added "expose -input"
+    - Added specify/specparam parser support (simply ignore them)
+    - Added "write_blif -inames -iattr"
+    - Added "hierarchy -simcheck"
+    - Added an option to statically link abc into yosys
+    - Added protobuf back-end
+    - Added BLIF parsing support for .conn and .cname
+    - Added read_verilog error checking for reg/wire/logic misuse
+    - Added "make coverage" and ENABLE_GCOV build option
+
+ * Changes in Yosys APIs
+    - Added ConstEval defaultval feature
+    - Added {get,set}_src_attribute() methods on RTLIL::AttrObject
+    - Added SigSpec::is_fully_ones() and Const::is_fully_ones()
+    - Added log_file_warning() and log_file_error() functions
+
+ * Formal Verification
+    - Added "write_aiger"
+    - Added "yosys-smtbmc --aig"
+    - Added "always <positive_int>" to .smtc format
+    - Added $cover cell type and support for cover properties
+    - Added $fair/$live cell type and support for liveness properties
+    - Added smtbmc support for memory vcd dumping
+    - Added "chformal" command
+    - Added "write_smt2 -stbv" and "write_smt2 -stdt"
+    - Fix equiv_simple, old behavior now available with "equiv_simple -short"
+    - Change to Yices2 as default SMT solver (it is GPL now)
+    - Added "yosys-smtbmc --presat" (now default in SymbiYosys)
+    - Added "yosys-smtbmc --smtc-init --smtc-top --noinit"
+    - Added a brand new "write_btor" command for BTOR2
+    - Added clk2fflogic memory support and other improvements
+    - Added "async memory write" support to write_smt2
+    - Simulate clock toggling in yosys-smtbmc VCD output
+    - Added $allseq/$allconst cells for EA-solving
+    - Make -nordff the default in "prep"
+    - Added (* gclk *) attribute
+    - Added "async2sync" pass for single-clock designs with async resets
+
+ * Verific support
+    - Many improvements in Verific front-end
+    - Added proper handling of concurent SVA properties
+    - Map "const" and "rand const" to $anyseq/$anyconst
+    - Added "verific -import -flatten" and "verific -import -extnets"
+    - Added "verific -vlog-incdir -vlog-define -vlog-libdir"
+    - Remove PSL support (because PSL has been removed in upstream Verific)
+    - Improve integration with "hierarchy" command design elaboration
+    - Added YOSYS_NOVERIFIC for running non-verific test cases with verific bin
+    - Added simpilied "read" command that automatically uses verific if available
+    - Added "verific -set-<severity> <msg_id>.."
+    - Added "verific -work <libname>"
+
+ * New back-ends
+    - Added initial Coolrunner-II support
+    - Added initial eASIC support
+    - Added initial ECP5 support
+
+ * GreenPAK Support
+    - Added support for GP_DLATCH, GP_SPI, GP_DCMx, GP_COUNTx, etc.
+
+ * iCE40 Support
+    - Add "synth_ice40 -vpr"
+    - Add "synth_ice40 -nodffe"
+    - Add "synth_ice40 -json"
+    - Add Support for UltraPlus cells
+
  * MAX10 and Cyclone IV Support
     - Added initial version of metacommand "synth_intel".
     - Improved write_verilog command to produce VQM netlist for Quartus Prime.
@@ -14,6 +121,7 @@ Yosys 0.7 .. Yosys ???
     - Added example of implementation for DE2i-150 board.
     - Added example of implementation for MAX10 development kit.
     - Added LFSR example from Asic World.
+    - Added "dffinit -highlow" for mapping to Intel primitives
 
 
 Yosys 0.6 .. Yosys 0.7
diff --git a/CodingReadme b/CodingReadme
index 4ab132a63..b64e79178 100644
--- a/CodingReadme
+++ b/CodingReadme
@@ -373,6 +373,7 @@ Finally run all tests with "make config-{clang,gcc,gcc-4.8}":
 	cd ~yosys
 	make clean
 	make test
+	make ystests
 	make vloghtb
 	make install
 
diff --git a/Makefile b/Makefile
index eed4e8f23..365b92ea4 100644
--- a/Makefile
+++ b/Makefile
@@ -19,6 +19,7 @@ ENABLE_LIBYOSYS := 0
 ENABLE_PROTOBUF := 0
 
 # other configuration flags
+ENABLE_GCOV := 0
 ENABLE_GPROF := 0
 ENABLE_DEBUG := 0
 ENABLE_NDEBUG := 0
@@ -156,12 +157,30 @@ LD = gcc
 CXXFLAGS += -std=c++11 -Os
 ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
+else ifeq ($(CONFIG),gcc-static)
+LD = $(CXX)
+LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -static
+LDLIBS := $(filter-out -lrt,$(LDLIBS)) 
+CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
+CXXFLAGS += -std=c++11 -Os
+ABCMKARGS = CC="$(CC)" CXX="$(CXX)" LD="$(LD)" ABC_USE_LIBSTDCXX=1 LIBS="-lm -lpthread -static" OPTFLAGS="-O" \
+                       ARCHFLAGS="-DABC_USE_STDINT_H -DABC_NO_DYNAMIC_LINKING=1 -Wno-unused-but-set-variable $(ARCHFLAGS)" ABC_USE_NO_READLINE=1
+ifeq ($(DISABLE_ABC_THREADS),1)
+ABCMKARGS += "ABC_USE_NO_PTHREADS=1"
+endif
+
 else ifeq ($(CONFIG),gcc-4.8)
 CXX = gcc-4.8
 LD = gcc-4.8
 CXXFLAGS += -std=c++11 -Os
 ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
+else ifeq ($(CONFIG),cygwin)
+CXX = gcc
+LD = gcc
+CXXFLAGS += -std=gnu++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
+
 else ifeq ($(CONFIG),emcc)
 CXX = emcc
 LD = emcc
@@ -300,6 +319,11 @@ endif
 endif
 endif
 
+ifeq ($(ENABLE_GCOV),1)
+CXXFLAGS += --coverage
+LDFLAGS += --coverage
+endif
+
 ifeq ($(ENABLE_GPROF),1)
 CXXFLAGS += -pg
 LDFLAGS += -pg
@@ -567,6 +591,14 @@ vloghtb: $(TARGETS) $(EXTRA_TARGETS)
 	@echo "  Passed \"make vloghtb\"."
 	@echo ""
 
+ystests: $(TARGETS) $(EXTRA_TARGETS)
+	rm -rf tests/ystests
+	git clone https://github.com/YosysHQ/yosys-tests.git tests/ystests
+	+PATH="$$PWD:$$PATH" cd tests/ystests && $(MAKE)
+	@echo ""
+	@echo "  Finished \"make ystests\"."
+	@echo ""
+
 # Unit test
 unit-test: libyosys.so
 	@$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CPPFLAGS="$(CPPFLAGS)" \
@@ -632,6 +664,12 @@ clean-abc:
 mrproper: clean
 	git clean -xdf
 
+coverage:
+	./yosys -qp 'help; help -all'
+	rm -rf coverage.info coverage_html
+	lcov --capture -d . --no-external -o coverage.info
+	genhtml coverage.info --output-directory coverage_html
+
 qtcreator:
 	{ for file in $(basename $(OBJS)); do \
 		for prefix in cc y l; do if [ -f $${file}.$${prefix} ]; then echo $$file.$${prefix}; fi; done \
@@ -671,6 +709,12 @@ config-clang: clean
 config-gcc: clean
 	echo 'CONFIG := gcc' > Makefile.conf
 
+config-gcc-static: clean
+	echo 'CONFIG := gcc-static' > Makefile.conf
+	echo 'ENABLE_PLUGINS := 0' >> Makefile.conf
+	echo 'ENABLE_READLINE := 0' >> Makefile.conf
+	echo 'ENABLE_TCL := 0' >> Makefile.conf
+
 config-gcc-4.8: clean
 	echo 'CONFIG := gcc-4.8' > Makefile.conf
 
@@ -691,6 +735,14 @@ config-msys2: clean
 config-msys2-64: clean
 	echo 'CONFIG := msys2-64' > Makefile.conf
 
+config-cygwin: clean
+	echo 'CONFIG := cygwin' > Makefile.conf
+
+config-gcov: clean
+	echo 'CONFIG := gcc' > Makefile.conf
+	echo 'ENABLE_GCOV := 1' >> Makefile.conf
+	echo 'ENABLE_DEBUG := 1' >> Makefile.conf
+
 config-gprof: clean
 	echo 'CONFIG := gcc' > Makefile.conf
 	echo 'ENABLE_GPROF := 1' >> Makefile.conf
@@ -711,6 +763,6 @@ echo-git-rev:
 -include kernel/*.d
 -include techlibs/*/*.d
 
-.PHONY: all top-all abc test install install-abc manual clean mrproper qtcreator
-.PHONY: config-clean config-clang config-gcc config-gcc-4.8 config-gprof config-sudo
+.PHONY: all top-all abc test install install-abc manual clean mrproper qtcreator coverage vcxsrc mxebin
+.PHONY: config-clean config-clang config-gcc config-gcc-static config-gcc-4.8 config-gprof config-sudo
 
diff --git a/README.md b/README.md
index 424d9bbf2..41ae4ac18 100644
--- a/README.md
+++ b/README.md
@@ -69,6 +69,10 @@ On FreeBSD use the following command to install all prerequisites:
 On FreeBSD system use gmake instead of make. To run tests use:
     % MAKE=gmake CC=cc gmake test
 
+For Cygwin use the following command to install all prerequisites, or select these additional packages:
+
+	setup-x86_64.exe -q --packages=bison,flex,gcc-core,gcc-g++,git,libffi-devel,libreadline-devel,make,pkg-config,python3,tcl-devel
+
 There are also pre-compiled Yosys binary packages for Ubuntu and Win32 as well
 as a source distribution for Visual Studio. Visit the Yosys download page for
 more information: http://www.clifford.at/yosys/download.html
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 4f56f498c..32410a651 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -32,6 +32,27 @@ pool<string> used_names;
 dict<IdString, string> namecache;
 int autoid_counter;
 
+typedef unsigned FDirection;
+static const FDirection FD_NODIRECTION = 0x0;
+static const FDirection FD_IN = 0x1;
+static const FDirection FD_OUT = 0x2;
+static const FDirection FD_INOUT = 0x3;
+
+// Get a port direction with respect to a specific module.
+FDirection getPortFDirection(IdString id, Module *module)
+{
+	Wire *wire = module->wires_.at(id);
+	FDirection direction = FD_NODIRECTION;
+	if (wire && wire->port_id)
+	{
+		if (wire->port_input)
+			direction |= FD_IN;
+		if (wire->port_output)
+			direction |= FD_OUT;
+	}
+	return direction;
+}
+
 string next_id()
 {
 	string new_id;
@@ -77,6 +98,8 @@ struct FirrtlWorker
 
 	dict<SigBit, pair<string, int>> reverse_wire_map;
 	string unconn_id;
+	RTLIL::Design *design;
+	std::string indent;
 
 	void register_reverse_wire_map(string id, SigSpec sig)
 	{
@@ -84,11 +107,11 @@ struct FirrtlWorker
 			reverse_wire_map[sig[i]] = make_pair(id, i);
 	}
 
-	FirrtlWorker(Module *module, std::ostream &f) : module(module), f(f)
+	FirrtlWorker(Module *module, std::ostream &f, RTLIL::Design *theDesign) : module(module), f(f), design(theDesign), indent("    ")
 	{
 	}
 
-	string make_expr(SigSpec sig)
+	string make_expr(const SigSpec &sig)
 	{
 		string expr;
 
@@ -135,6 +158,65 @@ struct FirrtlWorker
 		return expr;
 	}
 
+	std::string fid(RTLIL::IdString internal_id)
+	{
+		const char *str = internal_id.c_str();
+		return *str == '\\' ? str + 1 : str;
+	}
+
+
+	std::string cellname(RTLIL::Cell *cell)
+	{
+		return fid(cell->name).c_str();
+	}
+
+	void process_instance(RTLIL::Cell *cell, vector<string> &wire_exprs)
+	{
+		std::string cell_type = fid(cell->type);
+
+		std::string cell_name = cellname(cell);
+		std::string cell_name_comment;
+		if (cell_name != fid(cell->name))
+			cell_name_comment = " /* " + fid(cell->name) + " */ ";
+		else
+			cell_name_comment = "";
+		// Find the module corresponding to this instance.
+		auto instModule = design->module(cell->type);
+		wire_exprs.push_back(stringf("%s" "inst %s%s of %s", indent.c_str(), cell_name.c_str(), cell_name_comment.c_str(), cell_type.c_str()));
+
+		for (auto it = cell->connections().begin(); it != cell->connections().end(); ++it) {
+			if (it->second.size() > 0) {
+				const SigSpec &secondSig = it->second;
+				const std::string firstName = cell_name + "." + make_id(it->first);
+				const std::string secondName = make_expr(secondSig);
+				// Find the direction for this port.
+				FDirection dir = getPortFDirection(it->first, instModule);
+				std::string source, sink;
+				switch (dir) {
+					case FD_INOUT:
+						log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", log_id(cell_type), log_signal(it->second));
+					case FD_OUT:
+						source = firstName;
+						sink = secondName;
+						break;
+					case FD_NODIRECTION:
+						log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", log_id(cell_type), log_signal(it->second));
+						/* FALL_THROUGH */
+					case FD_IN:
+						source = secondName;
+						sink = firstName;
+						break;
+					default:
+						log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", log_id(cell_type), log_signal(it->second), dir);
+						break;
+				}
+				wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sink.c_str(), source.c_str()));
+			}
+		}
+		wire_exprs.push_back(stringf("\n"));
+
+	}
+
 	void run()
 	{
 		f << stringf("  module %s:\n", make_id(module->name));
@@ -142,21 +224,28 @@ struct FirrtlWorker
 
 		for (auto wire : module->wires())
 		{
+			const auto wireName = make_id(wire->name);
 			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));
+						wireName, wire->width));
 			}
 			else
 			{
-				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", make_id(wire->name), wire->width));
+				wire_decls.push_back(stringf("    wire %s: UInt<%d>\n", wireName, wire->width));
 			}
 		}
 
 		for (auto cell : module->cells())
 		{
+		  // Is this cell is a module instance?
+			if (cell->type[0] != '$')
+			{
+				process_instance(cell, wire_exprs);
+				continue;
+			}
 			if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
 			{
 				string y_id = make_id(cell->name);
@@ -169,7 +258,10 @@ struct FirrtlWorker
 					a_expr = "asSInt(" + a_expr + ")";
 				}
 
-				a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+				// Don't use the results of logical operations (a single bit) to control padding
+				if (!(cell->type.in("$eq", "$eqx", "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$reduce_bool", "$logic_not") && y_width == 1) ) {
+					a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
+				}
 
 				string primop;
                                 bool always_uint = false;
@@ -187,9 +279,12 @@ struct FirrtlWorker
                                         a_expr = stringf("xorr(%s)", a_expr.c_str());
                                 }
 				if (cell->type == "$reduce_bool") {
-                                        primop = "neq";
-                                        a_expr = stringf("%s, UInt(0)", a_expr.c_str());
-                                }
+					primop = "neq";
+					// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
+					bool a_signed = cell->parameters.at("\\A_SIGNED").as_bool();
+					int a_width =  cell->parameters.at("\\A_WIDTH").as_int();
+					a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
+				}
 
 				string expr = stringf("%s(%s)", primop.c_str(), a_expr.c_str());
 
@@ -215,16 +310,16 @@ struct FirrtlWorker
 				if (cell->parameters.at("\\A_SIGNED").as_bool()) {
 					a_expr = "asSInt(" + a_expr + ")";
 				}
-				if (cell->parameters.at("\\A_SIGNED").as_bool()  & (cell->type != "$shr")) {
-					b_expr = "asSInt(" + b_expr + ")";
+				// Shift amount is always unsigned, and needn't be padded to result width.
+				if (!cell->type.in("$shr", "$sshr", "$shl", "$sshl")) {
+					if (cell->parameters.at("\\B_SIGNED").as_bool()) {
+						b_expr = "asSInt(" + b_expr + ")";
+					}
+					b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
 				}
 
 				a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
 
-				if ((cell->type != "$shl") && (cell->type != "$sshl")) {
-				        b_expr = stringf("pad(%s, %d)", b_expr.c_str(), y_width);
-                                }
-
 				if (cell->parameters.at("\\A_SIGNED").as_bool()  & (cell->type == "$shr")) {
 					a_expr = "asUInt(" + a_expr + ")";
 				}
@@ -494,14 +589,14 @@ struct FirrtlWorker
 			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_decls.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)));
+				wire_decls.push_back(stringf("    %s is invalid\n", make_id(wire->name)));
 			}
 		}
 
@@ -570,7 +665,7 @@ struct FirrtlBackend : public Backend {
 
 		for (auto module : design->modules())
 		{
-			FirrtlWorker worker(module, *f);
+			FirrtlWorker worker(module, *f, design);
 			worker.run();
 		}
 
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 44e4e5f97..ae9031510 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -779,6 +779,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
+	if (cell->type == "$lut")
+	{
+		f << stringf("%s" "assign ", indent.c_str());
+		dump_sigspec(f, cell->getPort("\\Y"));
+		f << stringf(" = ");
+		dump_const(f, cell->parameters.at("\\LUT"));
+		f << stringf(" >> ");
+		dump_attributes(f, "", cell->attributes, ' ');
+		dump_sigspec(f, cell->getPort("\\A"));
+		f << stringf(";\n");
+		return true;
+	}
+
 	if (cell->type == "$dffsr")
 	{
 		SigSpec sig_clk = cell->getPort("\\CLK");
@@ -1510,7 +1523,7 @@ struct VerilogBackend : public Backend {
 		log("\n");
 		log("    -nodec\n");
 		log("        32-bit constant values are by default dumped as decimal numbers,\n");
-		log("        not bit pattern. This option decativates this feature and instead\n");
+		log("        not bit pattern. This option deactivates this feature and instead\n");
 		log("        will write out all constants in binary.\n");
 		log("\n");
 		log("    -decimal\n");
@@ -1518,13 +1531,13 @@ struct VerilogBackend : public Backend {
 		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("        dumped as hex values. This option deactivates 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");
-		log("        decativates this feature and instead will write string constants\n");
+		log("        deactivates this feature and instead will write string constants\n");
 		log("        as binary numbers.\n");
 		log("\n");
 		log("    -defparam\n");
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 7c72a50d9..e79be953a 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -44,7 +44,7 @@ namespace AST {
 
 // instanciate global variables (private API)
 namespace AST_INTERNAL {
-	bool flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
+	bool flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
 	bool flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire;
 	AstNode *current_ast, *current_ast_mod;
 	std::map<std::string, AstNode*> current_scope;
@@ -267,10 +267,12 @@ void AstNode::dumpAst(FILE *f, std::string indent) const
 	std::string type_name = type2str(type);
 	fprintf(f, "%s%s <%s:%d>", indent.c_str(), type_name.c_str(), filename.c_str(), linenum);
 
-	if (id2ast)
-		fprintf(f, " [%p -> %p]", this, id2ast);
-	else
-		fprintf(f, " [%p]", this);
+	if (!flag_no_dump_ptr) {
+		if (id2ast)
+			fprintf(f, " [%p -> %p]", this, id2ast);
+		else
+			fprintf(f, " [%p]", this);
+	}
 
 	if (!str.empty())
 		fprintf(f, " str='%s'", str.c_str());
@@ -1008,12 +1010,13 @@ static AstModule* process_module(AstNode *ast, bool defer)
 }
 
 // create AstModule instances for all modules in the AST tree and add them to 'design'
-void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool dump_rtlil,
+void AST::process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog, bool dump_rtlil,
 		bool nolatches, bool nomeminit, bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool nooverwrite, bool overwrite, bool defer, bool autowire)
 {
 	current_ast = ast;
 	flag_dump_ast1 = dump_ast1;
 	flag_dump_ast2 = dump_ast2;
+	flag_no_dump_ptr = no_dump_ptr;
 	flag_dump_vlog = dump_vlog;
 	flag_dump_rtlil = dump_rtlil;
 	flag_nolatches = nolatches;
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index d94199643..7e97bdb3b 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -274,7 +274,7 @@ namespace AST
 	};
 
 	// process an AST tree (ast must point to an AST_DESIGN node) and generate RTLIL code
-	void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool dump_vlog, bool dump_rtlil, bool nolatches, bool nomeminit,
+	void process(RTLIL::Design *design, AstNode *ast, bool dump_ast1, bool dump_ast2, bool no_dump_ptr, bool dump_vlog, bool dump_rtlil, bool nolatches, bool nomeminit,
 			bool nomem2reg, bool mem2reg, bool lib, bool noopt, bool icells, bool nooverwrite, bool overwrite, bool defer, bool autowire);
 
 	// parametric modules are supported directly by the AST library
@@ -305,7 +305,7 @@ namespace AST
 namespace AST_INTERNAL
 {
 	// internal state variables
-	extern bool flag_dump_ast1, flag_dump_ast2, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
+	extern bool flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_rtlil, flag_nolatches, flag_nomeminit;
 	extern bool flag_nomem2reg, flag_mem2reg, flag_lib, flag_noopt, flag_icells, flag_autowire;
 	extern AST::AstNode *current_ast, *current_ast_mod;
 	extern std::map<std::string, AST::AstNode*> current_scope;
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 04c429f7f..aa3b982d8 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1781,7 +1781,7 @@ skip_dynamic_range_lvalue_expansion:;
 				if (GetSize(children) == 2)
 				{
 					AstNode *buf = children[1]->clone();
-					while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { }
+					while (buf->simplify(true, false, false, stage, -1, false, false)) { }
 					if (buf->type != AST_CONSTANT)
 						log_file_error(filename, linenum, "Failed to evaluate system function `%s' with non-constant value.\n", str.c_str());
 
diff --git a/frontends/ilang/.gitignore b/frontends/ilang/.gitignore
index 43106a814..f586b33c7 100644
--- a/frontends/ilang/.gitignore
+++ b/frontends/ilang/.gitignore
@@ -1,4 +1,4 @@
 ilang_lexer.cc
 ilang_parser.output
 ilang_parser.tab.cc
-ilang_parser.tab.h
+ilang_parser.tab.hh
diff --git a/frontends/ilang/Makefile.inc b/frontends/ilang/Makefile.inc
index e2a476c93..6f1f0e8fc 100644
--- a/frontends/ilang/Makefile.inc
+++ b/frontends/ilang/Makefile.inc
@@ -1,15 +1,14 @@
 
 GENFILES += frontends/ilang/ilang_parser.tab.cc
-GENFILES += frontends/ilang/ilang_parser.tab.h
+GENFILES += frontends/ilang/ilang_parser.tab.hh
 GENFILES += frontends/ilang/ilang_parser.output
 GENFILES += frontends/ilang/ilang_lexer.cc
 
 frontends/ilang/ilang_parser.tab.cc: frontends/ilang/ilang_parser.y
 	$(Q) mkdir -p $(dir $@)
-	$(P) $(BISON) -d -r all -b frontends/ilang/ilang_parser $<
-	$(Q) mv frontends/ilang/ilang_parser.tab.c frontends/ilang/ilang_parser.tab.cc
+	$(P) $(BISON) -o $@ -d -r all -b frontends/ilang/ilang_parser $<
 
-frontends/ilang/ilang_parser.tab.h: frontends/ilang/ilang_parser.tab.cc
+frontends/ilang/ilang_parser.tab.hh: frontends/ilang/ilang_parser.tab.cc
 
 frontends/ilang/ilang_lexer.cc: frontends/ilang/ilang_lexer.l
 	$(Q) mkdir -p $(dir $@)
diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l
index 842388548..d8e01ae4d 100644
--- a/frontends/ilang/ilang_lexer.l
+++ b/frontends/ilang/ilang_lexer.l
@@ -30,7 +30,7 @@
 #endif
 
 #include "frontends/ilang/ilang_frontend.h"
-#include "ilang_parser.tab.h"
+#include "ilang_parser.tab.hh"
 
 USING_YOSYS_NAMESPACE
 
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index b8c0375ce..c5fa58313 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -64,6 +64,7 @@ YOSYS_NAMESPACE_BEGIN
 int verific_verbose;
 bool verific_import_pending;
 string verific_error_msg;
+int verific_sva_fsm_limit;
 
 vector<string> verific_incdirs, verific_libdirs;
 
@@ -1618,6 +1619,8 @@ struct VerificExtNets
 
 void verific_import(Design *design, std::string top)
 {
+	verific_sva_fsm_limit = 16;
+
 	std::set<Netlist*> nl_todo, nl_done;
 
 	{
@@ -1706,11 +1709,18 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
 		log("\n");
+		log("\n");
 		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
 		log("\n");
+		log("    verific -work <libname> {-sv|-vhdl|...} <hdl-file>\n");
+		log("\n");
+		log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
+		log("(default library when -work is not present: \"work\")\n");
+		log("\n");
+		log("\n");
 		log("    verific -vlog-incdir <directory>..\n");
 		log("\n");
 		log("Add Verilog include directories.\n");
@@ -1782,6 +1792,9 @@ struct VerificPass : public Pass {
 		log("  -nosva\n");
 		log("    Ignore SVA properties, do not infer checker logic.\n");
 		log("\n");
+		log("  -L <int>\n");
+		log("    Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+		log("\n");
 		log("  -n\n");
 		log("    Keep all Verific names on instances and nets. By default only\n");
 		log("    user-declared names are preserved.\n");
@@ -1823,6 +1836,7 @@ struct VerificPass : public Pass {
 		}
 
 		verific_verbose = 0;
+		verific_sva_fsm_limit = 16;
 
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
@@ -1837,6 +1851,7 @@ struct VerificPass : public Pass {
 		log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
 
 		int argidx = 1;
+		std::string work = "work";
 
 		if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
 				args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
@@ -1895,6 +1910,15 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
+		for (; argidx < GetSize(args); argidx++)
+		{
+			if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
+				work = args[++argidx];
+				continue;
+			}
+			break;
+		}
+
 		if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
 				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
 		{
@@ -1942,7 +1966,7 @@ struct VerificPass : public Pass {
 			while (argidx < GetSize(args))
 				file_names.Insert(args[argidx++].c_str());
 
-			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
+			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
 					log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
 
 			verific_import_pending = true;
@@ -1952,7 +1976,7 @@ struct VerificPass : public Pass {
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
 			for (argidx++; argidx < GetSize(args); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
 					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
 			verific_import_pending = true;
 			goto check_error;
@@ -1961,7 +1985,7 @@ struct VerificPass : public Pass {
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
 			for (argidx++; argidx < GetSize(args); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
 					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
 			verific_import_pending = true;
 			goto check_error;
@@ -1970,7 +1994,7 @@ struct VerificPass : public Pass {
 		if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
 			for (argidx++; argidx < GetSize(args); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
 					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
 			verific_import_pending = true;
 			goto check_error;
@@ -1979,7 +2003,7 @@ struct VerificPass : public Pass {
 		if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
 			for (argidx++; argidx < GetSize(args); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
 					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
 			verific_import_pending = true;
 			goto check_error;
@@ -2019,6 +2043,10 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
+				if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+					verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+					continue;
+				}
 				if (args[argidx] == "-n") {
 					mode_names = true;
 					continue;
@@ -2089,8 +2117,8 @@ struct VerificPass : public Pass {
 #else
 				log("Running hier_tree::ElaborateAll().\n");
 
-				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
-				VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+				VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
 
 				Array veri_libs, vhdl_libs;
 				if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
@@ -2137,7 +2165,7 @@ struct VerificPass : public Pass {
 						continue;
 					}
 
-					VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+					VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
 					VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
 					if (vhdl_unit) {
 						log("Adding VHDL unit '%s' to elaboration queue.\n", name);
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index cbd9314db..334a436af 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -101,6 +101,8 @@ void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst
 void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
 bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
 
+extern int verific_sva_fsm_limit;
+
 YOSYS_NAMESPACE_END
 
 #endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 85b842186..cdc9ece8c 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -466,13 +466,14 @@ struct SvaFsm
 
 		dnode.ctrl.sort_and_unify();
 
-		if (GetSize(dnode.ctrl) > 16) {
+		if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
 			if (verific_verbose >= 2) {
 				log("    detected state explosion in DFSM generation:\n");
 				dump();
 				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
 			}
-			log_error("SVA DFSM state ctrl signal has %d (>16) bits. Stopping to prevent exponential design size explosion.\n", GetSize(dnode.ctrl));
+			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
+					GetSize(dnode.ctrl), verific_sva_fsm_limit);
 		}
 
 		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
diff --git a/frontends/verilog/.gitignore b/frontends/verilog/.gitignore
index 1d4ae9e5c..aadbcdcdd 100644
--- a/frontends/verilog/.gitignore
+++ b/frontends/verilog/.gitignore
@@ -1,4 +1,4 @@
 verilog_lexer.cc
 verilog_parser.output
 verilog_parser.tab.cc
-verilog_parser.tab.h
+verilog_parser.tab.hh
diff --git a/frontends/verilog/Makefile.inc b/frontends/verilog/Makefile.inc
index a06c1d5ab..dbaace585 100644
--- a/frontends/verilog/Makefile.inc
+++ b/frontends/verilog/Makefile.inc
@@ -1,15 +1,14 @@
 
 GENFILES += frontends/verilog/verilog_parser.tab.cc
-GENFILES += frontends/verilog/verilog_parser.tab.h
+GENFILES += frontends/verilog/verilog_parser.tab.hh
 GENFILES += frontends/verilog/verilog_parser.output
 GENFILES += frontends/verilog/verilog_lexer.cc
 
 frontends/verilog/verilog_parser.tab.cc: frontends/verilog/verilog_parser.y
 	$(Q) mkdir -p $(dir $@)
-	$(P) $(BISON) -d -r all -b frontends/verilog/verilog_parser $<
-	$(Q) mv frontends/verilog/verilog_parser.tab.c frontends/verilog/verilog_parser.tab.cc
+	$(P) $(BISON) -o $@ -d -r all -b frontends/verilog/verilog_parser $<
 
-frontends/verilog/verilog_parser.tab.h: frontends/verilog/verilog_parser.tab.cc
+frontends/verilog/verilog_parser.tab.hh: frontends/verilog/verilog_parser.tab.cc
 
 frontends/verilog/verilog_lexer.cc: frontends/verilog/verilog_lexer.l
 	$(Q) mkdir -p $(dir $@)
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 911e36112..aeea36a2b 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -66,18 +66,30 @@ struct VerilogFrontend : public Frontend {
 		log("        enable support for SystemVerilog assertions and some Yosys extensions\n");
 		log("        replace the implicit -D SYNTHESIS with -D FORMAL\n");
 		log("\n");
+		log("    -noassert\n");
+		log("        ignore assert() statements\n");
+		log("\n");
+		log("    -noassume\n");
+		log("        ignore assume() statements\n");
+		log("\n");
 		log("    -norestrict\n");
-		log("        ignore restrict() assertions\n");
+		log("        ignore restrict() statements\n");
 		log("\n");
 		log("    -assume-asserts\n");
 		log("        treat all assert() statements like assume() statements\n");
 		log("\n");
+		log("    -assert-assumes\n");
+		log("        treat all assume() statements like assert() statements\n");
+		log("\n");
 		log("    -dump_ast1\n");
 		log("        dump abstract syntax tree (before simplification)\n");
 		log("\n");
 		log("    -dump_ast2\n");
 		log("        dump abstract syntax tree (after simplification)\n");
 		log("\n");
+		log("    -no_dump_ptr\n");
+		log("        do not include hex memory addresses in dump (easier to diff dumps)\n");
+		log("\n");
 		log("    -dump_vlog\n");
 		log("        dump ast as Verilog code (after simplification)\n");
 		log("\n");
@@ -184,6 +196,7 @@ struct VerilogFrontend : public Frontend {
 	{
 		bool flag_dump_ast1 = false;
 		bool flag_dump_ast2 = false;
+		bool flag_no_dump_ptr = false;
 		bool flag_dump_vlog = false;
 		bool flag_dump_rtlil = false;
 		bool flag_nolatches = false;
@@ -225,6 +238,14 @@ struct VerilogFrontend : public Frontend {
 				formal_mode = true;
 				continue;
 			}
+			if (arg == "-noassert") {
+				noassert_mode = true;
+				continue;
+			}
+			if (arg == "-noassume") {
+				noassume_mode = true;
+				continue;
+			}
 			if (arg == "-norestrict") {
 				norestrict_mode = true;
 				continue;
@@ -233,6 +254,10 @@ struct VerilogFrontend : public Frontend {
 				assume_asserts_mode = true;
 				continue;
 			}
+			if (arg == "-assert-assumes") {
+				assert_assumes_mode = true;
+				continue;
+			}
 			if (arg == "-dump_ast1") {
 				flag_dump_ast1 = true;
 				continue;
@@ -241,6 +266,10 @@ struct VerilogFrontend : public Frontend {
 				flag_dump_ast2 = true;
 				continue;
 			}
+			if (arg == "-no_dump_ptr") {
+				flag_no_dump_ptr = true;
+				continue;
+			}
 			if (arg == "-dump_vlog") {
 				flag_dump_vlog = true;
 				continue;
@@ -381,7 +410,7 @@ struct VerilogFrontend : public Frontend {
 		if (flag_nodpi)
 			error_on_dpi_function(current_ast);
 
-		AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire);
+		AST::process(design, current_ast, flag_dump_ast1, flag_dump_ast2, flag_no_dump_ptr, flag_dump_vlog, flag_dump_rtlil, flag_nolatches, flag_nomeminit, flag_nomem2reg, flag_mem2reg, lib_mode, flag_noopt, flag_icells, flag_nooverwrite, flag_overwrite, flag_defer, default_nettype_wire);
 
 		if (!flag_nopp)
 			delete lexin;
diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 16edc7985..523bbc897 100644
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -54,12 +54,21 @@ namespace VERILOG_FRONTEND
 	// running in -formal mode
 	extern bool formal_mode;
 
+	// running in -noassert mode
+	extern bool noassert_mode;
+
+	// running in -noassume mode
+	extern bool noassume_mode;
+
 	// running in -norestrict mode
 	extern bool norestrict_mode;
 
 	// running in -assume-asserts mode
 	extern bool assume_asserts_mode;
 
+	// running in -assert-assumes mode
+	extern bool assert_assumes_mode;
+
 	// running in -lib mode
 	extern bool lib_mode;
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 0134416c1..83921bf0b 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -42,7 +42,7 @@
 #include "kernel/log.h"
 #include "frontends/verilog/verilog_frontend.h"
 #include "frontends/ast/ast.h"
-#include "verilog_parser.tab.h"
+#include "verilog_parser.tab.hh"
 
 USING_YOSYS_NAMESPACE
 using namespace AST;
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 78cac5543..16cac1460 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -58,7 +58,8 @@ namespace VERILOG_FRONTEND {
 	bool do_not_require_port_stubs;
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
-	bool norestrict_mode, assume_asserts_mode;
+	bool noassert_mode, noassume_mode, norestrict_mode;
+	bool assume_asserts_mode, assert_assumes_mode;
 	bool current_wire_rand, current_wire_const;
 	std::istream *lexin;
 }
@@ -654,7 +655,7 @@ specify_item:
 	// | pulsestyle_declaration
 	// | showcancelled_declaration
 	| path_declaration
-	// | system_timing_declaration
+	| system_timing_declaration
 	;
 
 specparam_declaration:
@@ -682,22 +683,23 @@ showcancelled_declaration :
 */
 
 path_declaration :
-	simple_path_declaration
+	simple_path_declaration ';'
 	// | edge_sensitive_path_declaration
 	// | state_dependent_path_declaration
 	;
 
 simple_path_declaration :
-	parallel_path_description '=' path_delay_value ';'
-	// | full_path_description '=' path_delay_value ';'
+	parallel_path_description '=' path_delay_value |
+	full_path_description '=' path_delay_value
 	;
 
 path_delay_value :
-	//list_of_path_delay_expressions
-	'(' list_of_path_delay_expressions ')'
+	'(' path_delay_expression list_of_path_delay_extra_expressions ')'
+	|     path_delay_expression
+	|     path_delay_expression list_of_path_delay_extra_expressions
 	;
 
-list_of_path_delay_expressions :
+list_of_path_delay_extra_expressions :
 /*
 	t_path_delay_expression
 	| trise_path_delay_expression ',' tfall_path_delay_expression
@@ -709,12 +711,11 @@ list_of_path_delay_expressions :
 	  t0x_path_delay_expression ',' tx1_path_delay_expression ',' t1x_path_delay_expression ','
 	  tx0_path_delay_expression ',' txz_path_delay_expression ',' tzx_path_delay_expression
 */
-	path_delay_expression
-	| path_delay_expression ',' path_delay_expression
-	| path_delay_expression ',' path_delay_expression ',' path_delay_expression
-	| path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
+	',' path_delay_expression
+	|  ',' path_delay_expression ',' path_delay_expression
+	|  ',' path_delay_expression ',' path_delay_expression ','
 	  path_delay_expression ',' path_delay_expression ',' path_delay_expression
-	| path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
+	|  ',' path_delay_expression ',' path_delay_expression ','
 	  path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
 	  path_delay_expression ',' path_delay_expression ',' path_delay_expression ','
 	  path_delay_expression ',' path_delay_expression ',' path_delay_expression
@@ -723,6 +724,22 @@ list_of_path_delay_expressions :
 parallel_path_description :
 	'(' specify_input_terminal_descriptor opt_polarity_operator '=' '>' specify_output_terminal_descriptor ')' ;
 
+full_path_description :
+	'(' list_of_path_inputs '*' '>' list_of_path_outputs ')' ;
+
+// This was broken into 2 rules to solve shift/reduce conflicts
+list_of_path_inputs :
+	specify_input_terminal_descriptor                  opt_polarity_operator  |
+	specify_input_terminal_descriptor more_path_inputs opt_polarity_operator ;
+
+more_path_inputs :
+    ',' specify_input_terminal_descriptor |
+    more_path_inputs ',' specify_input_terminal_descriptor ;
+
+list_of_path_outputs :
+	specify_output_terminal_descriptor |
+	list_of_path_outputs ',' specify_output_terminal_descriptor ;
+	
 opt_polarity_operator :
 	'+'
 	| '-'
@@ -736,11 +753,18 @@ specify_input_terminal_descriptor :
 specify_output_terminal_descriptor :
 	TOK_ID ;
 
-/*
 system_timing_declaration :
-	;
-*/
+	TOK_ID '(' system_timing_args ')' ';' ;
+
+system_timing_arg :
+	TOK_POSEDGE TOK_ID |
+	TOK_NEGEDGE TOK_ID |
+	expr ;
 
+system_timing_args :
+	system_timing_arg |
+	system_timing_args ',' system_timing_arg ;
+ 
 /*
 t_path_delay_expression :
 	path_delay_expression;
@@ -792,7 +816,7 @@ tzx_path_delay_expression :
 */
 
 path_delay_expression :
-	constant_mintypmax_expression;
+	constant_expression;
 
 constant_mintypmax_expression :
 	constant_expression
@@ -858,9 +882,15 @@ param_decl_list:
 
 single_param_decl:
 	TOK_ID '=' expr {
-		if (astbuf1 == nullptr)
-			frontend_verilog_yyerror("syntax error");
-		AstNode *node = astbuf1->clone();
+		AstNode *node;
+		if (astbuf1 == nullptr) {
+			if (!sv_mode)
+				frontend_verilog_yyerror("syntax error");
+			node = new AstNode(AST_PARAMETER);
+			node->children.push_back(AstNode::mkconst_int(0, true));
+		} else {
+			node = astbuf1->clone();
+		}
 		node->str = *$1;
 		delete node->children[0];
 		node->children[0] = $3;
@@ -1252,16 +1282,28 @@ opt_stmt_label:
 
 assert:
 	opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
+		if (noassert_mode)
+			delete $5;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5));
 	} |
 	opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5));
+		if (noassume_mode)
+			delete $5;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5));
 	} |
 	opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
+		if (noassert_mode)
+			delete $6;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6));
 	} |
 	opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' {
-		ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6));
+		if (noassume_mode)
+			delete $6;
+		else
+			ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6));
 	} |
 	opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5));
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index 264b1f63d..ad032899c 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -166,7 +166,7 @@ std::string vstringf(const char *fmt, va_list ap)
 	std::string string;
 	char *str = NULL;
 
-#ifdef _WIN32
+#if defined(_WIN32 )|| defined(__CYGWIN__) 
 	int sz = 64, rc;
 	while (1) {
 		va_list apc;
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 8af8ccdd0..fea2354e6 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -4421,13 +4421,13 @@ Write the current design to a Verilog file.
 
     -nodec
         32-bit constant values are by default dumped as decimal numbers,
-        not bit pattern. This option decativates this feature and instead
+        not bit pattern. This option deactivates this feature and instead
         will write out all constants in binary.
 
     -nostr
         Parameters and attributes that are specified as strings in the
         original input will be output as strings by this back-end. This
-        decativates this feature and instead will write string constants
+        deactivates this feature and instead will write string constants
         as binary numbers.
 
     -defparam
diff --git a/misc/create_vcxsrc.sh b/misc/create_vcxsrc.sh
index 215e27c53..924d2722e 100644
--- a/misc/create_vcxsrc.sh
+++ b/misc/create_vcxsrc.sh
@@ -5,11 +5,11 @@ vcxsrc="$1-$2"
 yosysver="$2"
 gitsha="$3"
 
-rm -rf YosysVS-Tpl-v1.zip YosysVS
-wget http://www.clifford.at/yosys/nogit/YosysVS-Tpl-v1.zip
+rm -rf YosysVS-Tpl-v2.zip YosysVS
+wget http://www.clifford.at/yosys/nogit/YosysVS-Tpl-v2.zip
 
-unzip YosysVS-Tpl-v1.zip
-rm -f YosysVS-Tpl-v1.zip
+unzip YosysVS-Tpl-v2.zip
+rm -f YosysVS-Tpl-v2.zip
 mv YosysVS "$vcxsrc"
 
 {
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index ec04418fa..a48873244 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -584,6 +584,7 @@ struct ShowPass : public Pass {
 		log("\n");
 		log("    -viewer <viewer>\n");
 		log("        Run the specified command with the graphics file as parameter.\n");
+		log("        On Windows, this pauses yosys until the viewer exits.\n");
 		log("\n");
 		log("    -format <format>\n");
 		log("        Generate a graphics file in the specified format. Use 'dot' to just\n");
@@ -645,7 +646,7 @@ struct ShowPass : public Pass {
 		log("        do not add the module name as graph title to the dot file\n");
 		log("\n");
 		log("When no <format> is specified, 'dot' is used. When no <format> and <viewer> is\n");
-		log("specified, 'xdot' is used to display the schematic.\n");
+		log("specified, 'xdot' is used to display the schematic (POSIX systems only).\n");
 		log("\n");
 		log("The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',\n");
 		log("unless another prefix is specified using -prefix <prefix>.\n");
@@ -817,14 +818,30 @@ struct ShowPass : public Pass {
 			log_cmd_error("Nothing there to show.\n");
 
 		if (format != "dot" && !format.empty()) {
-			std::string cmd = stringf("dot -T%s '%s' > '%s.new' && mv '%s.new' '%s'", format.c_str(), dot_file.c_str(), out_file.c_str(), out_file.c_str(), out_file.c_str());
+			#ifdef _WIN32
+				// system()/cmd.exe does not understand single quotes on Windows.
+				#define DOT_CMD "dot -T%s \"%s\" > \"%s.new\" && move \"%s.new\" \"%s\""
+			#else
+				#define DOT_CMD "dot -T%s '%s' > '%s.new' && mv '%s.new' '%s'"
+			#endif
+			std::string cmd = stringf(DOT_CMD, format.c_str(), dot_file.c_str(), out_file.c_str(), out_file.c_str(), out_file.c_str());
+			#undef DOT_CMD
 			log("Exec: %s\n", cmd.c_str());
 			if (run_command(cmd) != 0)
 				log_cmd_error("Shell command failed!\n");
 		}
 
 		if (!viewer_exe.empty()) {
-			std::string cmd = stringf("%s '%s' &", viewer_exe.c_str(), out_file.c_str());
+			#ifdef _WIN32
+				// system()/cmd.exe does not understand single quotes nor
+				// background tasks on Windows. So we have to pause yosys
+				// until the viewer exits.
+				#define VIEW_CMD "%s \"%s\""
+			#else
+				#define VIEW_CMD "%s '%s' &"
+			#endif
+			std::string cmd = stringf(VIEW_CMD, viewer_exe.c_str(), out_file.c_str());
+			#undef VIEW_CMD
 			log("Exec: %s\n", cmd.c_str());
 			if (run_command(cmd) != 0)
 				log_cmd_error("Shell command failed!\n");
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index fadffcdbc..53e248adf 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -778,7 +778,7 @@ struct SimPass : public Pass {
 		log("        number of cycles to simulate (default: 20)\n");
 		log("\n");
 		log("    -a\n");
-		log("        include all nets in VCD output, nut just those with public names\n");
+		log("        include all nets in VCD output, not just those with public names\n");
 		log("\n");
 		log("    -w\n");
 		log("        writeback mode: use final simulation state as new init state\n");
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index 9f73aeb07..e0a07af32 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -920,19 +920,40 @@ parameter A_SIGNED = 1'b0;
 parameter B_SIGNED = 1'b0;
 endmodule
 
-(* blackbox *)
-module SB_SPRAM256KA(
+module SB_SPRAM256KA (
 	input [13:0] ADDRESS,
 	input [15:0] DATAIN,
 	input [3:0] MASKWREN,
-	input WREN,
-	input CHIPSELECT,
-	input CLOCK,
-	input STANDBY,
-	input SLEEP,
-	input POWEROFF,
-	output [15:0] DATAOUT
+	input WREN, CHIPSELECT, CLOCK, STANDBY, SLEEP, POWEROFF,
+	output reg [15:0] DATAOUT
 );
+`ifndef BLACKBOX
+	reg [15:0] mem [0:16383];
+	wire off = SLEEP || !POWEROFF;
+	integer i;
+
+	always @(negedge POWEROFF) begin
+		for (i = 0; i <= 16383; i = i+1)
+			mem[i] = 'bx;
+	end
+
+	always @(posedge CLOCK, posedge off) begin
+		if (off) begin
+			DATAOUT <= 0;
+		end else
+		if (CHIPSELECT && !STANDBY && !WREN) begin
+			DATAOUT <= mem[ADDRESS];
+		end else begin
+			if (CHIPSELECT && !STANDBY && WREN) begin
+				if (MASKWREN[0]) mem[ADDRESS][ 3: 0] = DATAIN[ 3: 0];
+				if (MASKWREN[1]) mem[ADDRESS][ 7: 4] = DATAIN[ 7: 4];
+				if (MASKWREN[2]) mem[ADDRESS][11: 8] = DATAIN[11: 8];
+				if (MASKWREN[3]) mem[ADDRESS][15:12] = DATAIN[15:12];
+			end
+			DATAOUT <= 'bx;
+		end
+	end
+`endif
 endmodule
 
 (* blackbox *)