Merge tag 'upstream/0.7'

69 files changed, 2188 insertions, 307 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 31cd94a5..bfea999a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -3,6 +3,105 @@ List of major changes and improvements between releases
 =======================================================
 
 
+Yosys 0.6 .. Yosys 0.7
+----------------------
+
+ * Various
+    - Added "yosys -D" feature
+    - Added support for installed plugins in $(DATDIR)/plugins/
+    - Renamed opt_const to opt_expr
+    - Renamed opt_share to opt_merge
+    - Added "prep -flatten" and "synth -flatten"
+    - Added "prep -auto-top" and "synth -auto-top"
+    - Using "mfs" and "lutpack" in ABC lut mapping
+    - Support for abstract modules in chparam
+    - Cleanup abstract modules at end of "hierarchy -top"
+    - Added tristate buffer support to iopadmap
+    - Added opt_expr support for div/mod by power-of-two
+    - Added "select -assert-min <N> -assert-max <N>"
+    - Added "attrmvcp" pass
+    - Added "attrmap" command
+    - Added "tee +INT -INT"
+    - Added "zinit" pass
+    - Added "setparam -type"
+    - Added "shregmap" pass
+    - Added "setundef -init"
+    - Added "nlutmap -assert"
+    - Added $sop cell type and "abc -sop -I <num> -P <num>"
+    - Added "dc2" to default ABC scripts
+    - Added "deminout"
+    - Added "insbuf" command
+    - Added "prep -nomem"
+    - Added "opt_rmdff -keepdc"
+    - Added "prep -nokeepdc"
+    - Added initial version of "synth_gowin"
+    - Added "fsm_expand -full"
+    - Added support for fsm_encoding="user"
+    - Many improvements in GreenPAK4 support
+    - Added black box modules for all Xilinx 7-series lib cells
+    - Added synth_ice40 support for latches via logic loops
+    - Fixed ice40_opt lut unmapping, added "ice40_opt -unlut"
+
+ * Build System
+    - Added ABCEXTERNAL and ABCURL make variables
+    - Added BINDIR, LIBDIR, and DATDIR make variables
+    - Added PKG_CONFIG make variable
+    - Added SEED make variable (for "make test")
+    - Added YOSYS_VER_STR make variable
+    - Updated min GCC requirement to GCC 4.8
+    - Updated required Bison version to Bison 3.x
+
+ * Internal APIs
+    - Added ast.h to exported headers
+    - Added ScriptPass helper class for script-like passes
+    - Added CellEdgesDatabase API
+
+ * Front-ends and Back-ends
+    - Added filename glob support to all front-ends
+    - Added avail (black-box) module params to ilang format
+    - Added $display %m support
+    - Added support for $stop Verilog system task
+    - Added support for SystemVerilog packages
+    - Fixed procedural assignments to non-unique lvalues, e.g. {y,y} = {a,b}
+    - Added support for "active high" and "active low" latches in read_blif and write_blif
+    - Use init value "2" for all uninitialized FFs in BLIF back-end
+    - Added "read_blif -sop"
+    - Added "write_blif -noalias"
+    - Added various write_blif options for VTR support
+    - write_json: also write module attributes.
+    - Added "write_verilog -nodec -nostr -defparam"
+    - Added "read_verilog -norestrict -assume-asserts"
+    - Added support for bus interfaces to "read_liberty -lib"
+    - Added liberty parser support for types within cell decls
+    - Added "write_verilog -renameprefix -v"
+    - Added "write_edif -nogndvcc"
+
+ * Formal Verification
+    - Support for hierarchical designs in smt2 back-end
+    - Yosys-smtbmc: Support for hierarchical VCD dumping
+    - Added $initstate cell type and vlog function
+    - Added $anyconst and $anyseq cell types and vlog functions
+    - Added printing of code loc of failed asserts to yosys-smtbmc
+    - Added memory_memx pass, "memory -memx", and "prep -memx"
+    - Added "proc_mux -ifx"
+    - Added "yosys-smtbmc -g"
+    - Deprecated "write_smt2 -regs" (by default on now)
+    - Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
+    - Added support for memories to smtio.py
+    - Added "yosys-smtbmc --dump-vlogtb"
+    - Added "yosys-smtbmc --smtc --dump-smtc"
+    - Added "yosys-smtbmc --dump-all"
+    - Added assertpmux command
+    - Added "yosys-smtbmc --unroll"
+    - Added $past, $stable, $rose, $fell SVA functions
+    - Added "yosys-smtbmc --noinfo and --dummy"
+    - Added "yosys-smtbmc --noincr"
+    - Added "yosys-smtbmc --cex <filename>"
+    - Added $ff and $_FF_ cell types
+    - Added $global_clock verilog syntax support for creating $ff cells
+    - Added clk2fflogic
+
+
 Yosys 0.5 .. Yosys 0.6
 ----------------------
 
diff --git a/Makefile b/Makefile
index fd31776a..0a61fe65 100644
--- a/Makefile
+++ b/Makefile
@@ -72,7 +72,7 @@ else
 	LDLIBS += -lrt
 endif
 
-YOSYS_VER := 0.6+$(shell test -e .git && { git log --author=clifford@clifford.at --oneline 5869d26da021.. | wc -l; })
+YOSYS_VER := 0.7
 GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
 OBJS = kernel/version_$(GIT_REV).o
 
@@ -82,14 +82,14 @@ 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 = 8e08604f8ad3
+ABCREV = eb6eca6807cc
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"
 
 # set ABCEXTERNAL = <abc-command> to use an external ABC instance
 # Note: The in-tree ABC (yosys-abc) will not be installed when ABCEXTERNAL is set.
-ABCEXTERNAL =
+ABCEXTERNAL ?=
 
 define newline
 
@@ -370,10 +370,12 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS))
 	$(Q) mkdir -p $(dir $@)
 	$(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $<
 
+YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) $(shell \
+		$(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))
+
 kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile
 	$(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc
-	$(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) ` \
-			$(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1` $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))\"; }" > kernel/version_$(GIT_REV).cc
+	$(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"$(YOSYS_VER_STR)\"; }" > kernel/version_$(GIT_REV).cc
 
 yosys-config: misc/yosys-config.in
 	$(P) $(SED) -e 's#@CXXFLAGS@#$(subst -I. -I"$(YOSYS_SRC)",-I"$(DATDIR)/include",$(CXXFLAGS))#;' \
@@ -404,16 +406,22 @@ endif
 yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE)
 	$(P) cp abc/abc-$(ABCREV)$(EXE) yosys-abc$(EXE)
 
+ifneq ($(SEED),)
+SEEDOPT="-S $(SEED)"
+else
+SEEDOPT=""
+endif
+
 test: $(TARGETS) $(EXTRA_TARGETS)
-	+cd tests/simple && bash run-test.sh
-	+cd tests/hana && bash run-test.sh
-	+cd tests/asicworld && bash run-test.sh
-	+cd tests/realmath && bash run-test.sh
-	+cd tests/share && bash run-test.sh
-	+cd tests/fsm && bash run-test.sh
+	+cd tests/simple && bash run-test.sh $(SEEDOPT)
+	+cd tests/hana && bash run-test.sh $(SEEDOPT)
+	+cd tests/asicworld && bash run-test.sh $(SEEDOPT)
+	+cd tests/realmath && bash run-test.sh $(SEEDOPT)
+	+cd tests/share && bash run-test.sh $(SEEDOPT)
+	+cd tests/fsm && bash run-test.sh $(SEEDOPT)
 	+cd tests/techmap && bash run-test.sh
-	+cd tests/memories && bash run-test.sh
-	+cd tests/bram && bash run-test.sh
+	+cd tests/memories && bash run-test.sh $(SEEDOPT)
+	+cd tests/bram && bash run-test.sh $(SEEDOPT)
 	+cd tests/various && bash run-test.sh
 	+cd tests/sat && bash run-test.sh
 	@echo ""
diff --git a/README b/README
index 32e9ba24..8e43d444 100644
--- a/README
+++ b/README
@@ -374,6 +374,27 @@ Verilog Attributes and non-standard features
   and constant values). The intended use for this is synthesis-time DRC.
 
 
+Non-standard or SystemVerilog features for formal verification
+==============================================================
+
+- 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
+  to 0 otherwise.
+
+- The system task $anyconst evaluates to any constant value.
+
+- 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 syntax @($global_clock) can be used to create FFs that have no
+  explicit clock input ($ff cells).
+
+
 Supported features from SystemVerilog
 =====================================
 
@@ -384,8 +405,8 @@ from SystemVerilog:
   form. In module context: "assert property (<expression>);" and within an
   always block: "assert(<expression>);". It is transformed to a $assert cell.
 
-- The "assume" 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.
diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc
index 6a379e67..d9d0cc17 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -77,9 +77,6 @@ struct BlifDumper
 						case State::S1:
 							init_bits[initsig[i]] = 1;
 							break;
-						case State::Sx:
-							init_bits[initsig[i]] = 2;
-							break;
 						default:
 							break;
 					}
@@ -126,7 +123,7 @@ struct BlifDumper
 		sigmap.apply(sig);
 
 		if (init_bits.count(sig) == 0)
-			return "";
+			return " 2";
 
 		string str = stringf(" %d", init_bits.at(sig));
 
@@ -315,6 +312,12 @@ struct BlifDumper
 				continue;
 			}
 
+			if (!config->icells_mode && cell->type == "$_FF_") {
+				f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
+						cstr_init(cell->getPort("\\Q")));
+				continue;
+			}
+
 			if (!config->icells_mode && cell->type == "$_DFF_N_") {
 				f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
 						cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 03e29c52..16d1a97f 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -228,6 +228,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
 		f << stringf("\n");
 		break;
 	case RTLIL::STa: f << stringf("always\n"); break;
+	case RTLIL::STg: f << stringf("global\n"); break;
 	case RTLIL::STi: f << stringf("init\n"); break;
 	}
 
@@ -277,6 +278,13 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu
 		}
 
 		f << stringf("%s" "module %s\n", indent.c_str(), module->name.c_str());
+
+		if (!module->avail_parameters.empty()) {
+			if (only_selected)
+				f << stringf("\n");
+			for (auto &p : module->avail_parameters)
+				f << stringf("%s" "  parameter %s\n", indent.c_str(), p.c_str());
+		}
 	}
 
 	if (print_body)
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9a25f3a2..ddac6900 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -379,7 +379,7 @@ struct Smt2Worker
 			return;
 		}
 
-		if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+		if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
 		{
 			registers.insert(cell);
 			decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
@@ -407,7 +407,7 @@ struct Smt2Worker
 
 		if (bvmode)
 		{
-			if (cell->type == "$dff")
+			if (cell->type.in("$ff", "$dff"))
 			{
 				registers.insert(cell);
 				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
@@ -417,7 +417,7 @@ struct Smt2Worker
 				return;
 			}
 
-			if (cell->type == "$anyconst")
+			if (cell->type.in("$anyconst", "$anyseq"))
 			{
 				registers.insert(cell);
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
@@ -586,7 +586,7 @@ struct Smt2Worker
 			return;
 		}
 
-		log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
+		log_error("Unsupported cell type %s for cell %s.%s.\n",
 				log_id(cell->type), log_id(module), log_id(cell));
 	}
 
@@ -596,7 +596,7 @@ struct Smt2Worker
 
 		pool<SigBit> reg_bits;
 		for (auto cell : module->cells())
-			if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) {
+			if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
 				// not using sigmap -- we want the net directly at the dff output
 				for (auto bit : cell->getPort("\\Q"))
 					reg_bits.insert(bit);
@@ -674,14 +674,14 @@ struct Smt2Worker
 
 			for (auto cell : this_regs)
 			{
-				if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+				if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
 				{
 					std::string expr_d = get_bool(cell->getPort("\\D"));
 					std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
 				}
 
-				if (cell->type == "$dff")
+				if (cell->type.in("$ff", "$dff"))
 				{
 					std::string expr_d = get_bv(cell->getPort("\\D"));
 					std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index bb763647..04c25f91 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -26,6 +26,7 @@ skip_steps = 0
 step_size = 1
 num_steps = 20
 vcdfile = None
+cexfile = None
 vlogtbfile = None
 inconstr = list()
 outconstr = None
@@ -61,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --smtc <constr_filename>
         read constraints file
 
+    --cex <cex_filename>
+        read cex file as written by ABC's "write_cex -n"
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -94,7 +98,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"])
 except:
     usage()
 
@@ -118,6 +122,8 @@ for o, a in opts:
         final_only = True
     elif o == "--smtc":
         inconstr.append(a)
+    elif o == "--cex":
+        cexfile = a
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -146,6 +152,7 @@ if len(args) != 1:
 constr_final_start = None
 constr_asserts = defaultdict(list)
 constr_assumes = defaultdict(list)
+constr_write = list()
 
 for fn in inconstr:
     current_states = None
@@ -229,6 +236,14 @@ for fn in inconstr:
 
                 continue
 
+            if tokens[0] == "write":
+                constr_write.append(" ".join(tokens[1:]))
+                continue
+
+            if tokens[0] == "logic":
+                so.logic = " ".join(tokens[1:])
+                continue
+
             assert 0
 
 
@@ -240,7 +255,7 @@ def get_constr_expr(db, state, final=False, getvalues=False):
         if state not in db:
             return ([], [], []) if getvalues else "true"
 
-    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
+    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*)\](?=[ )]|$)')
 
     def replace_netref(match):
         state_sel = match.group(2)
@@ -280,6 +295,9 @@ def get_constr_expr(db, state, final=False, getvalues=False):
 
 smt = SmtIo(opts=so)
 
+if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None:
+    smt.produce_models = False
+
 def print_msg(msg):
     print("%s %s" % (smt.timestamp(), msg))
     sys.stdout.flush()
@@ -290,12 +308,46 @@ with open(args[0], "r") as f:
     for line in f:
         smt.write(line)
 
+for line in constr_write:
+    smt.write(line)
+
 if topmod is None:
     topmod = smt.topmod
 
 assert topmod is not None
 assert topmod in smt.modinfo
 
+if cexfile is not None:
+    with open(cexfile, "r") as f:
+        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
+        for entry in f.read().split():
+            match = cex_regex.match(entry)
+            assert match
+
+            name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
+
+            if extra_name != "":
+                continue
+
+            if name not in smt.modinfo[topmod].inputs:
+                continue
+
+            if bit is None:
+                bit = 0
+            else:
+                bit = int(bit[1:-1])
+
+            step = int(step[1:])
+            val = int(val)
+
+            if smt.modinfo[topmod].wsize[name] == 1:
+                assert bit == 0
+                smtexpr = "(= [%s] %s)" % (name, "true" if val else "false")
+            else:
+                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val)
+
+            # print("cex@%d: %s" % (step, smtexpr))
+            constr_assumes[step].append((cexfile, smtexpr))
 
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
@@ -625,9 +677,10 @@ else:  # not tempind
 
                 smt.write("(pop 1)")
 
-            for i in range(step, last_check_step+1):
-                smt.write("(assert (|%s_a| s%d))" % (topmod, i))
-                smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
+            if (constr_final_start is not None) or (last_check_step+1 != num_steps):
+                for i in range(step, last_check_step+1):
+                    smt.write("(assert (|%s_a| s%d))" % (topmod, i))
+                    smt.write("(assert %s)" % get_constr_expr(constr_asserts, i))
 
             if constr_final_start is not None:
                 for i in range(step, last_check_step+1):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 58554572..865eed1f 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -53,6 +53,9 @@ class SmtIo:
         self.logic_ax = True
         self.logic_uf = True
         self.logic_bv = True
+        self.produce_models = True
+        self.smt2cache = [list()]
+        self.p = None
 
         if opts is not None:
             self.logic = opts.logic
@@ -62,6 +65,9 @@ class SmtIo:
             self.dummy_file = opts.dummy_file
             self.timeinfo = opts.timeinfo
             self.unroll = opts.unroll
+            self.noincr = opts.noincr
+            self.info_stmts = opts.info_stmts
+            self.nocomments = opts.nocomments
 
         else:
             self.solver = "z3"
@@ -70,30 +76,40 @@ class SmtIo:
             self.dummy_file = None
             self.timeinfo = True
             self.unroll = False
+            self.noincr = False
+            self.info_stmts = list()
+            self.nocomments = False
 
         if self.solver == "yices":
-            popen_vargs = ['yices-smt2', '--incremental']
+            self.popen_vargs = ['yices-smt2', '--incremental']
 
         if self.solver == "z3":
-            popen_vargs = ['z3', '-smt2', '-in']
+            self.popen_vargs = ['z3', '-smt2', '-in']
 
         if self.solver == "cvc4":
-            popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
+            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
 
         if self.solver == "mathsat":
-            popen_vargs = ['mathsat']
+            self.popen_vargs = ['mathsat']
 
         if self.solver == "boolector":
-            popen_vargs = ['boolector', '--smt2', '-i']
+            self.popen_vargs = ['boolector', '--smt2', '-i']
             self.unroll = True
 
+        if self.solver == "abc":
+            self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
+            self.logic_ax = False
+            self.unroll = True
+            self.noincr = True
+
         if self.solver == "dummy":
             assert self.dummy_file is not None
             self.dummy_fd = open(self.dummy_file, "r")
         else:
             if self.dummy_file is not None:
                 self.dummy_fd = open(self.dummy_file, "w")
-            self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+            if not self.noincr:
+                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 
         if self.unroll:
             self.logic_uf = False
@@ -123,9 +139,15 @@ class SmtIo:
             if self.logic_bv: self.logic += "BV"
 
         self.setup_done = True
-        self.write("(set-option :produce-models true)")
+
+        if self.produce_models:
+            self.write("(set-option :produce-models true)")
+
         self.write("(set-logic %s)" % self.logic)
 
+        for stmt in self.info_stmts:
+            self.write(stmt)
+
     def timestamp(self):
         secs = int(time() - self.start_time)
         return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
@@ -187,11 +209,12 @@ class SmtIo:
 
         stmt = stmt.strip()
 
-        if unroll and self.unroll:
+        if self.nocomments or self.unroll:
             if stmt.startswith(";"):
                 return
-
             stmt = re.sub(r" ;.*", "", stmt)
+
+        if unroll and self.unroll:
             stmt = self.unroll_buffer + stmt
             self.unroll_buffer = ""
 
@@ -246,8 +269,22 @@ class SmtIo:
             self.debug_file.flush()
 
         if self.solver != "dummy":
-            self.p.stdin.write(bytes(stmt + "\n", "ascii"))
-            self.p.stdin.flush()
+            if self.noincr:
+                if self.p is not None and not stmt.startswith("(get-"):
+                    self.p.stdin.close()
+                    self.p = None
+                if stmt == "(push 1)":
+                    self.smt2cache.append(list())
+                elif stmt == "(pop 1)":
+                    self.smt2cache.pop()
+                else:
+                    if self.p is not None:
+                        self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+                        self.p.stdin.flush()
+                    self.smt2cache[-1].append(stmt)
+            else:
+                self.p.stdin.write(bytes(stmt + "\n", "ascii"))
+                self.p.stdin.flush()
 
     def info(self, stmt):
         if not stmt.startswith("; yosys-smt2-"):
@@ -355,11 +392,20 @@ class SmtIo:
     def check_sat(self):
         if self.debug_print:
             print("> (check-sat)")
-        if self.debug_file:
+        if self.debug_file and not self.nocomments:
             print("; running check-sat..", file=self.debug_file)
             self.debug_file.flush()
 
         if self.solver != "dummy":
+            if self.noincr:
+                if self.p is not None:
+                    self.p.stdin.close()
+                    self.p = None
+                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+                for cache_ctx in self.smt2cache:
+                    for cache_stmt in cache_ctx:
+                        self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))
+
             self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
             self.p.stdin.flush()
 
@@ -495,6 +541,10 @@ class SmtIo:
     def net_expr(self, mod, base, path):
         if len(path) == 1:
             assert mod in self.modinfo
+            if path[0] == "":
+                return base
+            if path[0] in self.modinfo[mod].cells:
+                return "(|%s_h %s| %s)" % (mod, path[0], base)
             if path[0] in self.modinfo[mod].wsize:
                 return "(|%s_n %s| %s)" % (mod, path[0], base)
             if path[0] in self.modinfo[mod].memories:
@@ -555,21 +605,24 @@ class SmtIo:
         return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
 
     def wait(self):
-        if self.solver != "dummy":
+        if self.p is not None:
             self.p.wait()
 
 
 class SmtOpts:
     def __init__(self):
         self.shortopts = "s:v"
-        self.longopts = ["unroll", "no-progress", "dump-smt2=", "logic=", "dummy="]
+        self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
         self.solver = "z3"
         self.debug_print = False
         self.debug_file = None
         self.dummy_file = None
         self.unroll = False
+        self.noincr = False
         self.timeinfo = True
         self.logic = None
+        self.info_stmts = list()
+        self.nocomments = False
 
     def handle(self, o, a):
         if o == "-s":
@@ -578,7 +631,9 @@ class SmtOpts:
             self.debug_print = True
         elif o == "--unroll":
             self.unroll = True
-        elif o == "--no-progress":
+        elif o == "--noincr":
+            self.noincr = True
+        elif o == "--noprogress":
             self.timeinfo = True
         elif o == "--dump-smt2":
             self.debug_file = open(a, "w")
@@ -586,6 +641,10 @@ class SmtOpts:
             self.logic = a
         elif o == "--dummy":
             self.dummy_file = a
+        elif o == "--info":
+            self.info_stmts.append(a)
+        elif o == "--nocomments":
+            self.nocomments = True
         else:
             return False
         return True
@@ -609,11 +668,21 @@ class SmtOpts:
     --unroll
         unroll uninterpreted functions
 
-    --no-progress
+    --noincr
+        don't use incremental solving, instead restart solver for
+        each (check-sat). This also avoids (push) and (pop).
+
+    --noprogress
         disable timer display during solving
 
     --dump-smt2 <filename>
         write smt2 statements to file
+
+    --info <smt2-info-stmt>
+        include the specified smt2 info statement in the smt2 output
+
+    --nocomments
+        strip all comments from the generated smt2 code
 """
 
 
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 52cf861d..a617215f 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -33,10 +33,11 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool norename, noattr, attr2comment, noexpr, nodec, nostr, defparam;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, 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;
 
@@ -85,13 +86,14 @@ void reset_auto_counter(RTLIL::Module *module)
 	for (size_t i = 10; i < auto_name_offset + auto_name_map.size(); i = i*10)
 		auto_name_digits++;
 
-	for (auto it = auto_name_map.begin(); it != auto_name_map.end(); ++it)
-		log("  renaming `%s' to `_%0*d_'.\n", it->first.c_str(), auto_name_digits, auto_name_offset + it->second);
+	if (verbose)
+		for (auto it = auto_name_map.begin(); it != auto_name_map.end(); ++it)
+			log("  renaming `%s' to `%s_%0*d_'.\n", it->first.c_str(), auto_prefix.c_str(), auto_name_digits, auto_name_offset + it->second);
 }
 
 std::string next_auto_id()
 {
-	return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_counter++);
+	return stringf("%s_%0*d_", auto_prefix.c_str(), auto_name_digits, auto_name_offset + auto_name_counter++);
 }
 
 std::string id(RTLIL::IdString internal_id, bool may_rename = true)
@@ -100,7 +102,7 @@ std::string id(RTLIL::IdString internal_id, bool may_rename = true)
 	bool do_escape = false;
 
 	if (may_rename && auto_name_map.count(internal_id) != 0)
-		return stringf("_%0*d_", auto_name_digits, auto_name_offset + auto_name_map[internal_id]);
+		return stringf("%s_%0*d_", auto_prefix.c_str(), auto_name_digits, auto_name_offset + auto_name_map[internal_id]);
 
 	if (*str == '\\')
 		str++;
@@ -1342,6 +1344,9 @@ struct VerilogBackend : public Backend {
 		log("        instead of a backslash prefix) are changed to short names in the\n");
 		log("        format '_<number>_'.\n");
 		log("\n");
+		log("    -renameprefix <prefix>\n");
+		log("        insert this prefix in front of auto-generated instance names\n");
+		log("\n");
 		log("    -noattr\n");
 		log("        with this option no attributes are included in the output\n");
 		log("\n");
@@ -1376,6 +1381,9 @@ struct VerilogBackend : public Backend {
 		log("        only write selected modules. modules must be selected entirely or\n");
 		log("        not at all.\n");
 		log("\n");
+		log("    -v\n");
+		log("        verbose output (print new names of all renamed wires and cells)\n");
+		log("\n");
 		log("Note that RTLIL processes can't always be mapped directly to Verilog\n");
 		log("always blocks. This frontend should only be used to export an RTLIL\n");
 		log("netlist, i.e. after the \"proc\" pass has been used to convert all\n");
@@ -1387,6 +1395,7 @@ struct VerilogBackend : public Backend {
 	{
 		log_header(design, "Executing Verilog backend.\n");
 
+		verbose = false;
 		norename = false;
 		noattr = false;
 		attr2comment = false;
@@ -1394,6 +1403,7 @@ struct VerilogBackend : public Backend {
 		nodec = false;
 		nostr = false;
 		defparam = false;
+		auto_prefix = "";
 
 		bool blackboxes = false;
 		bool selected = false;
@@ -1431,6 +1441,10 @@ struct VerilogBackend : public Backend {
 				norename = true;
 				continue;
 			}
+			if (arg == "-renameprefix" && argidx+1 < args.size()) {
+				auto_prefix = args[++argidx];
+				continue;
+			}
 			if (arg == "-noattr") {
 				noattr = true;
 				continue;
@@ -1463,6 +1477,10 @@ struct VerilogBackend : public Backend {
 				selected = true;
 				continue;
 			}
+			if (arg == "-v") {
+				verbose = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
diff --git a/examples/smtbmc/demo7.v b/examples/smtbmc/demo7.v
index 75b3865c..63f6272f 100644
--- a/examples/smtbmc/demo7.v
+++ b/examples/smtbmc/demo7.v
@@ -1,6 +1,7 @@
 // Demo for memory initialization
 
-module demo7 (input [2:0] addr);
+module demo7;
+	wire [2:0] addr = $anyseq;
 	reg [15:0] memory [0:7];
 
 	initial begin
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index fd272400..92513a24 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -934,10 +934,15 @@ static AstModule* process_module(AstNode *ast, bool defer)
 		if (flag_lib) {
 			std::vector<AstNode*> new_children;
 			for (auto child : ast->children) {
-				if (child->type == AST_WIRE && (child->is_input || child->is_output))
+				if (child->type == AST_WIRE && (child->is_input || child->is_output)) {
 					new_children.push_back(child);
-				else
+				} else if (child->type == AST_PARAMETER) {
+					child->delete_children();
+					child->children.push_back(AstNode::mkconst_int(0, false, 0));
+					new_children.push_back(child);
+				} else {
 					delete child;
+				}
 			}
 			ast->children.swap(new_children);
 			ast->attributes["\\blackbox"] = AstNode::mkconst_int(1, false);
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 3c57162a..db8d7409 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -220,12 +220,19 @@ struct AST_INTERNAL::ProcessGenerator
 		subst_lvalue_to = new_temp_signal(subst_lvalue_from);
 		subst_lvalue_map = subst_lvalue_from.to_sigbit_map(subst_lvalue_to);
 
+		bool found_global_syncs = false;
 		bool found_anyedge_syncs = false;
 		for (auto child : always->children)
-			if (child->type == AST_EDGE)
-				found_anyedge_syncs = true;
+			if (child->type == AST_EDGE) {
+				if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->str == "\\$global_clock")
+					found_global_syncs = true;
+				else
+					found_anyedge_syncs = true;
+			}
 
 		if (found_anyedge_syncs) {
+			if (found_global_syncs)
+				log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
 			log("Note: Assuming pure combinatorial block at %s:%d in\n", always->filename.c_str(), always->linenum);
 			log("compliance with IEC 62142(E):2005 / IEEE Std. 1364.1(E):2002. Recommending\n");
 			log("use of @* instead of @(...) for better match of synthesis and simulation.\n");
@@ -236,7 +243,7 @@ struct AST_INTERNAL::ProcessGenerator
 		for (auto child : always->children)
 			if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) {
 				found_clocked_sync = true;
-				if (found_anyedge_syncs)
+				if (found_global_syncs || found_anyedge_syncs)
 					log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
 				RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
 				syncrule->type = child->type == AST_POSEDGE ? RTLIL::STp : RTLIL::STn;
@@ -248,7 +255,7 @@ struct AST_INTERNAL::ProcessGenerator
 			}
 		if (proc->syncs.empty()) {
 			RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
-			syncrule->type = RTLIL::STa;
+			syncrule->type = found_global_syncs ? RTLIL::STg : RTLIL::STa;
 			syncrule->signal = RTLIL::SigSpec();
 			addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true);
 			proc->syncs.push_back(syncrule);
@@ -755,7 +762,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
 		break;
 
 	case AST_FCALL:
-		if (str == "\\$anyconst") {
+		if (str == "\\$anyconst" || str == "\\$anyseq") {
 			if (GetSize(children) == 1) {
 				while (children[0]->simplify(true, false, false, 1, -1, false, true) == true) { }
 				if (children[0]->type != AST_CONSTANT)
@@ -1264,6 +1271,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 			wire->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
 
 			int mem_width, mem_size, addr_bits;
+			is_signed = id2ast->is_signed;
 			id2ast->meminfo(mem_width, mem_size, addr_bits);
 
 			RTLIL::SigSpec addr_sig = children[0]->genRTLIL();
@@ -1458,7 +1466,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 		} break;
 
 	case AST_FCALL: {
-			if (str == "\\$anyconst")
+			if (str == "\\$anyconst" || str == "\\$anyseq")
 			{
 				string myid = stringf("%s$%d", str.c_str() + 1, autoidx++);
 				int width = width_hint;
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 57aa648c..9d5c75fe 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1510,6 +1510,7 @@ skip_dynamic_range_lvalue_expansion:;
 		}
 
 		int mem_width, mem_size, addr_bits;
+		bool mem_signed = children[0]->id2ast->is_signed;
 		children[0]->id2ast->meminfo(mem_width, mem_size, addr_bits);
 
 		int data_range_left = children[0]->id2ast->children[0]->range_left;
@@ -1529,6 +1530,7 @@ skip_dynamic_range_lvalue_expansion:;
 
 		AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true)));
 		wire_data->str = id_data;
+		wire_data->is_signed = mem_signed;
 		current_ast_mod->children.push_back(wire_data);
 		current_scope[wire_data->str] = wire_data;
 		while (wire_data->simplify(true, false, false, 1, -1, false, false)) { }
@@ -1807,8 +1809,8 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
-			// $anyconst is mapped in AstNode::genRTLIL()
-			if (str == "\\$anyconst") {
+			// $anyconst and $anyseq are mapped in AstNode::genRTLIL()
+			if (str == "\\$anyconst" || str == "\\$anyseq") {
 				recursion_counter--;
 				return false;
 			}
@@ -2894,6 +2896,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 		std::string id_addr = sstr.str() + "_ADDR", id_data = sstr.str() + "_DATA";
 
 		int mem_width, mem_size, addr_bits;
+		bool mem_signed = children[0]->id2ast->is_signed;
 		children[0]->id2ast->meminfo(mem_width, mem_size, addr_bits);
 
 		AstNode *wire_addr = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(addr_bits-1, true), mkconst_int(0, true)));
@@ -2906,6 +2909,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 		AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true)));
 		wire_data->str = id_data;
 		wire_data->is_reg = true;
+		wire_data->is_signed = mem_signed;
 		wire_data->attributes["\\nosync"] = AstNode::mkconst_int(1, false);
 		mod->children.push_back(wire_data);
 		while (wire_data->simplify(true, false, false, 1, -1, false, false)) { }
@@ -2967,6 +2971,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 			std::string id_addr = sstr.str() + "_ADDR", id_data = sstr.str() + "_DATA";
 
 			int mem_width, mem_size, addr_bits;
+			bool mem_signed = id2ast->is_signed;
 			id2ast->meminfo(mem_width, mem_size, addr_bits);
 
 			AstNode *wire_addr = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(addr_bits-1, true), mkconst_int(0, true)));
@@ -2980,6 +2985,7 @@ bool AstNode::mem2reg_as_needed_pass2(pool<AstNode*> &mem2reg_set, AstNode *mod,
 			AstNode *wire_data = new AstNode(AST_WIRE, new AstNode(AST_RANGE, mkconst_int(mem_width-1, true), mkconst_int(0, true)));
 			wire_data->str = id_data;
 			wire_data->is_reg = true;
+			wire_data->is_signed = mem_signed;
 			if (block)
 				wire_data->attributes["\\nosync"] = AstNode::mkconst_int(1, false);
 			mod->children.push_back(wire_data);
diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 3717a1e5..6d4d6087 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -23,6 +23,7 @@ YOSYS_NAMESPACE_BEGIN
 
 static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, std::istream &f)
 {
+	string strbuf;
 	int buffer_len = 0;
 	buffer[0] = 0;
 
@@ -42,8 +43,13 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count,
 			if (buffer_len > 0 && buffer[buffer_len-1] == '\\')
 				buffer[--buffer_len] = 0;
 			line_count++;
-			if (!f.getline(buffer+buffer_len, buffer_size-buffer_len))
+			if (!std::getline(f, strbuf))
 				return false;
+			while (buffer_size-buffer_len < strbuf.size()+1) {
+				buffer_size *= 2;
+				buffer = (char*)realloc(buffer, buffer_size);
+			}
+			strcpy(buffer+buffer_len, strbuf.c_str());
 		} else
 			return true;
 	}
@@ -256,9 +262,13 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 					cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false);
 				else {
 			no_latch_clock:
-					cell = module->addCell(NEW_ID, dff_name);
-					cell->setPort("\\D", blif_wire(d));
-					cell->setPort("\\Q", blif_wire(q));
+					if (dff_name.empty()) {
+						cell = module->addFf(NEW_ID, blif_wire(d), blif_wire(q));
+					} else {
+						cell = module->addCell(NEW_ID, dff_name);
+						cell->setPort("\\D", blif_wire(d));
+						cell->setPort("\\Q", blif_wire(q));
+					}
 				}
 
 				obj_attributes = &cell->attributes;
@@ -477,7 +487,7 @@ struct BlifFrontend : public Frontend {
 		}
 		extra_args(f, filename, args, argidx);
 
-		parse_blif(design, *f, "\\DFF", true, sop_mode);
+		parse_blif(design, *f, "", true, sop_mode);
 	}
 } BlifFrontend;
 
diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l
index 415de74e..84238854 100644
--- a/frontends/ilang/ilang_lexer.l
+++ b/frontends/ilang/ilang_lexer.l
@@ -74,6 +74,7 @@ USING_YOSYS_NAMESPACE
 "negedge"	{ return TOK_NEGEDGE; }
 "edge"		{ return TOK_EDGE; }
 "always"	{ return TOK_ALWAYS; }
+"global"	{ return TOK_GLOBAL; }
 "init"		{ return TOK_INIT; }
 "update"	{ return TOK_UPDATE; }
 "process"	{ return TOK_PROCESS; }
diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y
index cc31c864..bfc062fe 100644
--- a/frontends/ilang/ilang_parser.y
+++ b/frontends/ilang/ilang_parser.y
@@ -57,7 +57,7 @@ USING_YOSYS_NAMESPACE
 %token <integer> TOK_INT
 %token TOK_AUTOIDX TOK_MODULE TOK_WIRE TOK_WIDTH TOK_INPUT TOK_OUTPUT TOK_INOUT
 %token TOK_CELL TOK_CONNECT TOK_SWITCH TOK_CASE TOK_ASSIGN TOK_SYNC
-%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_INIT
+%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_GLOBAL TOK_INIT
 %token TOK_UPDATE TOK_PROCESS TOK_END TOK_INVALID TOK_EOL TOK_OFFSET
 %token TOK_PARAMETER TOK_ATTRIBUTE TOK_MEMORY TOK_SIZE TOK_SIGNED TOK_UPTO
 
@@ -112,7 +112,13 @@ module_body:
 	/* empty */;
 
 module_stmt:
-	attr_stmt | wire_stmt | memory_stmt | cell_stmt | proc_stmt | conn_stmt;
+	param_stmt | attr_stmt | wire_stmt | memory_stmt | cell_stmt | proc_stmt | conn_stmt;
+
+param_stmt:
+	TOK_PARAMETER TOK_ID EOL {
+		current_module->avail_parameters.insert($2);
+		free($2);
+	};
 
 attr_stmt:
 	TOK_ATTRIBUTE TOK_ID constant EOL {
@@ -301,6 +307,12 @@ sync_list:
 		rule->signal = RTLIL::SigSpec();
 		current_process->syncs.push_back(rule);
 	} update_list |
+	sync_list TOK_SYNC TOK_GLOBAL EOL {
+		RTLIL::SyncRule *rule = new RTLIL::SyncRule;
+		rule->type = RTLIL::SyncType::STg;
+		rule->signal = RTLIL::SigSpec();
+		current_process->syncs.push_back(rule);
+	} update_list |
 	sync_list TOK_SYNC TOK_INIT EOL {
 		RTLIL::SyncRule *rule = new RTLIL::SyncRule;
 		rule->type = RTLIL::SyncType::STi;
diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc
index 73d927fa..4666c818 100644
--- a/frontends/liberty/liberty.cc
+++ b/frontends/liberty/liberty.cc
@@ -401,6 +401,47 @@ static void create_latch(RTLIL::Module *module, LibertyAst *node)
 	cell->setPort("\\E", enable_sig);
 }
 
+void parse_type_map(std::map<std::string, std::tuple<int, int, bool>> &type_map, LibertyAst *ast)
+{
+	for (auto type_node : ast->children)
+	{
+		if (type_node->id != "type" || type_node->args.size() != 1)
+			continue;
+
+		std::string type_name = type_node->args.at(0);
+		int bit_width = -1, bit_from = -1, bit_to = -1;
+		bool upto = false;
+
+		for (auto child : type_node->children)
+		{
+			if (child->id == "base_type" && child->value != "array")
+				goto next_type;
+
+			if (child->id == "data_type" && child->value != "bit")
+				goto next_type;
+
+			if (child->id == "bit_width")
+				bit_width = atoi(child->value.c_str());
+
+			if (child->id == "bit_from")
+				bit_from = atoi(child->value.c_str());
+
+			if (child->id == "bit_to")
+				bit_to = atoi(child->value.c_str());
+
+			if (child->id == "downto" && (child->value == "0" || child->value == "false" || child->value == "FALSE"))
+				upto = true;
+		}
+
+		if (bit_width != (std::max(bit_from, bit_to) - std::min(bit_from, bit_to) + 1))
+			log_error("Incompatible array type '%s': bit_width=%d, bit_from=%d, bit_to=%d.\n",
+					type_name.c_str(), bit_width, bit_from, bit_to);
+
+		type_map[type_name] = std::tuple<int, int, bool>(bit_width, std::min(bit_from, bit_to), upto);
+	next_type:;
+	}
+}
+
 struct LibertyFrontend : public Frontend {
 	LibertyFrontend() : Frontend("liberty", "read cells from liberty file") { }
 	virtual void help()
@@ -469,45 +510,8 @@ struct LibertyFrontend : public Frontend {
 		LibertyParser parser(*f);
 		int cell_count = 0;
 
-		std::map<std::string, std::tuple<int, int, bool>> type_map;
-
-		for (auto type_node : parser.ast->children)
-		{
-			if (type_node->id != "type" || type_node->args.size() != 1)
-				continue;
-
-			std::string type_name = type_node->args.at(0);
-			int bit_width = -1, bit_from = -1, bit_to = -1;
-			bool upto = false;
-
-			for (auto child : type_node->children)
-			{
-				if (child->id == "base_type" && child->value != "array")
-					goto next_type;
-
-				if (child->id == "data_type" && child->value != "bit")
-					goto next_type;
-
-				if (child->id == "bit_width")
-					bit_width = atoi(child->value.c_str());
-
-				if (child->id == "bit_from")
-					bit_from = atoi(child->value.c_str());
-
-				if (child->id == "bit_to")
-					bit_to = atoi(child->value.c_str());
-
-				if (child->id == "downto" && (child->value == "0" || child->value == "false" || child->value == "FALSE"))
-					upto = true;
-			}
-
-			if (bit_width != (std::max(bit_from, bit_to) - std::min(bit_from, bit_to) + 1))
-				log_error("Incompatible array type '%s': bit_width=%d, bit_from=%d, bit_to=%d.\n",
-						type_name.c_str(), bit_width, bit_from, bit_to);
-
-			type_map[type_name] = std::tuple<int, int, bool>(bit_width, std::min(bit_from, bit_to), upto);
-		next_type:;
-		}
+		std::map<std::string, std::tuple<int, int, bool>> global_type_map;
+		parse_type_map(global_type_map, parser.ast);
 
 		for (auto cell : parser.ast->children)
 		{
@@ -524,6 +528,9 @@ struct LibertyFrontend : public Frontend {
 
 			// log("Processing cell type %s.\n", RTLIL::unescape_id(cell_name).c_str());
 
+			std::map<std::string, std::tuple<int, int, bool>> type_map = global_type_map;
+			parse_type_map(type_map, cell);
+
 			RTLIL::Module *module = new RTLIL::Module;
 			module->name = cell_name;
 
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index c730ce5b..5bbda535 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -1229,7 +1229,7 @@ rvalue:
 		$$ = new AstNode(AST_IDENTIFIER, $2);
 		$$->str = *$1;
 		delete $1;
-		if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst"))
+		if ($2 == nullptr && formal_mode && ($$->str == "\\$initstate" || $$->str == "\\$anyconst" || $$->str == "\\$anyseq"))
 			$$->type = AST_FCALL;
 	} |
 	hierarchical_id non_opt_multirange {
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 900c12d0..f0ead1e8 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -118,6 +118,7 @@ struct CellTypes
 		setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
+		setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$equiv", {A, B}, {Y}, true);
 	}
 
@@ -130,6 +131,7 @@ struct CellTypes
 		IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT";
 
 		setup_type("$sr", {SET, CLR}, {Q});
+		setup_type("$ff", {D}, {Q});
 		setup_type("$dff", {CLK, D}, {Q});
 		setup_type("$dffe", {CLK, EN, D}, {Q});
 		setup_type("$dffsr", {CLK, SET, CLR, D}, {Q});
@@ -184,6 +186,8 @@ struct CellTypes
 		for (auto c2 : list_np)
 			setup_type(stringf("$_SR_%c%c_", c1, c2), {S, R}, {Q});
 
+		setup_type("$_FF_", {D}, {Q});
+
 		for (auto c1 : list_np)
 			setup_type(stringf("$_DFF_%c_", c1), {C, D}, {Q});
 
diff --git a/kernel/driver.cc b/kernel/driver.cc
index 5cfc4171..f8d00c38 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -510,7 +510,9 @@ int main(int argc, char **argv)
 #endif
 
 	log_flush();
-#ifdef _WIN32
+#if defined(_MSC_VER)
+	_exit(0);
+#elif defined(_WIN32)
 	_Exit(0);
 #endif
 
diff --git a/kernel/log.cc b/kernel/log.cc
index 3f1d8881..abc401f5 100644
--- a/kernel/log.cc
+++ b/kernel/log.cc
@@ -207,6 +207,8 @@ void logv_error(const char *format, va_list ap)
 #ifdef EMSCRIPTEN
 	log_files = backup_log_files;
 	throw 0;
+#elif defined(_MSC_VER)
+	_exit(1);
 #else
 	_Exit(1);
 #endif
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 32efe4f0..66bbf042 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -866,6 +866,13 @@ namespace {
 				return;
 			}
 
+			if (cell->type == "$ff") {
+				port("\\D", param("\\WIDTH"));
+				port("\\Q", param("\\WIDTH"));
+				check_expected();
+				return;
+			}
+
 			if (cell->type == "$dff") {
 				param_bool("\\CLK_POLARITY");
 				port("\\CLK", 1);
@@ -1030,7 +1037,7 @@ namespace {
 				return;
 			}
 
-			if (cell->type == "$anyconst") {
+			if (cell->type.in("$anyconst", "$anyseq")) {
 				port("\\Y", param("\\WIDTH"));
 				check_expected();
 				return;
@@ -1069,6 +1076,7 @@ namespace {
 			if (cell->type == "$_SR_PN_") { check_gate("SRQ"); return; }
 			if (cell->type == "$_SR_PP_") { check_gate("SRQ"); return; }
 
+			if (cell->type == "$_FF_")    { check_gate("DQ");  return; }
 			if (cell->type == "$_DFF_N_") { check_gate("DQC"); return; }
 			if (cell->type == "$_DFF_P_") { check_gate("DQC"); return; }
 
@@ -1830,6 +1838,15 @@ RTLIL::Cell* RTLIL::Module::addSr(RTLIL::IdString name, RTLIL::SigSpec sig_set,
 	return cell;
 }
 
+RTLIL::Cell* RTLIL::Module::addFf(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q)
+{
+	RTLIL::Cell *cell = addCell(name, "$ff");
+	cell->parameters["\\WIDTH"] = sig_q.size();
+	cell->setPort("\\D", sig_d);
+	cell->setPort("\\Q", sig_q);
+	return cell;
+}
+
 RTLIL::Cell* RTLIL::Module::addDff(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity)
 {
 	RTLIL::Cell *cell = addCell(name, "$dff");
@@ -1912,6 +1929,14 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, RTLIL::SigSpec sig
 	return cell;
 }
 
+RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q)
+{
+	RTLIL::Cell *cell = addCell(name, "$_FF_");
+	cell->setPort("\\D", sig_d);
+	cell->setPort("\\Q", sig_q);
+	return cell;
+}
+
 RTLIL::Cell* RTLIL::Module::addDffGate(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity)
 {
 	RTLIL::Cell *cell = addCell(name, stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'));
@@ -1984,6 +2009,15 @@ RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width)
 	return sig;
 }
 
+RTLIL::SigSpec RTLIL::Module::Anyseq(RTLIL::IdString name, int width)
+{
+	RTLIL::SigSpec sig = addWire(NEW_ID, width);
+	Cell *cell = addCell(name, "$anyseq");
+	cell->setParam("\\WIDTH", width);
+	cell->setPort("\\Y", sig);
+	return sig;
+}
+
 RTLIL::SigSpec RTLIL::Module::Initstate(RTLIL::IdString name)
 {
 	RTLIL::SigSpec sig = addWire(NEW_ID);
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index a426e0bd..9430dcb3 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -42,7 +42,8 @@ namespace RTLIL
 		STn = 3, // edge sensitive: negedge
 		STe = 4, // edge sensitive: both edges
 		STa = 5, // always active
-		STi = 6  // init
+		STg = 6, // global clock
+		STi = 7  // init
 	};
 
 	enum ConstFlags : unsigned char {
@@ -1008,6 +1009,7 @@ public:
 	RTLIL::Cell* addEquiv  (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y);
 
 	RTLIL::Cell* addSr    (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true);
+	RTLIL::Cell* addFf    (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q);
 	RTLIL::Cell* addDff   (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d,   RTLIL::SigSpec sig_q, bool clk_polarity = true);
 	RTLIL::Cell* addDffe  (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en,  RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true);
 	RTLIL::Cell* addDffsr (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr,
@@ -1032,6 +1034,7 @@ public:
 	RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y);
 	RTLIL::Cell* addOai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y);
 
+	RTLIL::Cell* addFfGate     (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q);
 	RTLIL::Cell* addDffGate    (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true);
 	RTLIL::Cell* addDffeGate   (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true);
 	RTLIL::Cell* addDffsrGate  (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr,
@@ -1105,6 +1108,7 @@ public:
 	RTLIL::SigBit Oai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d);
 
 	RTLIL::SigSpec Anyconst  (RTLIL::IdString name, int width = 1);
+	RTLIL::SigSpec Anyseq    (RTLIL::IdString name, int width = 1);
 	RTLIL::SigSpec Initstate (RTLIL::IdString name);
 };
 
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 0a65b490..690f8e33 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -1293,7 +1293,7 @@ struct SatGen
 			return true;
 		}
 
-		if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_"))
+		if (timestep > 0 && cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_"))
 		{
 			if (timestep == 1)
 			{
@@ -1332,8 +1332,8 @@ struct SatGen
 
 			if (model_undef)
 			{
-				std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1);
-				std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep);
+				std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\Y"), timestep-1);
+				std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Y"), timestep);
 
 				ez->assume(ez->vec_eq(undef_d, undef_q));
 				undefGating(q, qq, undef_q);
@@ -1341,6 +1341,11 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$anyseq")
+		{
+			return true;
+		}
+
 		if (cell->type == "$_BUF_" || cell->type == "$equiv")
 		{
 			std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
diff --git a/kernel/yosys.h b/kernel/yosys.h
index aab6b584..ae73146b 100644
--- a/kernel/yosys.h
+++ b/kernel/yosys.h
@@ -64,6 +64,7 @@
 #include <string.h>
 #include <stdint.h>
 #include <stdio.h>
+#include <limits.h>
 
 #ifndef _YOSYS_
 #  error It looks like you are trying to build Yosys without the config defines set. \
@@ -100,6 +101,10 @@
 #  endif
 #endif
 
+#ifndef PATH_MAX
+#  define PATH_MAX 4096
+#endif
+
 #define PRIVATE_NAMESPACE_BEGIN  namespace {
 #define PRIVATE_NAMESPACE_END    }
 #define YOSYS_NAMESPACE_BEGIN    namespace Yosys {
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index bd73ae23..a831fdf3 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -421,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber
 using the {\tt abc} pass.
 
 \begin{fixme}
-Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, and {\tt \$anyconst} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
 \end{fixme}
 
 \begin{fixme}
@@ -437,6 +437,10 @@ Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cel
 \end{fixme}
 
 \begin{fixme}
+Add information about {\tt \$ff} and {\tt \$\_FF\_} cells.
+\end{fixme}
+
+\begin{fixme}
 Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells.
 \end{fixme}
 
diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex
index 425d89b6..8af8ccdd 100644
--- a/manual/command-reference-manual.tex
+++ b/manual/command-reference-manual.tex
@@ -9,7 +9,7 @@ This pass uses the ABC tool [1] for technology mapping of yosys's internal gate
 library to a target architecture.
 
     -exe <command>
-        use the specified command name instead of "yosys-abc" to execute ABC.
+        use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC.
         This can e.g. be used to call a specific version of ABC or a wrapper.
 
     -script <file>
@@ -23,33 +23,45 @@ library to a target architecture.
         if no -script parameter is given, the following scripts are used:
 
         for -liberty without -constr:
-          strash; scorr; ifraig; retime {D}; strash; dch -f; map {D}
+          strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f;
+               map {D}
 
         for -liberty with -constr:
-          strash; scorr; ifraig; retime {D}; strash; dch -f; map {D};
-               buffer; upsize {D}; dnsize {D}; stime -p
+          strash; dc2; scorr; ifraig; retime -o {D}; strash; dch -f;
+               map {D}; buffer; upsize {D}; dnsize {D}; stime -p
 
-        for -lut:
-          strash; scorr; ifraig; retime; strash; dch -f; if
+        for -lut/-luts (only one LUT size):
+          strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs;
+               lutpack
+
+        for -lut/-luts (different LUT sizes):
+          strash; dc2; scorr; ifraig; retime -o; strash; dch -f; if; mfs
+
+        for -sop:
+          strash; dc2; scorr; ifraig; retime -o; strash; dch -f;
+               cover {I} {P}
 
         otherwise:
-          strash; scorr; ifraig; retime; strash; dch -f; map
+          strash; dc2; scorr; ifraig; retime -o; strash; dch -f; map
 
     -fast
         use different default scripts that are slightly faster (at the cost
         of output quality):
 
         for -liberty without -constr:
-          retime {D}; map {D}
+          retime -o {D}; map {D}
 
         for -liberty with -constr:
-          retime {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p
+          retime -o {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p
 
-        for -lut:
-          retime; if
+        for -lut/-luts:
+          retime -o; if
+
+        for -sop:
+          retime -o; cover -I {I} -P {P}
 
         otherwise:
-          retime; map
+          retime -o; map
 
     -liberty <file>
         generate netlists for the specified cell library (using the liberty
@@ -70,6 +82,14 @@ library to a target architecture.
         set delay target. the string {D} in the default scripts above is
         replaced by this option when used, and an empty string otherwise.
 
+    -I <num>
+        maximum number of SOP inputs.
+        (replaces {I} in the default scripts above)
+
+    -P <num>
+        maximum number of SOP products.
+        (replaces {P} in the default scripts above)
+
     -lut <width>
         generate netlist using luts of (max) the specified width.
 
@@ -83,6 +103,9 @@ library to a target architecture.
         generate netlist using luts. Use the specified costs for luts with 1,
         2, 3, .. inputs.
 
+    -sop
+        map to sum-of-product cells and inverters
+
     -g type1,type2,...
         Map the the specified list of gate types. Supported gates types are:
         AND, NAND, OR, NOR, XOR, XNOR, MUX, AOI3, OAI3, AOI4, OAI4.
@@ -166,6 +189,85 @@ This pass translates arithmetic operations like $add, $mul, $lt, etc. to $alu
 and $macc cells.
 \end{lstlisting}
 
+\section{assertpmux -- convert internal signals to module ports}
+\label{cmd:assertpmux}
+\begin{lstlisting}[numbers=left,frame=single]
+    assertpmux [options] [selection]
+
+This command adds asserts to the design that assert that all parallel muxes
+($pmux cells) have a maximum of one of their inputs enable at any time.
+
+    -noinit
+        do not enforce the pmux condition during the init state
+
+    -always
+        usually the $pmux condition is only checked when the $pmux output
+        is used be the mux tree it drives. this option will deactivate this
+        additional constrained and check the $pmux condition always.
+\end{lstlisting}
+
+\section{attrmap -- renaming attributes}
+\label{cmd:attrmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    attrmap [options] [selection]
+
+This command renames attributes and/or mapps key/value pairs to
+other key/value pairs.
+
+    -tocase <name>
+        Match attribute names case-insensitively and set it to the specified
+        name.
+
+    -rename <old_name> <new_name>
+        Rename attributes as specified
+
+    -map <old_name>=<old_value> <new_name>=<new_value>
+        Map key/value pairs as indicated.
+
+    -imap <old_name>=<old_value> <new_name>=<new_value>
+        Like -map, but use case-insensitive match for <old_value> when
+        it is a string value.
+
+    -remove <name>=<value>
+        Remove attributes matching this pattern.
+
+    -modattr
+        Operate on module attributes instead of attributes on wires and cells.
+
+For example, mapping Xilinx-style "keep" attributes to Yosys-style:
+
+    attrmap -tocase keep -imap keep="true" keep=1 \
+            -imap keep="false" keep=0 -remove keep=0
+\end{lstlisting}
+
+\section{attrmvcp -- move or copy attributes from wires to driving cells}
+\label{cmd:attrmvcp}
+\begin{lstlisting}[numbers=left,frame=single]
+    attrmvcp [options] [selection]
+
+Move or copy attributes on wires to the cells driving them.
+
+    -copy
+        By default, attributes are moved. This will only add
+        the attribute to the cell, without removing it from
+        the wire.
+
+    -purge
+        If no selected cell consumes the attribute, then it is
+        left on the wire by default. This option will cause the
+        attribute to be removed from the wire, even if no selected
+        cell takes it.
+
+    -driven
+        By default, attriburtes are moved to the cell driving the
+        wire. With this option set it will be moved to the cell
+        driven by the wire instead.
+
+    -attr <attrname>
+        Move or copy this attribute. This option can be used
+        multiple times.
+\end{lstlisting}
+
 \section{cd -- a shortcut for 'select -module <name>'}
 \label{cmd:cd}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -233,6 +335,16 @@ When commands are separated using the ';;;' token, this command will be executed
 in -purge mode between the commands.
 \end{lstlisting}
 
+\section{clk2fflogic -- convert clocked FFs to generic \$ff cells}
+\label{cmd:clk2fflogic}
+\begin{lstlisting}[numbers=left,frame=single]
+    clk2fflogic [options] [selection]
+
+This command replaces clocked flip-flops with generic $ff cells that use the
+implicit global clock. This is useful for formal verification of designs with
+multiple clocks.
+\end{lstlisting}
+
 \section{connect -- create or remove connections}
 \label{cmd:connect}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -356,6 +468,14 @@ Does not delete any object but removes the input and/or output flag on the
 selected wires, thus 'deleting' module ports.
 \end{lstlisting}
 
+\section{deminout -- demote inout ports to input or output}
+\label{cmd:deminout}
+\begin{lstlisting}[numbers=left,frame=single]
+    deminout [options] [selection]
+
+"Demote" inout ports to input or output ports, if possible.
+\end{lstlisting}
+
 \section{design -- save, restore and reset current design}
 \label{cmd:design}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -910,6 +1030,9 @@ Options:
     -expand, -norecode, -export, -nomap
         enable or disable passes as indicated above
 
+    -fullexpand
+        call expand with -full option
+
     -encoding type
     -fm_set_fsm_file file
     -encfile file
@@ -934,11 +1057,14 @@ Signals can be protected from being detected by this pass by setting the
 \section{fsm\_expand -- expand FSM cells by merging logic into it}
 \label{cmd:fsm_expand}
 \begin{lstlisting}[numbers=left,frame=single]
-    fsm_expand [selection]
+    fsm_expand [-full] [selection]
 
 The fsm_extract pass is conservative about the cells that belong to a finite
 state machine. This pass can be used to merge additional auxiliary gates into
 the finite state machine.
+
+By default, fsm_expand is still a bit conservative regarding merging larger
+word-wide cells. Call with -full to consider all cells for merging.
 \end{lstlisting}
 
 \section{fsm\_export -- exporting FSMs to KISS2 files}
@@ -1029,6 +1155,23 @@ one-hot encoding and binary encoding is supported.
             .map <old_bitpattern> <new_bitpattern>
 \end{lstlisting}
 
+\section{greenpak4\_counters -- Extract GreenPak4 counter cells}
+\label{cmd:greenpak4_counters}
+\begin{lstlisting}[numbers=left,frame=single]
+    greenpak4_counters [options] [selection]
+
+This pass converts non-resettable or async resettable down counters to GreenPak4
+counter cells (All other GreenPak4 counter modes must be instantiated manually.)
+\end{lstlisting}
+
+\section{greenpak4\_dffinv -- merge greenpak4 inverters and DFFs}
+\label{cmd:greenpak4_dffinv}
+\begin{lstlisting}[numbers=left,frame=single]
+    greenpak4_dffinv [options] [selection]
+
+Merge GP_INV cells with GP_DFF* cells.
+\end{lstlisting}
+
 \section{help -- display help messages}
 \label{cmd:help}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1157,11 +1300,26 @@ This command executes the following script:
 
     do
         <ice40 specific optimizations>
-        opt_const -mux_undef -undriven [-full]
-        opt_share
+        opt_expr -mux_undef -undriven [-full]
+        opt_merge
         opt_rmdff
         opt_clean
     while <changed design>
+
+When called with the option -unlut, this command will transform all already
+mapped SB_LUT4 cells back to logic.
+\end{lstlisting}
+
+\section{insbuf -- insert buffer cells for connected wires}
+\label{cmd:insbuf}
+\begin{lstlisting}[numbers=left,frame=single]
+    insbuf [options] [selection]
+
+Insert buffer cells into the design for directly connected wires.
+
+    -buf <celltype> <in-portname> <out-portname>
+        Use the given cell type instead of $_BUF_. (Notice that the next
+        call to "clean" will remove all $_BUF_ in the design.)
 \end{lstlisting}
 
 \section{iopadmap -- technology mapping of i/o pads (or buffers)}
@@ -1177,12 +1335,23 @@ the resulting cells to more sophisticated PAD cells.
         Map module input ports to the given cell type with the
         given output port name. if a 2nd portname is given, the
         signal is passed through the pad call, using the 2nd
-        portname as input.
+        portname as the port facing the module port.
 
     -outpad <celltype> <portname>[:<portname>]
     -inoutpad <celltype> <portname>[:<portname>]
         Similar to -inpad, but for output and inout ports.
 
+    -toutpad <celltype> <portname>:<portname>[:<portname>]
+        Merges $_TBUF_ cells into the output pad cell. This takes precedence
+        over the other -outpad cell. The first portname is the enable input
+        of the tristate driver.
+
+    -tinoutpad <celltype> <portname>:<portname>:<portname>[:<portname>]
+        Merges $_TBUF_ cells into the inout pad cell. This takes precedence
+        over the other -inoutpad cell. The first portname is the enable input
+        of the tristate driver and the 2nd portname is the internal output
+        buffering the external signal.
+
     -widthparam <param_name>
         Use the specified parameter name to set the port width.
 
@@ -1193,6 +1362,8 @@ the resulting cells to more sophisticated PAD cells.
         create individual bit-wide buffers even for ports that
         are wider. (the default behavior is to create word-wide
         buffers using -widthparam to set the word size on the cell.)
+
+Tristate PADS (-toutpad, -tinoutpad) always operate in -bits mode.
 \end{lstlisting}
 
 \section{json -- write design in JSON format}
@@ -1265,14 +1436,15 @@ is used then the $macc cell is mapped to $add, $sub, etc. cells instead.
 \section{memory -- translate memories to basic cells}
 \label{cmd:memory}
 \begin{lstlisting}[numbers=left,frame=single]
-    memory [-nomap] [-nordff] [-bram <bram_rules>] [selection]
+    memory [-nomap] [-nordff] [-memx] [-bram <bram_rules>] [selection]
 
 This pass calls all the other memory_* passes in a useful order:
 
-    memory_dff [-nordff]
+    memory_dff [-nordff]                (-memx implies -nordff)
     opt_clean
     memory_share
     opt_clean
+    memory_memx                         (when called with -memx)
     memory_collect
     memory_bram -rules <bram_rules>     (when called with -bram)
     memory_map                          (skipped if called with -nomap)
@@ -1401,6 +1573,15 @@ This pass converts multiport memory cells as generated by the memory_collect
 pass to word-wide DFFs and address decoders.
 \end{lstlisting}
 
+\section{memory\_memx -- emulate vlog sim behavior for mem ports}
+\label{cmd:memory_memx}
+\begin{lstlisting}[numbers=left,frame=single]
+    memory_memx [selection]
+
+This pass adds additional circuitry that emulates the Verilog simulation
+behavior for out-of-bounds memory reads and writes.
+\end{lstlisting}
+
 \section{memory\_share -- consolidate memory ports}
 \label{cmd:memory_share}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1423,7 +1604,7 @@ The following methods are used to consolidate the number of memory ports:
 
 Note that in addition to the algorithms implemented in this pass, the $memrd
 and $memwr cells are also subject to generic resource sharing passes (and other
-optimizations) such as opt_share.
+optimizations) such as "share" and "opt_merge".
 \end{lstlisting}
 
 \section{memory\_unpack -- unpack multi-port memory cells}
@@ -1461,7 +1642,7 @@ detected.
         also create an 'assert' cell that checks if trigger is always low.
 
     -flatten
-        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.
+        call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.
 
 
     miter -assert [options] module [miter_name]
@@ -1475,7 +1656,7 @@ module is modified.
         keep module output ports.
 
     -flatten
-        call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.
+        call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.
 \end{lstlisting}
 
 \section{muxcover -- cover trees of MUX cells with wider MUXes}
@@ -1507,6 +1688,9 @@ provides a small number of differently sized LUTs.
         The number of LUTs with 1, 2, 3, ... inputs that are
         available in the target architecture.
 
+    -assert
+        Create an error if not all logic can be mapped
+
 Excess logic that does not fit into the specified LUTs is mapped back
 to generic logic gates ($_AND_, etc.).
 \end{lstlisting}
@@ -1520,24 +1704,24 @@ This pass calls all the other opt_* passes in a useful order. This performs
 a series of trivial optimizations and cleanups. This pass executes the other
 passes in the following order:
 
-    opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
-    opt_share [-share_all] -nomux
+    opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+    opt_merge [-share_all] -nomux
 
     do
         opt_muxtree
         opt_reduce [-fine] [-full]
-        opt_share [-share_all]
-        opt_rmdff
+        opt_merge [-share_all]
+        opt_rmdff [-keepdc]
         opt_clean [-purge]
-        opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
     while <changed design>
 
 When called with -fast the following script is used instead:
 
     do
-        opt_const [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
-        opt_share [-share_all]
-        opt_rmdff
+        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]
+        opt_merge [-share_all]
+        opt_rmdff [-keepdc]
         opt_clean [-purge]
     while <changed design in opt_rmdff>
 
@@ -1561,12 +1745,13 @@ This pass only operates on completely selected modules without processes.
         also remove internal nets if they have a public name
 \end{lstlisting}
 
-\section{opt\_const -- perform const folding}
-\label{cmd:opt_const}
+\section{opt\_expr -- perform const folding and simple expression rewriting}
+\label{cmd:opt_expr}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_const [options] [selection]
+    opt_expr [options] [selection]
 
 This pass performs const folding on internal cell types with constant inputs.
+It also performs some simple expression rewritring.
 
     -mux_undef
         remove 'undef' inputs from $mux, $pmux and $_MUX_ cells
@@ -1593,6 +1778,21 @@ This pass performs const folding on internal cell types with constant inputs.
         replaced by 'a'. the -keepdc option disables all such optimizations.
 \end{lstlisting}
 
+\section{opt\_merge -- consolidate identical cells}
+\label{cmd:opt_merge}
+\begin{lstlisting}[numbers=left,frame=single]
+    opt_merge [options] [selection]
+
+This pass identifies cells with identical type and input signals. Such cells
+are then merged to one cell.
+
+    -nomux
+        Do not merge MUX cells.
+
+    -share_all
+        Operate on all cell types, not just built-in types.
+\end{lstlisting}
+
 \section{opt\_muxtree -- eliminate dead trees in multiplexer trees}
 \label{cmd:opt_muxtree}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1628,27 +1828,12 @@ input with the original control signals OR'ed together.
 \section{opt\_rmdff -- remove DFFs with constant inputs}
 \label{cmd:opt_rmdff}
 \begin{lstlisting}[numbers=left,frame=single]
-    opt_rmdff [selection]
+    opt_rmdff [-keepdc] [selection]
 
 This pass identifies flip-flops with constant inputs and replaces them with
 a constant driver.
 \end{lstlisting}
 
-\section{opt\_share -- consolidate identical cells}
-\label{cmd:opt_share}
-\begin{lstlisting}[numbers=left,frame=single]
-    opt_share [options] [selection]
-
-This pass identifies cells with identical type and input signals. Such cells
-are then merged to one cell.
-
-    -nomux
-        Do not merge MUX cells.
-
-    -share_all
-        Operate on all cell types, not just built-in types.
-\end{lstlisting}
-
 \section{plugin -- load and list loaded plugins}
 \label{cmd:plugin}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -1686,9 +1871,30 @@ on partly selected designs.
     -top <module>
         use the specified module as top module (default='top')
 
+    -auto-top
+        automatically determine the top of the design hierarchy
+
+    -flatten
+        flatten the design before synthesis. this will pass '-auto-top' to
+        'hierarchy' if no top module is specified.
+
+    -ifx
+        passed to 'proc'. uses verilog simulation behavior for verilog if/case
+        undef handling. this also prevents 'wreduce' from being run.
+
+    -memx
+        simulate verilog simulation behavior for out-of-bounds memory accesses
+        using the 'memory_memx' pass. This option implies -nordff.
+
+    -nomem
+        do not run any of the memory_* passes
+
     -nordff
         passed to 'memory_dff'. prohibits merging of FFs into memory read ports
 
+     -nokeepdc
+        do not call opt_* with -keepdc
+
     -run <from_label>[:<to_label>]
         only run the commands between the labels (see below). an empty
         from label is synonymous to 'begin', and empty to label is
@@ -1698,16 +1904,18 @@ on partly selected designs.
 The following commands are executed by this synthesis command:
 
     begin:
-        hierarchy -check [-top <top>]
+        hierarchy -check [-top <top> | -auto-top]
 
-    prep:
-        proc
-        opt_const
+    coarse:
+        proc [-ifx]
+        flatten    (if -flatten)
+        opt_expr -keepdc
         opt_clean
         check
         opt -keepdc
-        wreduce
+        wreduce [-memx]
         memory_dff [-nordff]
+        memory_memx    (if -memx)
         opt_clean
         memory_collect
         opt -keepdc -fast
@@ -1740,6 +1948,10 @@ The following options are supported:
 
     -global_arst [!]<netname>
         This option is passed through to proc_arst.
+
+    -ifx
+        This option is passed through to proc_mux. proc_rmdead is not
+        executed in -ifx mode.
 \end{lstlisting}
 
 \section{proc\_arst -- detect asynchronous resets}
@@ -1799,10 +2011,14 @@ respective wire.
 \section{proc\_mux -- convert decision trees to multiplexers}
 \label{cmd:proc_mux}
 \begin{lstlisting}[numbers=left,frame=single]
-    proc_mux [selection]
+    proc_mux [options] [selection]
 
 This pass converts the decision trees in processes (originating from if-else
 and case statements) to trees of multiplexer cells.
+
+    -ifx
+        Use Verilog simulation behavior with respect to undef values in
+        'case' expressions and 'if' conditions.
 \end{lstlisting}
 
 \section{proc\_rmdead -- eliminate dead trees in decision trees}
@@ -1835,6 +2051,9 @@ annotates the cells in the design with 'qwp_position' attributes.
     -dump <html_file_name>
         Dump a protocol of the placement algorithm to the html file.
 
+    -v
+        Verbose solver output for profiling or debugging
+
 Note: This implementation of a quadratic wirelength placer uses exact
 dense matrix operations. It is only a toy-placer for small circuits.
 \end{lstlisting}
@@ -1845,6 +2064,9 @@ dense matrix operations. It is only a toy-placer for small circuits.
     read_blif [filename]
 
 Load modules from a BLIF file into the current design.
+
+    -sop
+        Create $sop cells instead of $lut cells
 \end{lstlisting}
 
 \section{read\_ilang -- read modules from ilang file}
@@ -1894,9 +2116,15 @@ Verilog-2005 is supported.
         of SystemVerilog is supported)
 
     -formal
-        enable support for assert() and assume() from SystemVerilog
+        enable support for SystemVerilog assertions and some Yosys extensions
         replace the implicit -D SYNTHESIS with -D FORMAL
 
+    -norestrict
+        ignore restrict() assertions
+
+    -assume-asserts
+        treat all assert() statements like assume() statements
+
     -dump_ast1
         dump abstract syntax tree (before simplification)
 
@@ -1906,6 +2134,9 @@ Verilog-2005 is supported.
     -dump_vlog
         dump ast as Verilog code (after simplification)
 
+    -dump_rtlil
+        dump generated RTLIL netlist
+
     -yydebug
         enable parser debug output
 
@@ -1989,6 +2220,9 @@ Note that the Verilog frontend does a pretty good job of processing valid
 verilog input, but has not very good error reporting. It generally is
 recommended to use a simulator (for example Icarus Verilog) for checking
 the syntax of the code, rather than to rely on read_verilog for that.
+
+See the Yosys README file for a list of non-standard Verilog features
+supported by the Yosys Verilog front-end.
 \end{lstlisting}
 
 \section{rename -- rename object in the design}
@@ -2254,7 +2488,7 @@ marked with that label (until the next label) is executed.
 \label{cmd:select}
 \begin{lstlisting}[numbers=left,frame=single]
     select [ -add | -del | -set <name> ] {-read <filename> | <selection>}
-    select [ -assert-none | -assert-any ] {-read <filename> | <selection>}
+    select [ <assert_option> ] {-read <filename> | <selection>}
     select [ -list | -write <filename> | -count | -clear ]
     select -module <modname>
 
@@ -2290,6 +2524,14 @@ described here.
         do not modify the current selection. instead assert that the given
         selection contains exactly N objects.
 
+    -assert-max N
+        do not modify the current selection. instead assert that the given
+        selection contains less than or exactly N objects.
+
+    -assert-min N
+        do not modify the current selection. instead assert that the given
+        selection contains at least N objects.
+
     -list
         list all objects in the current selection
 
@@ -2473,10 +2715,12 @@ instead of objects within modules.
 \section{setparam -- set/unset parameters on objects}
 \label{cmd:setparam}
 \begin{lstlisting}[numbers=left,frame=single]
-    setparam [ -set name value | -unset name ]... [selection]
+    setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection]
 
 Set/unset the given parameters on the selected cells. String values must be
 passed in double quotes (").
+
+The -type option can be used to change the cell type of the selected cells.
 \end{lstlisting}
 
 \section{setundef -- replace undef values with defined constants}
@@ -2498,6 +2742,9 @@ This command replaced undef (x) constants with defined (0/1) constants.
     -random <seed>
         replace with random bits using the specified integer als seed
         value for the random number generator.
+
+    -init
+        also create/update init values for flip-flops
 \end{lstlisting}
 
 \section{share -- perform sat-based resource sharing}
@@ -2576,8 +2823,9 @@ to a graphics file (usually SVG or PostScript).
         Run the specified command with the graphics file as parameter.
 
     -format <format>
-        Generate a graphics file in the specified format.
-        Usually <format> is 'svg' or 'ps'.
+        Generate a graphics file in the specified format. Use 'dot' to just
+        generate a .dot file, or other <format> strings such as 'svg' or 'ps'
+        to generate files in other formats (this calls the 'dot' command).
 
     -lib <verilog_or_ilang_file>
         Use the specified library file for determining whether cell ports are
@@ -2640,7 +2888,65 @@ The generated output files are '~/.yosys_show.dot' and '~/.yosys_show.<format>',
 unless another prefix is specified using -prefix <prefix>.
 
 Yosys on Windows and YosysJS use different defaults: The output is written
-to 'show.dot' in the current directory and new viewer is launched.
+to 'show.dot' in the current directory and new viewer is launched each time
+the 'show' command is executed.
+\end{lstlisting}
+
+\section{shregmap -- map shift registers}
+\label{cmd:shregmap}
+\begin{lstlisting}[numbers=left,frame=single]
+    shregmap [options] [selection]
+
+This pass converts chains of $_DFF_[NP]_ gates to target specific shift register
+primitives. The generated shift register will be of type $__SHREG_DFF_[NP]_ and
+will use the same interface as the original $_DFF_*_ cells. The cell parameter
+'DEPTH' will contain the depth of the shift register. Use a target-specific
+'techmap' map file to convert those cells to the actual target cells.
+
+    -minlen N
+        minimum length of shift register (default = 2)
+        (this is the length after -keep_before and -keep_after)
+
+    -maxlen N
+        maximum length of shift register (default = no limit)
+        larger chains will be mapped to multiple shift register instances
+
+    -keep_before N
+        number of DFFs to keep before the shift register (default = 0)
+
+    -keep_after N
+        number of DFFs to keep after the shift register (default = 0)
+
+    -clkpol pos|neg|any
+        limit match to only positive or negative edge clocks. (default = any)
+
+    -enpol pos|neg|none|any_or_none|any
+        limit match to FFs with the specified enable polarity. (default = none)
+
+    -match <cell_type>[:<d_port_name>:<q_port_name>]
+        match the specified cells instead of $_DFF_N_ and $_DFF_P_. If
+        ':<d_port_name>:<q_port_name>' is omitted then 'D' and 'Q' is used
+        by default. E.g. the option '-clkpol pos' is just an alias for
+        '-match $_DFF_P_', which is an alias for '-match $_DFF_P_:D:Q'.
+
+    -params
+        instead of encoding the clock and enable polarity in the cell name by
+        deriving from the original cell name, simply name all generated cells
+        $__SHREG_ and use CLKPOL and ENPOL parameters. An ENPOL value of 2 is
+        used to denote cells without enable input. The ENPOL parameter is
+        omitted when '-enpol none' (or no -enpol option) is passed.
+
+    -zinit
+        assume the shift register is automatically zero-initialized, so it
+        becomes legal to merge zero initialized FFs into the shift register.
+
+    -init
+        map initialized registers to the shift reg, add an INIT parameter to
+        generated cells with the initialization value. (first bit to shift out
+        in LSB position)
+
+    -tech greenpak4
+        map to greenpak4 shift registers.
 \end{lstlisting}
 
 \section{simplemap -- mapping simple coarse-grain cells}
@@ -2654,7 +2960,7 @@ primitives. The following internal cell types are mapped by this pass:
   $not, $pos, $and, $or, $xor, $xnor
   $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool
   $logic_not, $logic_and, $logic_or, $mux, $tribuf
-  $sr, $dff, $dffsr, $adff, $dlatch
+  $sr, $ff, $dff, $dffsr, $adff, $dlatch
 \end{lstlisting}
 
 \section{singleton -- create singleton modules}
@@ -2793,6 +3099,13 @@ on partly selected designs.
     -top <module>
         use the specified module as top module (default='top')
 
+    -auto-top
+        automatically determine the top of the design hierarchy
+
+    -flatten
+        flatten the design before synthesis. this will pass '-auto-top' to
+        'hierarchy' if no top module is specified.
+
     -encfile <file>
         passed to 'fsm_recode' via 'fsm'
 
@@ -2818,11 +3131,12 @@ on partly selected designs.
 The following commands are executed by this synthesis command:
 
     begin:
-        hierarchy -check [-top <top>]
+        hierarchy -check [-top <top> | -auto-top]
 
     coarse:
         proc
-        opt_const
+        flatten    (if -flatten)
+        opt_expr
         opt_clean
         check
         opt
@@ -2850,6 +3164,73 @@ The following commands are executed by this synthesis command:
         check
 \end{lstlisting}
 
+\section{synth\_gowin -- synthesis for Gowin FPGAs}
+\label{cmd:synth_gowin}
+\begin{lstlisting}[numbers=left,frame=single]
+    synth_gowin [options]
+
+This command runs synthesis for Gowin FPGAs. This work is experimental.
+
+    -top <module>
+        use the specified module as top module (default='top')
+
+    -vout <file>
+        write the design to the specified Verilog netlist file. writing of an
+        output file is omitted if this parameter is not specified.
+
+    -run <from_label>:<to_label>
+        only run the commands between the labels (see below). an empty
+        from label is synonymous to 'begin', and empty to label is
+        synonymous to the end of the command list.
+
+    -retime
+        run 'abc' with -dff option
+
+
+The following commands are executed by this synthesis command:
+
+    begin:
+        read_verilog -lib +/gowin/cells_sim.v
+        hierarchy -check -top <top>
+
+    flatten:
+        proc
+        flatten
+        tribuf -logic
+        deminout
+
+    coarse:
+        synth -run coarse
+
+    fine:
+        opt -fast -mux_undef -undriven -fine
+        memory_map
+        opt -undriven -fine
+        techmap
+        clean -purge
+        splitnets -ports
+        setundef -undriven -zero
+        abc -dff    (only if -retime)
+
+    map_luts:
+        abc -lut 4
+        clean
+
+    map_cells:
+        techmap -map +/gowin/cells_map.v
+        hilomap -hicell VCC V -locell GND G
+        iopadmap -inpad IBUF O:I -outpad OBUF I:O
+        clean -purge
+
+    check:
+        hierarchy -check
+        stat
+        check -noinit
+
+    vout:
+        write_verilog -attr2comment -defparam -renameprefix gen <file-name>
+\end{lstlisting}
+
 \section{synth\_greenpak4 -- synthesis for GreenPAK4 FPGAs}
 \label{cmd:synth_greenpak4}
 \begin{lstlisting}[numbers=left,frame=single]
@@ -2860,12 +3241,12 @@ This command runs synthesis for GreenPAK4 FPGAs. This work is experimental.
     -top <module>
         use the specified module as top module (default='top')
 
-    -blif <file>
-        write the design to the specified BLIF file. writing of an output file
-        is omitted if this parameter is not specified.
+    -part <part>
+        synthesize for the specified part. Valid values are SLG46140V,
+        SLG46620V, and SLG46621V (default).
 
-    -edif <file>
-        write the design to the specified edif file. writing of an output file
+    -json <file>
+        write the design to the specified JSON file. writing of an output file
         is omitted if this parameter is not specified.
 
     -run <from_label>:<to_label>
@@ -2886,7 +3267,7 @@ The following commands are executed by this synthesis command:
         read_verilog -lib +/greenpak4/cells_sim.v
         hierarchy -check -top <top>
 
-    flatten:         (unless -noflatten)
+    flatten:    (unless -noflatten)
         proc
         flatten
         tribuf -logic
@@ -2895,20 +3276,34 @@ The following commands are executed by this synthesis command:
         synth -run coarse
 
     fine:
+        greenpak4_counters
+        clean
         opt -fast -mux_undef -undriven -fine
         memory_map
         opt -undriven -fine
         techmap
         dfflibmap -prepare -liberty +/greenpak4/gp_dff.lib
         opt -fast
-        abc -dff     (only if -retime)
+        abc -dff    (only if -retime)
 
     map_luts:
-        nlutmap -luts 0,8,16,2
+        nlutmap -assert -luts 0,6,8,2     (for -part SLG46140V)
+        nlutmap -assert -luts 2,8,16,2    (for -part SLG46620V)
+        nlutmap -assert -luts 2,8,16,2    (for -part SLG46621V)
         clean
 
     map_cells:
+        shregmap -tech greenpak4
+        dfflibmap -liberty +/greenpak4/gp_dff.lib
+        dffinit -ff GP_DFF Q INIT
+        dffinit -ff GP_DFFR Q INIT
+        dffinit -ff GP_DFFS Q INIT
+        dffinit -ff GP_DFFSR Q INIT
+        iopadmap -bits -inpad GP_IBUF OUT:IN -outpad GP_OBUF IN:OUT -inoutpad GP_OBUF OUT:IN -toutpad GP_OBUFT OE:IN:OUT -tinoutpad GP_IOBUF OE:OUT:IN:IO
+        attrmvcp -attr src -attr LOC t:GP_OBUF t:GP_OBUFT t:GP_IOBUF n:*
+        attrmvcp -attr src -attr LOC -driven t:GP_IBUF n:*
         techmap -map +/greenpak4/cells_map.v
+        greenpak4_dffinv
         clean
 
     check:
@@ -2916,11 +3311,8 @@ The following commands are executed by this synthesis command:
         stat
         check -noinit
 
-    blif:
-        write_blif -gates -attr -param <file-name>
-
-    edif:
-        write_edif <file-name>
+    json:
+        write_json <file-name>
 \end{lstlisting}
 
 \section{synth\_ice40 -- synthesis for iCE40 FPGAs}
@@ -2928,7 +3320,7 @@ The following commands are executed by this synthesis command:
 \begin{lstlisting}[numbers=left,frame=single]
     synth_ice40 [options]
 
-This command runs synthesis for iCE40 FPGAs. This work is experimental.
+This command runs synthesis for iCE40 FPGAs.
 
     -top <module>
         use the specified module as top module (default='top')
@@ -2968,15 +3360,16 @@ The following commands are executed by this synthesis command:
         read_verilog -lib +/ice40/cells_sim.v
         hierarchy -check -top <top>
 
-    flatten:         (unless -noflatten)
+    flatten:    (unless -noflatten)
         proc
         flatten
         tribuf -logic
+        deminout
 
     coarse:
         synth -run coarse
 
-    bram:            (skip if -nobram)
+    bram:    (skip if -nobram)
         memory_bram -rules +/ice40/brams.txt
         techmap -map +/ice40/brams_map.v
 
@@ -2984,15 +3377,15 @@ The following commands are executed by this synthesis command:
         opt -fast -mux_undef -undriven -fine
         memory_map
         opt -undriven -fine
-        techmap -map +/techmap.v [-map +/ice40/arith_map.v]
-        abc -dff     (only if -retime)
+        techmap -map +/techmap.v -map +/ice40/arith_map.v
+        abc -dff    (only if -retime)
         ice40_opt
 
     map_ffs:
         dffsr2dff
         dff2dffe -direct-match $_DFF_*
         techmap -map +/ice40/cells_map.v
-        opt_const -mux_undef
+        opt_expr -mux_undef
         simplemap
         ice40_ffinit
         ice40_ffssr
@@ -3001,6 +3394,7 @@ The following commands are executed by this synthesis command:
     map_luts:
         abc          (only if -abc2)
         ice40_opt    (only if -abc2)
+        techmap -map +/ice40/latches_map.v
         abc -lut 4
         clean
 
@@ -3052,6 +3446,7 @@ The following commands are executed by this synthesis command:
 
     begin:
         read_verilog -lib +/xilinx/cells_sim.v
+        read_verilog -lib +/xilinx/cells_xtra.v
         read_verilog -lib +/xilinx/brams_bb.v
         read_verilog -lib +/xilinx/drams_bb.v
         hierarchy -check -top <top>
@@ -3258,6 +3653,9 @@ specified logfile(s).
 
     -a logfile
         Write output to this file, append if exists.
+
+    +INT, -INT
+        Add/subract INT from the -v setting for this command.
 \end{lstlisting}
 
 \section{test\_abcloop -- automatically test handling of loops in abc command}
@@ -3326,7 +3724,7 @@ cell types. Use for example 'all /$add' for all cell types except $add.
         pass this option to techmap.
 
     -simlib
-        use "techmap -map +/simlib.v -max_iter 2 -autoproc"
+        use "techmap -D SIMLIB_NOCHECKS -map +/simlib.v -max_iter 2 -autoproc"
 
     -aigmap
         instead of calling "techmap", call "aigmap"
@@ -3347,6 +3745,9 @@ cell types. Use for example 'all /$add' for all cell types except $add.
     -noeval
         do not check const-eval models
 
+    -edges
+        test cell edges db creator against sat-based implementation
+
     -v
         print additional debug information to the console
 
@@ -3425,10 +3826,13 @@ Add the specified options to the list of default options to read_verilog.
 
 
     verilog_defaults -clear
+
 Clear the list of Verilog default options.
 
 
-    verilog_defaults -push    verilog_defaults -pop
+    verilog_defaults -push
+    verilog_defaults -pop
+
 Push or pop the list of default options to a stack. Note that -push does
 not imply -clear.
 \end{lstlisting}
@@ -3480,6 +3884,12 @@ the 32 bit adders in the following code with adders of more appropriate widths:
     module test(input [3:0] a, b, c, output [7:0] y);
         assign y = a + b + c + 1;
     endmodule
+
+Options:
+
+    -memx
+        Do not change the width of memory address ports. Use this options in
+        flows that use the 'memory_memx' pass.
 \end{lstlisting}
 
 \section{write\_blif -- write design to BLIF file}
@@ -3505,7 +3915,14 @@ Write the current design to an BLIF file.
         use the specified cell types to drive nets that are constant 1, 0, or
         undefined. when '-' is used as <cell-type>, then <out-port> specifies
         the wire name to be used for the constant signal and no cell driving
-        that wire is generated.
+        that wire is generated. when '+' is used as <cell-type>, then <out-port>
+        specifies the wire name to be used for the constant signal and a .names
+        statement is generated to drive the wire.
+
+    -noalias
+        if a net name is aliasing another net name, then by default a net
+        without fanout is created that is driven by the other net. This option
+        suppresses the generation of this nets without fanout.
 
 The following options can be useful when the generated file is not going to be
 read by a BLIF parser but a custom tool. It is recommended to not name the output
@@ -3557,6 +3974,11 @@ Write the current design to an EDIF netlist file.
     -top top_module
         set the specified module as design top module
 
+    -nogndvcc
+        do not create "GND" and "VCC" cells. (this will produce an error
+        if the design contains constant nets. use "hilomap" to map to custom
+        constant drivers first)
+
 Unfortunately there are different "flavors" of the EDIF file format. This
 command generates EDIF files for the Xilinx place&route tools. It might be
 necessary to make small modifications to this command when a different tool
@@ -3831,10 +4253,10 @@ functions operating on that state.
 
 The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions
 are provided that can be used to access the values of the signals in the module.
-Only ports, and signals with the 'keep' attribute set are made available via
-such functions. Without the -bv option, multi-bit wires are exported as
-separate functions of type Bool for the individual bits. With the -bv option
-multi-bit wires are exported as single functions of type BitVec.
+By default only ports, registers, and wires with the 'keep' attribute set are
+made available via such functions. With the -nobv option, multi-bit wires are
+exported as separate functions of type Bool for the individual bits. Without
+-nobv multi-bit wires are exported as single functions of type BitVec.
 
 The '<mod>_t' function evaluates to 'true' when the given pair of states
 describes a valid state transition.
@@ -3846,29 +4268,33 @@ The '<mod>_u' function evaluates to 'true' when the given state satisfies
 the assumptions in the module.
 
 The '<mod>_i' function evaluates to 'true' when the given state conforms
-to the initial state.
+to the initial state. Furthermore the '<mod>_is' function should be asserted
+to be true for initial states in addition to '<mod>_i', and should be
+asserted to be false for non-initial states.
+
+For hierarchical designs, the '<mod>_h' function must be asserted for each
+state to establish the design hierarchy. The '<mod>_h <cellname>' function
+evaluates to the state corresponding to the given cell within <mod>.
 
     -verbose
         this will print the recursive walk used to export the modules.
 
-    -bv
-        enable support for BitVec (FixedSizeBitVectors theory). with this
-        option set multi-bit wires are represented using the BitVec sort and
+    -nobv
+        disable support for BitVec (FixedSizeBitVectors theory). without this
+        option multi-bit wires are represented using the BitVec sort and
         support for coarse grain cells (incl. arithmetic) is enabled.
 
-    -mem
-        enable support for memories (via ArraysEx theory). this option
-        also implies -bv. only $mem cells without merged registers in
+    -nomem
+        disable support for memories (via ArraysEx theory). this option is
+        implied by -nobv. only $mem cells without merged registers in
         read ports are supported. call "memory" with -nordff to make sure
         that no registers are merged into $mem read ports. '<mod>_m' functions
         will be generated for accessing the arrays that are used to represent
         memories.
 
-    -regs
-        also create '<mod>_n' functions for all registers.
-
     -wires
-        also create '<mod>_n' functions for all public wires.
+        create '<mod>_n' functions for all public wires. by default only ports,
+        registers, and wires with the 'keep' attribute are exported.
 
     -tpl <template_file>
         use the given template file. the line containing only the token '%%'
@@ -3960,6 +4386,10 @@ Write the current design to an SPICE netlist file.
     -nc_prefix
         prefix for not-connected nets (default: _NC)
 
+    -inames
+        include names of internal ($-prefixed) nets in outputs
+        (default is to use net numbers instead)
+
     -top top_module
         set the specified module as design top module
 \end{lstlisting}
@@ -3976,6 +4406,9 @@ Write the current design to a Verilog file.
         instead of a backslash prefix) are changed to short names in the
         format '_<number>_'.
 
+    -renameprefix <prefix>
+        insert this prefix in front of auto-generated instance names
+
     -noattr
         with this option no attributes are included in the output
 
@@ -3986,6 +4419,21 @@ Write the current design to a Verilog file.
         without this option all internal cells are converted to Verilog
         expressions.
 
+    -nodec
+        32-bit constant values are by default dumped as decimal numbers,
+        not bit pattern. This option decativates 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
+        as binary numbers.
+
+    -defparam
+        Use 'defparam' statements instead of the Verilog-2001 syntax for
+        cell parameters.
+
     -blackboxes
         usually modules with the 'blackbox' attribute are ignored. with
         this option set only the modules with the 'blackbox' attribute
@@ -3994,5 +4442,25 @@ Write the current design to a Verilog file.
     -selected
         only write selected modules. modules must be selected entirely or
         not at all.
+
+    -v
+        verbose output (print new names of all renamed wires and cells)
+
+Note that RTLIL processes can't always be mapped directly to Verilog
+always blocks. This frontend should only be used to export an RTLIL
+netlist, i.e. after the "proc" pass has been used to convert all
+processes to logic networks and registers. A warning is generated when
+this command is called on a design with RTLIL processes.
+\end{lstlisting}
+
+\section{zinit -- add inverters so all FF are zero-initialized}
+\label{cmd:zinit}
+\begin{lstlisting}[numbers=left,frame=single]
+    zinit [options] [selection]
+
+Add inverters as needed to make all FFs zero-initialized.
+
+    -all
+        also add zero initialization to uninitialized FFs
 \end{lstlisting}
 
diff --git a/passes/cmds/setattr.cc b/passes/cmds/setattr.cc
index 9b05ae32..689e3148 100644
--- a/passes/cmds/setattr.cc
+++ b/passes/cmds/setattr.cc
@@ -134,15 +134,18 @@ struct SetparamPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    setparam [ -set name value | -unset name ]... [selection]\n");
+		log("    setparam [ -type cell_type ] [ -set name value | -unset name ]... [selection]\n");
 		log("\n");
 		log("Set/unset the given parameters on the selected cells. String values must be\n");
 		log("passed in double quotes (\").\n");
 		log("\n");
+		log("The -type option can be used to change the cell type of the selected cells.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
-		std::vector<setunset_t> setunset_list;
+		vector<setunset_t> setunset_list;
+		string new_cell_type;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
@@ -158,6 +161,10 @@ struct SetparamPass : public Pass {
 				setunset_list.push_back(setunset_t(args[++argidx]));
 				continue;
 			}
+			if (arg == "-type" && argidx+1 < args.size()) {
+				new_cell_type = RTLIL::escape_id(args[++argidx]);
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -170,8 +177,11 @@ struct SetparamPass : public Pass {
 				continue;
 
 			for (auto &it : module->cells_)
-				if (design->selected(module, it.second))
+				if (design->selected(module, it.second)) {
+					if (!new_cell_type.empty())
+						it.second->type = new_cell_type;
 					do_setunset(it.second->parameters, setunset_list);
+				}
 		}
 	}
 } SetparamPass;
diff --git a/passes/fsm/fsm.cc b/passes/fsm/fsm.cc
index 3b537ecd..997558b8 100644
--- a/passes/fsm/fsm.cc
+++ b/passes/fsm/fsm.cc
@@ -59,6 +59,9 @@ struct FsmPass : public Pass {
 		log("    -expand, -norecode, -export, -nomap\n");
 		log("        enable or disable passes as indicated above\n");
 		log("\n");
+		log("    -fullexpand\n");
+		log("        call expand with -full option\n");
+		log("\n");
 		log("    -encoding type\n");
 		log("    -fm_set_fsm_file file\n");
 		log("    -encfile file\n");
@@ -71,6 +74,7 @@ struct FsmPass : public Pass {
 		bool flag_norecode = false;
 		bool flag_nodetect = false;
 		bool flag_expand = false;
+		bool flag_fullexpand = false;
 		bool flag_export = false;
 		std::string fm_set_fsm_file_opt;
 		std::string encfile_opt;
@@ -110,6 +114,10 @@ struct FsmPass : public Pass {
 				flag_expand = true;
 				continue;
 			}
+			if (arg == "-fullexpand") {
+				flag_fullexpand = true;
+				continue;
+			}
 			if (arg == "-export") {
 				flag_export = true;
 				continue;
@@ -126,8 +134,8 @@ struct FsmPass : public Pass {
 		Pass::call(design, "opt_clean");
 		Pass::call(design, "fsm_opt");
 
-		if (flag_expand) {
-			Pass::call(design, "fsm_expand");
+		if (flag_expand || flag_fullexpand) {
+			Pass::call(design, flag_fullexpand ? "fsm_expand -full" : "fsm_expand");
 			Pass::call(design, "opt_clean");
 			Pass::call(design, "fsm_opt");
 		}
diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc
index 3ded3f37..e7b9dcf9 100644
--- a/passes/fsm/fsm_expand.cc
+++ b/passes/fsm/fsm_expand.cc
@@ -32,6 +32,8 @@ struct FsmExpand
 {
 	RTLIL::Module *module;
 	RTLIL::Cell *fsm_cell;
+	bool full_mode;
+
 	SigMap assign_map;
 	SigSet<RTLIL::Cell*, RTLIL::sort_by_name_id<RTLIL::Cell>> sig2driver, sig2user;
 	CellTypes ct;
@@ -45,6 +47,9 @@ struct FsmExpand
 
 	bool is_cell_merge_candidate(RTLIL::Cell *cell)
 	{
+		if (full_mode || cell->type == "$_MUX_")
+			return true;
+
 		if (cell->type == "$mux" || cell->type == "$pmux")
 			if (cell->getPort("\\A").size() < 2)
 				return true;
@@ -68,17 +73,6 @@ struct FsmExpand
 		if (new_signals.size() > 3)
 			return false;
 
-		if (cell->hasPort("\\Y")) {
-			new_signals.append(assign_map(cell->getPort("\\Y")));
-			new_signals.sort_and_unify();
-			new_signals.remove_const();
-			new_signals.remove(assign_map(fsm_cell->getPort("\\CTRL_IN")));
-			new_signals.remove(assign_map(fsm_cell->getPort("\\CTRL_OUT")));
-		}
-
-		if (new_signals.size() > 2)
-			return false;
-
 		return true;
 	}
 
@@ -200,13 +194,15 @@ struct FsmExpand
 		fsm_data.copy_to_cell(fsm_cell);
 	}
 
-	FsmExpand(RTLIL::Cell *cell, RTLIL::Design *design, RTLIL::Module *mod)
+	FsmExpand(RTLIL::Cell *cell, RTLIL::Design *design, RTLIL::Module *mod, bool full)
 	{
 		module = mod;
 		fsm_cell = cell;
+		full_mode = full;
 
 		assign_map.set(module);
 		ct.setup_internals();
+		ct.setup_stdcells();
 
 		for (auto &cell_it : module->cells_) {
 			RTLIL::Cell *c = cell_it.second;
@@ -249,17 +245,31 @@ struct FsmExpandPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    fsm_expand [selection]\n");
+		log("    fsm_expand [-full] [selection]\n");
 		log("\n");
 		log("The fsm_extract pass is conservative about the cells that belong to a finite\n");
 		log("state machine. This pass can be used to merge additional auxiliary gates into\n");
 		log("the finite state machine.\n");
 		log("\n");
+		log("By default, fsm_expand is still a bit conservative regarding merging larger\n");
+		log("word-wide cells. Call with -full to consider all cells for merging.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
+		bool full_mode = false;
+
 		log_header(design, "Executing FSM_EXPAND pass (merging auxiliary logic into FSMs).\n");
-		extra_args(args, 1, design);
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-full") {
+				full_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
 
 		for (auto &mod_it : design->modules_) {
 			if (!design->selected(mod_it.second))
@@ -269,7 +279,7 @@ struct FsmExpandPass : public Pass {
 				if (cell_it.second->type == "$fsm" && design->selected(mod_it.second, cell_it.second))
 					fsm_cells.push_back(cell_it.second);
 			for (auto c : fsm_cells) {
-				FsmExpand fsm_expand(c, design, mod_it.second);
+				FsmExpand fsm_expand(c, design, mod_it.second, full_mode);
 				fsm_expand.execute();
 			}
 		}
diff --git a/passes/fsm/fsm_map.cc b/passes/fsm/fsm_map.cc
index 5b32ed59..c4230375 100644
--- a/passes/fsm/fsm_map.cc
+++ b/passes/fsm/fsm_map.cc
@@ -272,7 +272,8 @@ static void map_fsm(RTLIL::Cell *fsm_cell, RTLIL::Module *module)
 		}
 		else
 		{
-			RTLIL::SigSpec sig_a, sig_b, sig_s;
+			RTLIL::SigSpec sig_a(RTLIL::State::Sx, next_state_wire->width);
+			RTLIL::SigSpec sig_b, sig_s;
 			int reset_state = fsm_data.reset_state;
 			if (reset_state < 0)
 				reset_state = 0;
diff --git a/passes/fsm/fsm_recode.cc b/passes/fsm/fsm_recode.cc
index 5102d833..e1bde728 100644
--- a/passes/fsm/fsm_recode.cc
+++ b/passes/fsm/fsm_recode.cc
@@ -57,13 +57,13 @@ static void fsm_recode(RTLIL::Cell *cell, RTLIL::Module *module, FILE *fm_set_fs
 
 	log("Recoding FSM `%s' from module `%s' using `%s' encoding:\n", cell->name.c_str(), module->name.c_str(), encoding.c_str());
 
-	if (encoding != "none" && encoding != "one-hot" && encoding != "binary" && encoding != "auto") {
+	if (encoding != "none" && encoding != "user" && encoding != "one-hot" && encoding != "binary" && encoding != "auto") {
 		log("  unknown encoding `%s': using auto instead.\n", encoding.c_str());
 		encoding = "auto";
 	}
 
-	if (encoding == "none") {
-		log("  nothing to do for encoding `none'.\n");
+	if (encoding == "none" || encoding == "user") {
+		log("  nothing to do for encoding `%s'.\n", encoding.c_str());
 		return;
 	}
 
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 4d1e3987..e21a7a4e 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -212,6 +212,10 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 				} else if (mod->wire(conn.first) == nullptr || mod->wire(conn.first)->port_id == 0)
 					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] != '$')
+					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));
 		}
 
 		if (cell->parameters.size() == 0)
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index 13ea5469..021c1a03 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,7 +44,7 @@ struct OptPass : public Pass {
 		log("        opt_muxtree\n");
 		log("        opt_reduce [-fine] [-full]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff\n");
+		log("        opt_rmdff [-keepdc]\n");
 		log("        opt_clean [-purge]\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("    while <changed design>\n");
@@ -54,7 +54,7 @@ struct OptPass : public Pass {
 		log("    do\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff\n");
+		log("        opt_rmdff [-keepdc]\n");
 		log("        opt_clean [-purge]\n");
 		log("    while <changed design in opt_rmdff>\n");
 		log("\n");
@@ -69,6 +69,7 @@ struct OptPass : public Pass {
 		std::string opt_expr_args;
 		std::string opt_reduce_args;
 		std::string opt_merge_args;
+		std::string opt_rmdff_args;
 		bool fast_mode = false;
 
 		log_header(design, "Executing OPT pass (performing simple optimizations).\n");
@@ -108,6 +109,7 @@ struct OptPass : public Pass {
 			}
 			if (args[argidx] == "-keepdc") {
 				opt_expr_args += " -keepdc";
+				opt_rmdff_args += " -keepdc";
 				continue;
 			}
 			if (args[argidx] == "-share_all") {
@@ -128,7 +130,7 @@ struct OptPass : public Pass {
 				Pass::call(design, "opt_expr" + opt_expr_args);
 				Pass::call(design, "opt_merge" + opt_merge_args);
 				design->scratchpad_unset("opt.did_something");
-				Pass::call(design, "opt_rmdff");
+				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
 				if (design->scratchpad_get_bool("opt.did_something") == false)
 					break;
 				Pass::call(design, "opt_clean" + opt_clean_args);
@@ -145,7 +147,7 @@ struct OptPass : public Pass {
 				Pass::call(design, "opt_muxtree");
 				Pass::call(design, "opt_reduce" + opt_reduce_args);
 				Pass::call(design, "opt_merge" + opt_merge_args);
-				Pass::call(design, "opt_rmdff");
+				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
 				Pass::call(design, "opt_clean" + opt_clean_args);
 				Pass::call(design, "opt_expr" + opt_expr_args);
 				if (design->scratchpad_get_bool("opt.did_something") == false)
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index fa954afa..922f086f 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -29,6 +29,7 @@ PRIVATE_NAMESPACE_BEGIN
 SigMap assign_map, dff_init_map;
 SigSet<RTLIL::Cell*> mux_drivers;
 dict<SigBit, pool<SigBit>> init_attributes;
+bool keepdc;
 
 void remove_init_attr(SigSpec sig)
 {
@@ -71,7 +72,11 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 	RTLIL::SigSpec sig_d, sig_q, sig_c, sig_r;
 	RTLIL::Const val_cp, val_rp, val_rv;
 
-	if (dff->type == "$_DFF_N_" || dff->type == "$_DFF_P_") {
+	if (dff->type == "$_FF_") {
+		sig_d = dff->getPort("\\D");
+		sig_q = dff->getPort("\\Q");
+	}
+	else if (dff->type == "$_DFF_N_" || dff->type == "$_DFF_P_") {
 		sig_d = dff->getPort("\\D");
 		sig_q = dff->getPort("\\Q");
 		sig_c = dff->getPort("\\C");
@@ -89,6 +94,10 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 		val_rp = RTLIL::Const(dff->type[7] == 'P', 1);
 		val_rv = RTLIL::Const(dff->type[8] == '1', 1);
 	}
+	else if (dff->type == "$ff") {
+		sig_d = dff->getPort("\\D");
+		sig_q = dff->getPort("\\Q");
+	}
 	else if (dff->type == "$dff") {
 		sig_d = dff->getPort("\\D");
 		sig_q = dff->getPort("\\Q");
@@ -115,12 +124,12 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 	bool has_init = false;
 	RTLIL::Const val_init;
 	for (auto bit : dff_init_map(sig_q).to_sigbit_vector()) {
-		if (bit.wire == NULL)
+		if (bit.wire == NULL || keepdc)
 			has_init = true;
 		val_init.bits.push_back(bit.wire == NULL ? bit.data : RTLIL::State::Sx);
 	}
 
-	if (dff->type == "$dff" && mux_drivers.has(sig_d)) {
+	if (dff->type.in("$ff", "$dff") && mux_drivers.has(sig_d)) {
 		std::set<RTLIL::Cell*> muxes;
 		mux_drivers.find(sig_d, muxes);
 		for (auto mux : muxes) {
@@ -137,7 +146,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 		}
 	}
 
-	if (sig_c.is_fully_const() && (!sig_r.size() || !has_init || val_init == val_rv)) {
+	if (!sig_c.empty() && sig_c.is_fully_const() && (!sig_r.size() || !has_init || val_init == val_rv)) {
 		if (val_rv.bits.size() == 0)
 			val_rv = val_init;
 		mod->connect(sig_q, val_rv);
@@ -182,7 +191,7 @@ struct OptRmdffPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    opt_rmdff [selection]\n");
+		log("    opt_rmdff [-keepdc] [selection]\n");
 		log("\n");
 		log("This pass identifies flip-flops with constant inputs and replaces them with\n");
 		log("a constant driver.\n");
@@ -193,7 +202,17 @@ struct OptRmdffPass : public Pass {
 		int total_count = 0, total_initdrv = 0;
 		log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n");
 
-		extra_args(args, 1, design);
+		keepdc = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-keepdc") {
+				keepdc = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
 
 		for (auto module : design->selected_modules())
 		{
@@ -243,10 +262,10 @@ struct OptRmdffPass : public Pass {
 				if (!design->selected(module, cell))
 					continue;
 
-				if (cell->type.in("$_DFF_N_", "$_DFF_P_",
+				if (cell->type.in("$_FF_", "$_DFF_N_", "$_DFF_P_",
 						"$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
 						"$_DFF_PN0_", "$_DFF_PN1_", "$_DFF_PP0_", "$_DFF_PP1_",
-						"$dff", "$adff"))
+						"$ff", "$dff", "$adff"))
 					dff_list.push_back(cell->name);
 
 				if (cell->type == "$dlatch")
diff --git a/passes/proc/proc_dff.cc b/passes/proc/proc_dff.cc
index f532990c..98653dc6 100644
--- a/passes/proc/proc_dff.cc
+++ b/passes/proc/proc_dff.cc
@@ -196,7 +196,7 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT
 	std::stringstream sstr;
 	sstr << "$procdff$" << (autoidx++);
 
-	RTLIL::Cell *cell = mod->addCell(sstr.str(), arst ? "$adff" : "$dff");
+	RTLIL::Cell *cell = mod->addCell(sstr.str(), clk.empty() ? "$ff" : arst ? "$adff" : "$dff");
 	cell->attributes = proc->attributes;
 
 	cell->parameters["\\WIDTH"] = RTLIL::Const(sig_in.size());
@@ -204,15 +204,21 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT
 		cell->parameters["\\ARST_POLARITY"] = RTLIL::Const(arst_polarity, 1);
 		cell->parameters["\\ARST_VALUE"] = val_rst;
 	}
-	cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1);
+	if (!clk.empty()) {
+		cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1);
+	}
 
 	cell->setPort("\\D", sig_in);
 	cell->setPort("\\Q", sig_out);
 	if (arst)
 		cell->setPort("\\ARST", *arst);
-	cell->setPort("\\CLK", clk);
+	if (!clk.empty())
+		cell->setPort("\\CLK", clk);
 
-	log("  created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
+	if (!clk.empty())
+		log("  created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
+	else
+		log("  created %s cell `%s' with global clock", cell->type.c_str(), cell->name.c_str());
 	if (arst)
 		log(" and %s level reset", arst_polarity ? "positive" : "negative");
 	log(".\n");
@@ -236,6 +242,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 		RTLIL::SyncRule *sync_level = NULL;
 		RTLIL::SyncRule *sync_edge = NULL;
 		RTLIL::SyncRule *sync_always = NULL;
+		bool global_clock = false;
 
 		std::map<RTLIL::SigSpec, std::set<RTLIL::SyncRule*>> many_async_rules;
 
@@ -267,6 +274,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 				sig.replace(action.first, action.second, &insig);
 				sync_always = sync;
 			}
+			else if (sync->type == RTLIL::SyncType::STg) {
+				sig.replace(action.first, action.second, &insig);
+				global_clock = true;
+			}
 			else {
 				log_error("Event with any-edge sensitivity found for this signal!\n");
 			}
@@ -328,7 +339,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 			continue;
 		}
 
-		if (!sync_edge)
+		if (!sync_edge && !global_clock)
 			log_error("Missing edge-sensitive event for this signal!\n");
 
 		if (many_async_rules.size() > 0)
@@ -346,9 +357,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 		}
 		else
 			gen_dff(mod, insig, rstval.as_const(), sig,
-					sync_edge->type == RTLIL::SyncType::STp,
+					sync_edge && sync_edge->type == RTLIL::SyncType::STp,
 					sync_level && sync_level->type == RTLIL::SyncType::ST1,
-					sync_edge->signal, sync_level ? &sync_level->signal : NULL, proc);
+					sync_edge ? sync_edge->signal : SigSpec(),
+					sync_level ? &sync_level->signal : NULL, proc);
 
 		if (free_sync_level)
 			delete sync_level;
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index 0c5f6fc6..6785b750 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -5,4 +5,5 @@ OBJS += passes/sat/eval.o
 OBJS += passes/sat/miter.o
 OBJS += passes/sat/expose.o
 OBJS += passes/sat/assertpmux.o
+OBJS += passes/sat/clk2fflogic.o
 
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
new file mode 100644
index 00000000..ef6d5dd7
--- /dev/null
+++ b/passes/sat/clk2fflogic.cc
@@ -0,0 +1,226 @@
+/*
+ *  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
+
+struct Clk2fflogicPass : public Pass {
+	Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    clk2fflogic [options] [selection]\n");
+		log("\n");
+		log("This command replaces clocked flip-flops with generic $ff cells that use the\n");
+		log("implicit global clock. This is useful for formal verification of designs with\n");
+		log("multiple clocks.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		// bool flag_noinit = false;
+
+		log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			// if (args[argidx] == "-noinit") {
+			// 	flag_noinit = true;
+			// 	continue;
+			// }
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		for (auto module : design->selected_modules())
+		{
+			SigMap sigmap(module);
+			dict<SigBit, State> initbits;
+			pool<SigBit> del_initbits;
+
+			for (auto wire : module->wires())
+				if (wire->attributes.count("\\init") > 0)
+				{
+					Const initval = wire->attributes.at("\\init");
+					SigSpec initsig = sigmap(wire);
+
+					for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
+						if (initval[i] == State::S0 || initval[i] == State::S1)
+							initbits[initsig[i]] = initval[i];
+				}
+
+			for (auto cell : vector<Cell*>(module->selected_cells()))
+			{
+				if (cell->type.in("$dlatch"))
+				{
+					bool enpol = cell->parameters["\\EN_POLARITY"].as_bool();
+
+					SigSpec sig_en = cell->getPort("\\EN");
+					SigSpec sig_d = cell->getPort("\\D");
+					SigSpec sig_q = cell->getPort("\\Q");
+
+					log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(sig_en), log_signal(sig_d), log_signal(sig_q));
+
+					Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
+					module->addFf(NEW_ID, sig_q, past_q);
+
+					if (enpol)
+						module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q);
+					else
+						module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q);
+
+					Const initval;
+					bool assign_initval = false;
+					for (int i = 0; i < GetSize(sig_d); i++) {
+						SigBit qbit = sigmap(sig_q[i]);
+						if (initbits.count(qbit)) {
+							initval.bits.push_back(initbits.at(qbit));
+							del_initbits.insert(qbit);
+						} else
+							initval.bits.push_back(State::Sx);
+						if (initval.bits.back() != State::Sx)
+							assign_initval = true;
+					}
+
+					if (assign_initval)
+						past_q->attributes["\\init"] = initval;
+
+					module->remove(cell);
+					continue;
+				}
+
+				if (cell->type.in("$dff", "$adff", "$dffsr"))
+				{
+					bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool();
+
+					SigSpec clk = cell->getPort("\\CLK");
+					Wire *past_clk = module->addWire(NEW_ID);
+					past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0;
+					module->addFf(NEW_ID, clk, past_clk);
+
+					SigSpec sig_d = cell->getPort("\\D");
+					SigSpec sig_q = cell->getPort("\\Q");
+
+					log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(clk), log_signal(sig_d), log_signal(sig_q));
+
+					SigSpec clock_edge_pattern;
+
+					if (clkpol) {
+						clock_edge_pattern.append_bit(State::S0);
+						clock_edge_pattern.append_bit(State::S1);
+					} else {
+						clock_edge_pattern.append_bit(State::S1);
+						clock_edge_pattern.append_bit(State::S0);
+					}
+
+					SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern);
+
+					Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d));
+					Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
+					module->addFf(NEW_ID, sig_d, past_d);
+					module->addFf(NEW_ID, sig_q, past_q);
+
+					if (cell->type == "$adff")
+					{
+						SigSpec arst = cell->getPort("\\ARST");
+						SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
+						Const rstval = cell->parameters["\\ARST_VALUE"];
+
+						if (cell->parameters["\\ARST_POLARITY"].as_bool())
+							module->addMux(NEW_ID, qval, rstval, arst, sig_q);
+						else
+							module->addMux(NEW_ID, rstval, qval, arst, sig_q);
+					}
+					else
+					if (cell->type == "$dffsr")
+					{
+						SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
+						SigSpec setval = cell->getPort("\\SET");
+						SigSpec clrval = cell->getPort("\\CLR");
+
+						if (!cell->parameters["\\SET_POLARITY"].as_bool())
+							setval = module->Not(NEW_ID, setval);
+
+						if (cell->parameters["\\CLR_POLARITY"].as_bool())
+							clrval = module->Not(NEW_ID, clrval);
+
+						qval = module->Or(NEW_ID, qval, setval);
+						module->addAnd(NEW_ID, qval, clrval, sig_q);
+					}
+					else
+					{
+						module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q);
+					}
+
+					Const initval;
+					bool assign_initval = false;
+					for (int i = 0; i < GetSize(sig_d); i++) {
+						SigBit qbit = sigmap(sig_q[i]);
+						if (initbits.count(qbit)) {
+							initval.bits.push_back(initbits.at(qbit));
+							del_initbits.insert(qbit);
+						} else
+							initval.bits.push_back(State::Sx);
+						if (initval.bits.back() != State::Sx)
+							assign_initval = true;
+					}
+
+					if (assign_initval) {
+						past_d->attributes["\\init"] = initval;
+						past_q->attributes["\\init"] = initval;
+					}
+
+					module->remove(cell);
+					continue;
+				}
+			}
+
+			for (auto wire : module->wires())
+				if (wire->attributes.count("\\init") > 0)
+				{
+					bool delete_initattr = true;
+					Const initval = wire->attributes.at("\\init");
+					SigSpec initsig = sigmap(wire);
+
+					for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
+						if (del_initbits.count(initsig[i]) > 0)
+							initval[i] = State::Sx;
+						else if (initval[i] != State::Sx)
+							delete_initattr = false;
+
+					if (delete_initattr)
+						wire->attributes.erase("\\init");
+					else
+						wire->attributes.at("\\init") = initval;
+				}
+		}
+
+	}
+} Clk2fflogicPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 4854e19b..9e150b60 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -312,18 +312,42 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
 		log_pop();
 	}
 
-	SigSpec or_signals;
+	SigSpec assert_signals, assume_signals;
 	vector<Cell*> cell_list = module->cells();
-	for (auto cell : cell_list) {
+	for (auto cell : cell_list)
+	{
+		if (!cell->type.in("$assert", "$assume"))
+			continue;
+
+		SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
+		SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
+
 		if (cell->type == "$assert") {
-			SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
-			SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
-			or_signals.append(module->And(NEW_ID, is_active, is_enabled));
-			module->remove(cell);
+			assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
+		} else {
+			assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
 		}
+
+		module->remove(cell);
 	}
 
-	module->addReduceOr(NEW_ID, or_signals, trigger);
+	if (assume_signals.empty())
+	{
+		module->addReduceOr(NEW_ID, assert_signals, trigger);
+	}
+	else
+	{
+		Wire *assume_q = module->addWire(NEW_ID);
+		assume_q->attributes["\\init"] = State::S0;
+		assume_signals.append(assume_q);
+
+		SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
+		SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
+		module->addFf(NEW_ID, assume_nok, assume_q);
+
+		SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
+		module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
+	}
 
 	if (flag_flatten) {
 		log_push();
diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc
index b5024fa9..311a1af9 100644
--- a/passes/techmap/Makefile.inc
+++ b/passes/techmap/Makefile.inc
@@ -31,6 +31,7 @@ OBJS += passes/techmap/deminout.o
 OBJS += passes/techmap/insbuf.o
 OBJS += passes/techmap/attrmvcp.o
 OBJS += passes/techmap/attrmap.o
+OBJS += passes/techmap/zinit.o
 endif
 
 GENFILES += passes/techmap/techmap.inc
diff --git a/passes/techmap/attrmap.cc b/passes/techmap/attrmap.cc
index f715b63e..dec81d21 100644
--- a/passes/techmap/attrmap.cc
+++ b/passes/techmap/attrmap.cc
@@ -33,13 +33,32 @@ Const make_value(string &value)
 	return sig.as_const();
 }
 
+bool string_compare_nocase(const string &str1, const string &str2)
+{
+	if (str1.size() != str2.size())
+		return false;
+
+	for (size_t i = 0; i < str1.size(); i++)
+	{
+		char ch1 = str1[i], ch2 = str2[i];
+		if ('a' <= ch1 && ch1 <= 'z')
+			ch1 -= 'a' - 'A';
+		if ('a' <= ch2 && ch2 <= 'z')
+			ch2 -= 'a' - 'A';
+		if (ch1 != ch2)
+			return false;
+	}
+
+	return true;
+}
+
 bool match_name(string &name, IdString &id, bool ignore_case=false)
 {
 	string str1 = RTLIL::escape_id(name);
 	string str2 = id.str();
 
 	if (ignore_case)
-		return !strcasecmp(str1.c_str(), str2.c_str());
+		return string_compare_nocase(str1, str2);
 
 	return str1 == str2;
 }
@@ -49,7 +68,7 @@ bool match_value(string &value, Const &val, bool ignore_case=false)
 	if (ignore_case && ((val.flags & RTLIL::CONST_FLAG_STRING) != 0) && GetSize(value) && value.front() == '"' && value.back() == '"') {
 		string str1 = value.substr(1, GetSize(value)-2);
 		string str2 = val.decode_string();
-		return !strcasecmp(str1.c_str(), str2.c_str());
+		return string_compare_nocase(str1, str2);
 	}
 
 	return make_value(value) == val;
diff --git a/passes/techmap/attrmvcp.cc b/passes/techmap/attrmvcp.cc
index 50eaf61d..1537def0 100644
--- a/passes/techmap/attrmvcp.cc
+++ b/passes/techmap/attrmvcp.cc
@@ -93,6 +93,7 @@ struct AttrmvcpPass : public Pass {
 
 			for (auto cell : module->selected_cells())
 			for (auto &conn : cell->connections())
+			{
 				if (driven_mode) {
 					if (cell->input(conn.first))
 						for (auto bit : sigmap(conn.second))
@@ -102,6 +103,7 @@ struct AttrmvcpPass : public Pass {
 						for (auto bit : sigmap(conn.second))
 							net2cells[bit].insert(cell);
 				}
+			}
 
 			for (auto wire : module->selected_wires())
 			{
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index 0fb64734..c6b932bd 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -388,6 +388,23 @@ void simplemap_sr(RTLIL::Module *module, RTLIL::Cell *cell)
 	}
 }
 
+void simplemap_ff(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+	int width = cell->parameters.at("\\WIDTH").as_int();
+
+	RTLIL::SigSpec sig_d = cell->getPort("\\D");
+	RTLIL::SigSpec sig_q = cell->getPort("\\Q");
+
+	std::string gate_type = "$_FF_";
+
+	for (int i = 0; i < width; i++) {
+		RTLIL::Cell *gate = module->addCell(NEW_ID, gate_type);
+		gate->add_strpool_attribute("\\src", cell->get_strpool_attribute("\\src"));
+		gate->setPort("\\D", sig_d[i]);
+		gate->setPort("\\Q", sig_q[i]);
+	}
+}
+
 void simplemap_dff(RTLIL::Module *module, RTLIL::Cell *cell)
 {
 	int width = cell->parameters.at("\\WIDTH").as_int();
@@ -532,6 +549,7 @@ void simplemap_get_mappers(std::map<RTLIL::IdString, void(*)(RTLIL::Module*, RTL
 	mappers["$slice"]       = simplemap_slice;
 	mappers["$concat"]      = simplemap_concat;
 	mappers["$sr"]          = simplemap_sr;
+	mappers["$ff"]          = simplemap_ff;
 	mappers["$dff"]         = simplemap_dff;
 	mappers["$dffe"]        = simplemap_dffe;
 	mappers["$dffsr"]       = simplemap_dffsr;
@@ -569,7 +587,7 @@ struct SimplemapPass : public Pass {
 		log("  $not, $pos, $and, $or, $xor, $xnor\n");
 		log("  $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n");
 		log("  $logic_not, $logic_and, $logic_or, $mux, $tribuf\n");
-		log("  $sr, $dff, $dffsr, $adff, $dlatch\n");
+		log("  $sr, $ff, $dff, $dffsr, $adff, $dlatch\n");
 		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc
index b2cc492b..6784f48c 100644
--- a/passes/techmap/techmap.cc
+++ b/passes/techmap/techmap.cc
@@ -345,6 +345,12 @@ struct TechmapWorker
 				c->setParam("\\MEMID", Const(memory_renames[memid].str()));
 			}
 
+			if (c->type == "$mem") {
+				string memid = c->getParam("\\MEMID").decode_string();
+				apply_prefix(cell->name.str(), memid);
+				c->setParam("\\MEMID", Const(memid));
+			}
+
 			if (c->attributes.count("\\src"))
 				c->add_strpool_attribute("\\src", extra_src_attrs);
 		}
@@ -1164,8 +1170,9 @@ struct FlattenPass : public Pass {
 				worker.flatten_do_list.erase(mod->name);
 			}
 		} else {
-			for (auto mod : vector<Module*>(design->modules()))
+			for (auto mod : vector<Module*>(design->modules())) {
 				while (worker.techmap_module(design, mod, design, handled_cells, celltypeMap, false)) { }
+			}
 		}
 
 		log("No more expansions possible.\n");
diff --git a/passes/techmap/zinit.cc b/passes/techmap/zinit.cc
new file mode 100644
index 00000000..a577e123
--- /dev/null
+++ b/passes/techmap/zinit.cc
@@ -0,0 +1,151 @@
+/*
+ *  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
+
+struct ZinitPass : public Pass {
+	ZinitPass() : Pass("zinit", "add inverters so all FF are zero-initialized") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    zinit [options] [selection]\n");
+		log("\n");
+		log("Add inverters as needed to make all FFs zero-initialized.\n");
+		log("\n");
+		log("    -all\n");
+		log("        also add zero initialization to uninitialized FFs\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		bool all_mode = false;
+
+		log_header(design, "Executing ZINIT pass (make all FFs zero-initialized).\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-singleton") {
+				all_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		for (auto module : design->selected_modules())
+		{
+			SigMap sigmap(module);
+			dict<SigBit, State> initbits;
+			pool<SigBit> donebits;
+
+			for (auto wire : module->selected_wires())
+			{
+				if (wire->attributes.count("\\init") == 0)
+					continue;
+
+				SigSpec wirebits = sigmap(wire);
+				Const initval = wire->attributes.at("\\init");
+				wire->attributes.erase("\\init");
+
+				for (int i = 0; i < GetSize(wirebits) && i < GetSize(initval); i++)
+				{
+					SigBit bit = wirebits[i];
+					State val = initval[i];
+
+					if (val != State::S0 && val != State::S1 && bit.wire != nullptr)
+						continue;
+
+					if (initbits.count(bit)) {
+						if (initbits.at(bit) != val)
+							log_error("Conflicting init values for signal %s (%s = %s != %s).\n",
+									log_signal(bit), log_signal(SigBit(wire, i)),
+									log_signal(val), log_signal(initbits.at(bit)));
+						continue;
+					}
+
+					initbits[bit] = val;
+				}
+			}
+
+			pool<IdString> dff_types = {
+				"$ff", "$dff", "$dffe", "$dffsr", "$adff",
+				"$_FF_", "$_DFFE_NN_", "$_DFFE_NP_", "$_DFFE_PN_", "$_DFFE_PP_",
+				"$_DFFSR_NNN_", "$_DFFSR_NNP_", "$_DFFSR_NPN_", "$_DFFSR_NPP_",
+				"$_DFFSR_PNN_", "$_DFFSR_PNP_", "$_DFFSR_PPN_", "$_DFFSR_PPP_",
+				"$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
+				"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1_", "$_DFF_PP0_", "$_DFF_PP1_"
+			};
+
+			for (auto cell : module->selected_cells())
+			{
+				if (!dff_types.count(cell->type))
+					continue;
+
+				SigSpec sig_d = sigmap(cell->getPort("\\D"));
+				SigSpec sig_q = sigmap(cell->getPort("\\Q"));
+
+				if (GetSize(sig_d) < 1 || GetSize(sig_q) < 1)
+					continue;
+
+				Const initval;
+
+				for (int i = 0; i < GetSize(sig_q); i++) {
+					if (initbits.count(sig_q[i])) {
+						initval.bits.push_back(initbits.at(sig_q[i]));
+						donebits.insert(sig_q[i]);
+					} else
+						initval.bits.push_back(all_mode ? State::S0 : State::Sx);
+				}
+
+				Wire *initwire = module->addWire(NEW_ID, GetSize(initval));
+				initwire->attributes["\\init"] = initval;
+
+				for (int i = 0; i < GetSize(initwire); i++)
+					if (initval.bits.at(i) == State::S1)
+					{
+						sig_d[i] = module->NotGate(NEW_ID, sig_d[i]);
+						module->addNotGate(NEW_ID, SigSpec(initwire, i), sig_q[i]);
+						initwire->attributes["\\init"].bits.at(i) = State::S0;
+					}
+					else
+					{
+						module->connect(sig_q[i], SigSpec(initwire, i));
+					}
+
+				log("FF init value for cell %s (%s): %s = %s\n", log_id(cell), log_id(cell->type),
+						log_signal(sig_q), log_signal(initval));
+
+				cell->setPort("\\D", sig_d);
+				cell->setPort("\\Q", initwire);
+			}
+
+			for (auto &it : initbits)
+				if (donebits.count(it.first) == 0)
+					log_error("Failed to handle init bit %s = %s.\n", log_signal(it.first), log_signal(it.second));
+		}
+	}
+} ZinitPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/techlibs/common/prep.cc b/techlibs/common/prep.cc
index fac6c4ba..71534983 100644
--- a/techlibs/common/prep.cc
+++ b/techlibs/common/prep.cc
@@ -63,6 +63,9 @@ struct PrepPass : public ScriptPass
 		log("    -nordff\n");
 		log("        passed to 'memory_dff'. prohibits merging of FFs into memory read ports\n");
 		log("\n");
+		log("     -nokeepdc\n");
+		log("        do not call opt_* with -keepdc\n");
+		log("\n");
 		log("    -run <from_label>[:<to_label>]\n");
 		log("        only run the commands between the labels (see below). an empty\n");
 		log("        from label is synonymous to 'begin', and empty to label is\n");
@@ -75,7 +78,7 @@ struct PrepPass : public ScriptPass
 	}
 
 	string top_module, fsm_opts, memory_opts;
-	bool autotop, flatten, ifxmode, memxmode, nomemmode;
+	bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc;
 
 	virtual void clear_flags() YS_OVERRIDE
 	{
@@ -87,6 +90,7 @@ struct PrepPass : public ScriptPass
 		ifxmode = false;
 		memxmode = false;
 		nomemmode = false;
+		nokeepdc = false;
 	}
 
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -136,6 +140,10 @@ struct PrepPass : public ScriptPass
 				memory_opts += " -nordff";
 				continue;
 			}
+			if (args[argidx] == "-nokeepdc") {
+				nokeepdc = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -177,10 +185,10 @@ struct PrepPass : public ScriptPass
 				run(ifxmode ? "proc -ifx" : "proc");
 			if (help_mode || flatten)
 				run("flatten", "(if -flatten)");
-			run("opt_expr -keepdc");
+			run(nokeepdc ? "opt_expr" : "opt_expr -keepdc");
 			run("opt_clean");
 			run("check");
-			run("opt -keepdc");
+			run(nokeepdc ? "opt" : "opt -keepdc");
 			if (!ifxmode) {
 				if (help_mode)
 					run("wreduce [-memx]");
@@ -194,7 +202,7 @@ struct PrepPass : public ScriptPass
 				run("opt_clean");
 				run("memory_collect");
 			}
-			run("opt -keepdc -fast");
+			run(nokeepdc ? "opt -fast" : "opt -keepdc -fast");
 		}
 
 		if (check_label("check"))
diff --git a/techlibs/common/simcells.v b/techlibs/common/simcells.v
index c4f170a3..e770c545 100644
--- a/techlibs/common/simcells.v
+++ b/techlibs/common/simcells.v
@@ -495,6 +495,23 @@ always @(posedge S, posedge R) begin
 end
 endmodule
 
+`ifdef SIMCELLS_FF
+//  |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+//-
+//-     $_FF_ (D, Q)
+//-
+//- A D-type flip-flop that is clocked from the implicit global clock. (This cell
+//- type is usually only used in netlists for formal verification.)
+//-
+module \$_FF_ (D, Q);
+input D;
+output reg Q;
+always @($global_clock) begin
+	Q <= D;
+end
+endmodule
+`endif
+
 //  |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 //-
 //-     $_DFF_N_ (D, C, Q)
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index 922a47ca..2c4db1ac 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1334,6 +1334,18 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$anyseq (Y);
+
+parameter WIDTH = 0;
+
+output [WIDTH-1:0] Y;
+
+assign Y = 'bx;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$equiv (A, B, Y);
 
 input A, B;
@@ -1382,6 +1394,23 @@ endmodule
 
 `endif
 // --------------------------------------------------------
+`ifdef SIMLIB_FF
+
+module \$ff (D, Q);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] D;
+output reg [WIDTH-1:0] Q;
+
+always @($global_clk) begin
+	Q <= D;
+end
+
+endmodule
+
+`endif
+// --------------------------------------------------------
 
 module \$dff (CLK, D, Q);
 
diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v
index 90c4ed7e..d7ec3947 100644
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -64,7 +64,7 @@ module _90_simplemap_various;
 endmodule
 
 (* techmap_simplemap *)
-(* techmap_celltype = "$sr $dff $dffe $adff $dffsr $dlatch" *)
+(* techmap_celltype = "$sr $ff $dff $dffe $adff $dffsr $dlatch" *)
 module _90_simplemap_registers;
 endmodule
 
diff --git a/techlibs/gowin/Makefile.inc b/techlibs/gowin/Makefile.inc
new file mode 100644
index 00000000..679d7eff
--- /dev/null
+++ b/techlibs/gowin/Makefile.inc
@@ -0,0 +1,6 @@
+
+OBJS += techlibs/gowin/synth_gowin.o
+
+$(eval $(call add_share_file,share/gowin,techlibs/gowin/cells_map.v))
+$(eval $(call add_share_file,share/gowin,techlibs/gowin/cells_sim.v))
+
diff --git a/techlibs/gowin/cells_map.v b/techlibs/gowin/cells_map.v
new file mode 100644
index 00000000..e1f85eff
--- /dev/null
+++ b/techlibs/gowin/cells_map.v
@@ -0,0 +1,31 @@
+module  \$_DFF_N_ (input D, C, output Q); DFFN _TECHMAP_REPLACE_ (.D(D), .Q(Q), .CLK(C)); endmodule
+module  \$_DFF_P_ (input D, C, output Q); DFF  _TECHMAP_REPLACE_ (.D(D), .Q(Q), .CLK(C)); endmodule
+
+module \$lut (A, Y);
+  parameter WIDTH = 0;
+  parameter LUT = 0;
+
+  input [WIDTH-1:0] A;
+  output Y;
+
+  generate
+    if (WIDTH == 1) begin
+      LUT1 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y),
+        .I0(A[0]));
+    end else
+    if (WIDTH == 2) begin
+      LUT2 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y),
+        .I0(A[0]), .I1(A[1]));
+    end else
+    if (WIDTH == 3) begin
+      LUT3 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y),
+        .I0(A[0]), .I1(A[1]), .I2(A[2]));
+    end else
+    if (WIDTH == 4) begin
+      LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.F(Y),
+        .I0(A[0]), .I1(A[1]), .I2(A[2]), .I3(A[3]));
+    end else begin
+      wire _TECHMAP_FAIL_ = 1;
+    end
+  endgenerate
+endmodule
diff --git a/techlibs/gowin/cells_sim.v b/techlibs/gowin/cells_sim.v
new file mode 100644
index 00000000..3a09c157
--- /dev/null
+++ b/techlibs/gowin/cells_sim.v
@@ -0,0 +1,51 @@
+module LUT1(output F, input I0);
+  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];
+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];
+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];
+endmodule
+
+module DFF (output reg Q, input CLK, D);
+	always @(posedge C)
+		Q <= D;
+endmodule
+
+module DFFN (output reg Q, input CLK, D);
+	always @(negedge C)
+		Q <= D;
+endmodule
+
+module VCC(output V);
+  assign V = 1;
+endmodule
+
+module GND(output G);
+  assign G = 0;
+endmodule
+
+module IBUF(output O, input I);
+  assign O = I;
+endmodule
+
+module OBUF(output O, input I);
+  assign O = I;
+endmodule
diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc
new file mode 100644
index 00000000..129ab839
--- /dev/null
+++ b/techlibs/gowin/synth_gowin.cc
@@ -0,0 +1,178 @@
+/*
+ *  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/register.h"
+#include "kernel/celltypes.h"
+#include "kernel/rtlil.h"
+#include "kernel/log.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct SynthGowinPass : public ScriptPass
+{
+	SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { }
+
+	virtual void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    synth_gowin [options]\n");
+		log("\n");
+		log("This command runs synthesis for Gowin FPGAs. This work is experimental.\n");
+		log("\n");
+		log("    -top <module>\n");
+		log("        use the specified module as top module (default='top')\n");
+		log("\n");
+		log("    -vout <file>\n");
+		log("        write the design to the specified Verilog netlist file. writing of an\n");
+		log("        output file is omitted if this parameter is not specified.\n");
+		log("\n");
+		log("    -run <from_label>:<to_label>\n");
+		log("        only run the commands between the labels (see below). an empty\n");
+		log("        from label is synonymous to 'begin', and empty to label is\n");
+		log("        synonymous to the end of the command list.\n");
+		log("\n");
+		log("    -retime\n");
+		log("        run 'abc' with -dff option\n");
+		log("\n");
+		log("\n");
+		log("The following commands are executed by this synthesis command:\n");
+		help_script();
+		log("\n");
+	}
+
+	string top_opt, vout_file;
+	bool retime;
+
+	virtual void clear_flags() YS_OVERRIDE
+	{
+		top_opt = "-auto-top";
+		vout_file = "";
+		retime = false;
+	}
+
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		string run_from, run_to;
+		clear_flags();
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-top" && argidx+1 < args.size()) {
+				top_opt = "-top " + args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-vout" && argidx+1 < args.size()) {
+				vout_file = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-run" && argidx+1 < args.size()) {
+				size_t pos = args[argidx+1].find(':');
+				if (pos == std::string::npos)
+					break;
+				run_from = args[++argidx].substr(0, pos);
+				run_to = args[argidx].substr(pos+1);
+				continue;
+			}
+			if (args[argidx] == "-retime") {
+				retime = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		if (!design->full_selection())
+			log_cmd_error("This comannd only operates on fully selected designs!\n");
+
+		log_header(design, "Executing SYNTH_GOWIN pass.\n");
+		log_push();
+
+		run_script(design, run_from, run_to);
+
+		log_pop();
+	}
+
+	virtual void script() YS_OVERRIDE
+	{
+		if (check_label("begin"))
+		{
+			run("read_verilog -lib +/gowin/cells_sim.v");
+			run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
+		}
+
+		if (check_label("flatten"))
+		{
+			run("proc");
+			run("flatten");
+			run("tribuf -logic");
+			run("deminout");
+		}
+
+		if (check_label("coarse"))
+		{
+			run("synth -run coarse");
+		}
+
+		if (check_label("fine"))
+		{
+			run("opt -fast -mux_undef -undriven -fine");
+			run("memory_map");
+			run("opt -undriven -fine");
+			run("techmap");
+			run("clean -purge");
+			run("splitnets -ports");
+			run("setundef -undriven -zero");
+			if (retime || help_mode)
+				run("abc -dff", "(only if -retime)");
+		}
+
+		if (check_label("map_luts"))
+		{
+			run("abc -lut 4");
+			run("clean");
+		}
+
+		if (check_label("map_cells"))
+		{
+			run("techmap -map +/gowin/cells_map.v");
+			run("hilomap -hicell VCC V -locell GND G");
+			run("iopadmap -inpad IBUF O:I -outpad OBUF I:O");
+			run("clean -purge");
+		}
+
+		if (check_label("check"))
+		{
+			run("hierarchy -check");
+			run("stat");
+			run("check -noinit");
+		}
+
+		if (check_label("vout"))
+		{
+			if (!vout_file.empty() || help_mode)
+				run(stringf("write_verilog -attr2comment -defparam -renameprefix gen %s",
+						help_mode ? "<file-name>" : vout_file.c_str()));
+		}
+	}
+} SynthGowinPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/techlibs/greenpak4/cells_sim.v b/techlibs/greenpak4/cells_sim.v
index 6ae9ae79..80746be0 100644
--- a/techlibs/greenpak4/cells_sim.v
+++ b/techlibs/greenpak4/cells_sim.v
@@ -131,9 +131,8 @@ endmodule
 module GP_DELAY(input IN, output reg OUT);
 	
 	parameter DELAY_STEPS = 1;
-	
-	//TODO: additional delay/glitch filter mode
-	
+	parameter GLITCH_FILTER = 0;
+		
 	initial OUT = 0;
 	
 	generate
@@ -241,6 +240,16 @@ module GP_DFFSRI(input D, CLK, nSR, output reg nQ);
 	end
 endmodule
 
+module GP_EDGEDET(input IN, output reg OUT);
+
+	parameter EDGE_DIRECTION = "RISING";
+	parameter DELAY_STEPS = 1;
+	parameter GLITCH_FILTER = 0;
+	
+	//not implemented for simulation
+	
+endmodule
+
 module GP_IBUF(input IN, output OUT);
 	assign OUT = IN;
 endmodule
@@ -296,6 +305,27 @@ module GP_PGA(input wire VIN_P, input wire VIN_N, input wire VIN_SEL, output reg
 
 endmodule
 
+module GP_PGEN(input wire nRST, input wire CLK, output reg OUT);
+	initial OUT = 0;
+	parameter PATTERN_DATA = 16'h0;
+	parameter PATTERN_LEN = 5'd16;
+
+	reg[3:0] count = 0;
+	always @(posedge CLK) begin
+		if(!nRST)
+			OUT <= PATTERN_DATA[0];
+
+		else begin
+			count <= count + 1;
+			OUT <= PATTERN_DATA[count];
+
+			if( (count + 1) == PATTERN_LEN)
+				count <= 0;			
+		end
+	end
+	
+endmodule
+
 module GP_POR(output reg RST_DONE);
 	parameter POR_TIME = 500;
 	
@@ -409,7 +439,8 @@ endmodule
 //keep constraint needed to prevent optimization since we have no outputs
 (* keep *)
 module GP_SYSRESET(input RST);
-	parameter RESET_MODE = "RISING";
+	parameter RESET_MODE = "EDGE";
+	parameter EDGE_SPEED = 4;
 	
 	//cannot simulate whole system reset
 	
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 38a9cf9d..2533d3af 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -35,7 +35,7 @@ struct SynthIce40Pass : public ScriptPass
 		log("\n");
 		log("    synth_ice40 [options]\n");
 		log("\n");
-		log("This command runs synthesis for iCE40 FPGAs. This work is experimental.\n");
+		log("This command runs synthesis for iCE40 FPGAs.\n");
 		log("\n");
 		log("    -top <module>\n");
 		log("        use the specified module as top module (default='top')\n");
diff --git a/tests/asicworld/run-test.sh b/tests/asicworld/run-test.sh
index 24983f1a..d5708c45 100755
--- a/tests/asicworld/run-test.sh
+++ b/tests/asicworld/run-test.sh
@@ -1,2 +1,14 @@
 #!/bin/bash
-exec ${MAKE:-make} -f ../tools/autotest.mk EXTRA_FLAGS="-e" *.v
+
+OPTIND=1
+seed=""    # default to no seed specified
+while getopts "S:" opt
+do
+    case "$opt" in
+	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+	   seed="SEED=$arg" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed EXTRA_FLAGS="-e" *.v
diff --git a/tests/bram/generate.py b/tests/bram/generate.py
index 05a7ed02..def0b23c 100644
--- a/tests/bram/generate.py
+++ b/tests/bram/generate.py
@@ -1,11 +1,11 @@
 #!/usr/bin/env python3
 
+import argparse
 import os
 import sys
 import random
 
 debug_mode = False
-seed = (int(os.times()[4]*100) + os.getpid()) % 900000 + 100000
 
 def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
     while True:
@@ -25,12 +25,15 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
             if wrmode.count(0) == 0: continue
             break
 
-        if random.randrange(2) or True:
+        if random.randrange(2):
             maxpol = 4
             maxtransp = 1
+            maxclocks = 4
         else:
-            maxpol = 2
+            maxpol = None
+            clkpol = random.randrange(4)
             maxtransp = 2
+            maxclocks = 1
 
         def generate_enable(i):
             if wrmode[i]:
@@ -45,11 +48,16 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
                 return random.randrange(maxtransp)
             return 0
 
-        ports  = [ random.randrange(1, 3)   for i in range(groups) ]
-        enable = [ generate_enable(i)       for i in range(groups) ]
-        transp = [ generate_transp(i)       for i in range(groups) ]
-        clocks = [ random.randrange(1, 4)   for i in range(groups) ]
-        clkpol = [ random.randrange(maxpol) for i in range(groups) ]
+        def generate_clkpol(i):
+            if maxpol is None:
+                return clkpol
+            return random.randrange(maxpol)
+
+        ports  = [ random.randrange(1, 3)           for i in range(groups) ]
+        enable = [ generate_enable(i)               for i in range(groups) ]
+        transp = [ generate_transp(i)               for i in range(groups) ]
+        clocks = [ random.randrange(maxclocks)+1    for i in range(groups) ]
+        clkpol = [ generate_clkpol(i)               for i in range(groups) ]
         break
 
     print("bram bram_%02d_%02d" % (k1, k2), file=dsc_f)
@@ -109,11 +117,13 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
             if clocks[p1] and not ("CLK%d" % clocks[p1]) in v_ports:
                 v_ports.add("CLK%d" % clocks[p1])
                 v_stmts.append("input CLK%d;" % clocks[p1])
-                tb_decls.append("reg CLK%d;" % clocks[p1])
+                tb_decls.append("reg CLK%d = 0;" % clocks[p1])
                 tb_clocks.append("CLK%d" % clocks[p1])
 
             v_ports.add("%sADDR" % pf)
             v_stmts.append("input [%d:0] %sADDR;" % (abits-1, pf))
+            if transp[p1]:
+                v_stmts.append("reg [%d:0] %sADDR_Q;" % (abits-1, pf))
             tb_decls.append("reg [%d:0] %sADDR;" % (abits-1, pf))
             tb_addr.append("%sADDR" % pf)
 
@@ -159,8 +169,11 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
                 for i in range(enable[p1]):
                     enrange = "[%d:%d]" % ((i+1)*dbits/enable[p1]-1, i*dbits/enable[p1])
                     v_always[last_always_hdr].append((portindex, pf, "if (%sEN[%d]) memory[%sADDR]%s = %sDATA%s;" % (pf, i, pf, enrange, pf, enrange)))
+            elif transp[p1]:
+                v_always[last_always_hdr].append((sum(ports)+1, pf, "%sADDR_Q %s %sADDR;" % (pf, assign_op, pf)))
+                v_stmts.append("always @* %sDATA = memory[%sADDR_Q];" % (pf, pf))
             else:
-                v_always[last_always_hdr].append((sum(ports)+1 if transp[p1] else 0, pf, "%sDATA %s memory[%sADDR];" % (pf, assign_op, pf)))
+                v_always[last_always_hdr].append((0, pf, "%sDATA %s memory[%sADDR];" % (pf, assign_op, pf)))
 
     for always_hdr in sorted(v_always):
         v_stmts.append(always_hdr[1])
@@ -243,10 +256,23 @@ def create_bram(dsc_f, sim_f, ref_f, tb_f, k1, k2, or_next):
     print("  end", file=tb_f)
     print("endmodule", file=tb_f)
 
-print("Rng seed: %d" % seed)
+parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
+parser.add_argument('-c', '--count', type = int, default = 5, help = 'number of test cases to generate')
+parser.add_argument('-d', '--debug', action='store_true')
+args = parser.parse_args()
+
+debug_mode = args.debug
+
+if args.seed is not None:
+    seed = args.seed
+else:
+    seed = (int(os.times()[4]*100) + os.getpid()) % 900000 + 100000
+
+print("PRNG seed: %d" % seed)
 random.seed(seed)
 
-for k1 in range(5):
+for k1 in range(args.count):
     dsc_f = open("temp/brams_%02d.txt" % k1, "w")
     sim_f = open("temp/brams_%02d.v" % k1, "w")
     ref_f = open("temp/brams_%02d_ref.v" % k1, "w")
diff --git a/tests/bram/run-single.sh b/tests/bram/run-single.sh
index 19a235c7..98a45b61 100644
--- a/tests/bram/run-single.sh
+++ b/tests/bram/run-single.sh
@@ -2,7 +2,7 @@
 set -e
 ../../yosys -qq -p "proc; opt; memory -nomap -bram temp/brams_${2}.txt; opt -fast -full" \
 		-l temp/synth_${1}_${2}.log -o temp/synth_${1}_${2}.v temp/brams_${1}.v
-iverilog -Dvcd_file=\"temp/tb_${1}_${2}.vcd\" -DSIMLIB_MEMDELAY=1ns -o temp/tb_${1}_${2}.tb temp/brams_${1}_tb.v \
+iverilog -Dvcd_file=\"temp/tb_${1}_${2}.vcd\" -DSIMLIB_MEMDELAY=1 -o temp/tb_${1}_${2}.tb temp/brams_${1}_tb.v \
 		temp/brams_${1}_ref.v temp/synth_${1}_${2}.v temp/brams_${2}.v ../../techlibs/common/simlib.v
 temp/tb_${1}_${2}.tb > temp/tb_${1}_${2}.txt
 if grep -q ERROR temp/tb_${1}_${2}.txt; then
diff --git a/tests/bram/run-test.sh b/tests/bram/run-test.sh
index f0bf0131..d6ba0de4 100755
--- a/tests/bram/run-test.sh
+++ b/tests/bram/run-test.sh
@@ -4,11 +4,26 @@
 # MAKE="make -j8" time bash -c 'for ((i=0; i<100; i++)); do echo "-- $i --"; bash run-test.sh || exit 1; done'
 
 set -e
+
+OPTIND=1
+count=5
+seed=""    # default to no seed specified
+debug=""
+while getopts "c:dS:" opt
+do
+    case "$opt" in
+	c) count="$OPTARG" ;;
+	d) debug="-d" ;;
+	S) seed="-S $OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 rm -rf temp
 mkdir -p temp
 
 echo "generating tests.."
-python3 generate.py
+python3 generate.py $debug -c $count $seed
 
 {
 	echo -n "all:"
diff --git a/tests/fsm/generate.py b/tests/fsm/generate.py
index 8757d474..c8eda0cd 100644
--- a/tests/fsm/generate.py
+++ b/tests/fsm/generate.py
@@ -1,5 +1,6 @@
 #!/usr/bin/env python3
 
+import argparse
 import sys
 import random
 from contextlib import contextmanager
@@ -30,7 +31,16 @@ def random_expr(variables):
         return "%d'd%s" % (bits, random.randint(0, 2**bits-1))
     raise AssertionError
 
-for idx in range(50):
+parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
+parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate')
+args = parser.parse_args()
+
+if args.seed is not None:
+    print("PRNG seed: %d" % args.seed)
+    random.seed(args.seed)
+
+for idx in range(args.count):
     with open('temp/uut_%05d.v' % idx, 'w') as f:
         with redirect_stdout(f):
             rst2 = random.choice([False, True])
diff --git a/tests/fsm/run-test.sh b/tests/fsm/run-test.sh
index 42389233..cf506470 100755
--- a/tests/fsm/run-test.sh
+++ b/tests/fsm/run-test.sh
@@ -5,10 +5,22 @@
 
 set -e
 
+OPTIND=1
+count=100
+seed=""    # default to no seed specified
+while getopts "c:S:" opt
+do
+    case "$opt" in
+	c) count="$OPTARG" ;;
+	S) seed="-S $OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 rm -rf temp
 mkdir -p temp
 echo "generating tests.."
-python3 generate.py
+python3 generate.py -c $count $seed
 
 {
 	all_targets="all_targets:"
diff --git a/tests/hana/run-test.sh b/tests/hana/run-test.sh
index fb766eec..878c80b3 100755
--- a/tests/hana/run-test.sh
+++ b/tests/hana/run-test.sh
@@ -1,2 +1,14 @@
 #!/bin/bash
-exec ${MAKE:-make} -f ../tools/autotest.mk EXTRA_FLAGS="-l hana_vlib.v -n 300 -e" test_*.v
+
+OPTIND=1
+seed=""    # default to no seed specified
+while getopts "S:" opt
+do
+    case "$opt" in
+	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+	   seed="SEED=$arg" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed EXTRA_FLAGS="-l hana_vlib.v -n 300 -e" test_*.v
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index c3b19618..734a9668 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -1,7 +1,18 @@
 #!/bin/bash
 
 set -e
-bash ../tools/autotest.sh -G *.v
+
+OPTIND=1
+seed=""    # default to no seed specified
+while getopts "S:" opt
+do
+    case "$opt" in
+	S) seed="-S $OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
+bash ../tools/autotest.sh $seed -G *.v
 
 for f in `egrep -l 'expect-(wr|rd)-ports' *.v`; do
 	echo -n "Testing expectations for $f .."
diff --git a/tests/realmath/generate.py b/tests/realmath/generate.py
index 19d01c7c..2bedf38e 100644
--- a/tests/realmath/generate.py
+++ b/tests/realmath/generate.py
@@ -1,5 +1,6 @@
 #!/usr/bin/env python3
 
+import argparse
 import sys
 import random
 from contextlib import contextmanager
@@ -36,7 +37,16 @@ def random_expression(depth = 3, maxparam = 0):
         return op + '(' + recursion() + ', ' + recursion() + ')'
     raise
 
-for idx in range(100):
+parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
+parser.add_argument('-c', '--count', type = int, default = 100, help = 'number of test cases to generate')
+args = parser.parse_args()
+
+if args.seed is not None:
+    print("PRNG seed: %d" % args.seed)
+    random.seed(args.seed)
+
+for idx in range(args.count):
     with open('temp/uut_%05d.v' % idx, 'w') as f:
         with redirect_stdout(f):
             print('module uut_%05d(output [63:0] %s);\n' % (idx, ', '.join(['y%02d' % i for i in range(100)])))
diff --git a/tests/realmath/run-test.sh b/tests/realmath/run-test.sh
index f1ec5476..e1a36c69 100755
--- a/tests/realmath/run-test.sh
+++ b/tests/realmath/run-test.sh
@@ -1,14 +1,26 @@
 #!/bin/bash
 set -e
 
+OPTIND=1
+count=100
+seed=""    # default to no seed specified
+while getopts "c:S:" opt
+do
+    case "$opt" in
+	c) count="$OPTARG" ;;
+	S) seed="-S $OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 rm -rf temp
 mkdir -p temp
 echo "generating tests.."
-python3 generate.py
+python3 generate.py -c $count $seed
 
 cd temp
 echo "running tests.."
-for ((i = 0; i < 100; i++)); do
+for ((i = 0; i < $count; i++)); do
 	echo -n "[$i]"
 	idx=$( printf "%05d" $i )
 	../../../yosys -qq uut_${idx}.ys
diff --git a/tests/share/generate.py b/tests/share/generate.py
index 01a19a8d..7e87bd64 100644
--- a/tests/share/generate.py
+++ b/tests/share/generate.py
@@ -1,5 +1,6 @@
 #!/usr/bin/env python3
 
+import argparse
 import sys
 import random
 from contextlib import contextmanager
@@ -21,7 +22,16 @@ def maybe_plus_x(expr):
     else:
         return expr
 
-for idx in range(100):
+parser = argparse.ArgumentParser(formatter_class = argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
+parser.add_argument('-c', '--count', type = int, default = 100, help = 'number of test cases to generate')
+args = parser.parse_args()
+
+if args.seed is not None:
+    print("PRNG seed: %d" % args.seed)
+    random.seed(args.seed)
+
+for idx in range(args.count):
     with open('temp/uut_%05d.v' % idx, 'w') as f:
         with redirect_stdout(f):
             if random.choice(['bin', 'uni']) == 'bin':
diff --git a/tests/share/run-test.sh b/tests/share/run-test.sh
index 18dbbc27..1bcd8e42 100755
--- a/tests/share/run-test.sh
+++ b/tests/share/run-test.sh
@@ -5,10 +5,22 @@
 
 set -e
 
+OPTIND=1
+count=100
+seed=""    # default to no seed specified
+while getopts "c:S:" opt
+do
+    case "$opt" in
+	c) count="$OPTARG" ;;
+	S) seed="-S $OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 rm -rf temp
 mkdir -p temp
 echo "generating tests.."
-python3 generate.py
+python3 generate.py -c $count $seed
 
 echo "running tests.."
 for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do
diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh
index 6531d51a..aaa1cf94 100755
--- a/tests/simple/run-test.sh
+++ b/tests/simple/run-test.sh
@@ -1,9 +1,20 @@
 #!/bin/bash
 
+OPTIND=1
+seed=""    # default to no seed specified
+while getopts "S:" opt
+do
+    case "$opt" in
+	S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space
+	   seed="SEED=$arg" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 # check for Icarus Verilog
 if ! which iverilog > /dev/null ; then
   echo "$0: Error: Icarus Verilog 'iverilog' not found."
   exit 1
 fi
 
-exec ${MAKE:-make} -f ../tools/autotest.mk *.v
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v
diff --git a/tests/tools/autotest.mk b/tests/tools/autotest.mk
index f65002ce..c6867892 100644
--- a/tests/tools/autotest.mk
+++ b/tests/tools/autotest.mk
@@ -1,8 +1,13 @@
 
 EXTRA_FLAGS=
+SEED=
+
+ifneq ($(strip $(SEED)),)
+SEEDOPT=-S$(SEED)
+endif
 
 $(MAKECMDGOALS):
-	@$(basename $(MAKEFILE_LIST)).sh -G -j $(EXTRA_FLAGS) $@
+	@$(basename $(MAKEFILE_LIST)).sh -G -j $(SEEDOPT) $(EXTRA_FLAGS) $@
 
 .PHONY: $(MAKECMDGOALS)