Merge branch 'YosysHQ-master'

28 files changed, 1348 insertions, 189 deletions

diff --git a/Makefile b/Makefile
index 1caa0038b..11803ec0a 100644
--- a/Makefile
+++ b/Makefile
@@ -15,6 +15,7 @@ ENABLE_EDITLINE := 0
 ENABLE_VERIFIC := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
+ENABLE_PROTOBUF := 0
 
 # other configuration flags
 ENABLE_GPROF := 0
@@ -22,6 +23,9 @@ ENABLE_DEBUG := 0
 ENABLE_NDEBUG := 0
 LINK_CURSES := 0
 LINK_TERMCAP := 0
+LINK_ABC := 0
+# Needed for environments that don't have proper thread support (i.e. emscripten)
+DISABLE_ABC_THREADS := 0
 
 # clang sanitizers
 SANITIZER =
@@ -103,7 +107,7 @@ OBJS = kernel/version_$(GIT_REV).o
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = f23ea8e
+ABCREV = 6df1396
 ABCPULL = 1
 ABCURL ?= https://github.com/berkeley-abc/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
@@ -126,6 +130,7 @@ ifeq ($(CONFIG),clang)
 CXX = clang
 LD = clang++
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 ifneq ($(SANITIZER),)
 $(info [Clang Sanitizer] $(SANITIZER))
@@ -148,16 +153,19 @@ else ifeq ($(CONFIG),gcc)
 CXX = gcc
 LD = gcc
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 else ifeq ($(CONFIG),gcc-4.8)
 CXX = gcc-4.8
 LD = gcc-4.8
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 else ifeq ($(CONFIG),emcc)
 CXX = emcc
 LD = emcc
 CXXFLAGS := -std=c++11 $(filter-out -fPIC -ggdb,$(CXXFLAGS))
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8"
 EMCCFLAGS := -Os -Wno-warn-absolute-paths
 EMCCFLAGS += --memory-init-file 0 --embed-file share -s NO_EXIT_RUNTIME=1
 EMCCFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg']"
@@ -171,6 +179,11 @@ EXE = .js
 TARGETS := $(filter-out yosys-config,$(TARGETS))
 EXTRA_TARGETS += yosysjs-$(YOSYS_VER).zip
 
+ifeq ($(ENABLE_ABC),1)
+LINK_ABC := 1
+DISABLE_ABC_THREADS := 1
+endif
+
 viz.js:
 	wget -O viz.js.part https://github.com/mdaines/viz.js/releases/download/0.0.3/viz.js
 	mv viz.js.part viz.js
@@ -192,8 +205,8 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
-ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1 CC="$(CXX)" CXX="$(CXX)"
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
+ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1
 EXE = .exe
 
 else ifeq ($(CONFIG),msys2)
@@ -203,8 +216,8 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
-ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)"
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
+ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0
 EXE = .exe
 
 else ifneq ($(CONFIG),none)
@@ -236,9 +249,15 @@ else
 ifeq ($(ENABLE_EDITLINE),1)
 CXXFLAGS += -DYOSYS_ENABLE_EDITLINE
 LDLIBS += -ledit -ltinfo -lbsd
+else
+ABCMKARGS += "ABC_USE_NO_READLINE=1"
 endif
 endif
 
+ifeq ($(DISABLE_ABC_THREADS),1)
+ABCMKARGS += "ABC_USE_NO_PTHREADS=1"
+endif
+
 ifeq ($(ENABLE_PLUGINS),1)
 CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags libffi) -DYOSYS_ENABLE_PLUGINS
 LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi)
@@ -288,10 +307,17 @@ endif
 
 ifeq ($(ENABLE_ABC),1)
 CXXFLAGS += -DYOSYS_ENABLE_ABC
+ifeq ($(LINK_ABC),1)
+CXXFLAGS += -DYOSYS_LINK_ABC
+ifeq ($(DISABLE_ABC_THREADS),0)
+LDLIBS += -lpthread
+endif
+else
 ifeq ($(ABCEXTERNAL),)
 TARGETS += yosys-abc$(EXE)
 endif
 endif
+endif
 
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= /usr/local/src/verific_lib_eval
@@ -300,6 +326,10 @@ CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABL
 LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -lz
 endif
 
+ifeq ($(ENABLE_PROTOBUF),1)
+LDLIBS += $(shell pkg-config --cflags --libs protobuf)
+endif
+
 ifeq ($(ENABLE_COVER),1)
 CXXFLAGS += -DYOSYS_ENABLE_COVER
 endif
@@ -411,6 +441,10 @@ include techlibs/common/Makefile.inc
 
 endif
 
+ifeq ($(LINK_ABC),1)
+OBJS += yosys-libabc.a
+endif
+
 top-all: $(TARGETS) $(EXTRA_TARGETS)
 	@echo ""
 	@echo "  Build successful."
@@ -455,7 +489,7 @@ yosys-config: misc/yosys-config.in
 			-e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > yosys-config
 	$(Q) chmod +x yosys-config
 
-abc/abc-$(ABCREV)$(EXE):
+abc/abc-$(ABCREV)$(EXE) abc/libabc-$(ABCREV).a:
 	$(P)
 ifneq ($(ABCREV),default)
 	$(Q) if test -d abc/.hg; then \
@@ -472,15 +506,19 @@ ifneq ($(ABCREV),default)
 	fi
 endif
 	$(Q) rm -f abc/abc-[0-9a-f]*
-	$(Q) cd abc && $(MAKE) $(S) $(ABCMKARGS) PROG="abc-$(ABCREV)$(EXE)" MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: "
+	$(Q) cd abc && $(MAKE) $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc-$(ABCREV)",PROG="abc-$(ABCREV)$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc-$(ABCREV).a)
 
 ifeq ($(ABCREV),default)
 .PHONY: abc/abc-$(ABCREV)$(EXE)
+.PHONY: abc/libabc-$(ABCREV).a
 endif
 
 yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE)
 	$(P) cp abc/abc-$(ABCREV)$(EXE) yosys-abc$(EXE)
 
+yosys-libabc.a: abc/libabc-$(ABCREV).a
+	$(P) cp abc/libabc-$(ABCREV).a yosys-libabc.a
+
 ifneq ($(SEED),)
 SEEDOPT="-S $(SEED)"
 else
@@ -564,7 +602,7 @@ clean:
 	rm -rf share
 	if test -d manual; then cd manual && sh clean.sh; fi
 	rm -f $(OBJS) $(GENFILES) $(TARGETS) $(EXTRA_TARGETS) $(EXTRA_OBJS)
-	rm -f kernel/version_*.o kernel/version_*.cc abc/abc-[0-9a-f]*
+	rm -f kernel/version_*.o kernel/version_*.cc abc/abc-[0-9a-f]* abc/libabc-[0-9a-f]*.a
 	rm -f libs/*/*.d frontends/*/*.d passes/*/*.d backends/*/*.d kernel/*.d techlibs/*/*.d
 	rm -rf tests/asicworld/*.out tests/asicworld/*.log
 	rm -rf tests/hana/*.out tests/hana/*.log
@@ -577,7 +615,7 @@ clean:
 
 clean-abc:
 	$(MAKE) -C abc DEP= clean
-	rm -f yosys-abc$(EXE) abc/abc-[0-9a-f]*
+	rm -f yosys-abc$(EXE) yosys-libabc.a abc/abc-[0-9a-f]* abc/libabc-[0-9a-f]*.a
 
 mrproper: clean
 	git clean -xdf
diff --git a/README.md b/README.md
index d5184bd7d..c02691d94 100644
--- a/README.md
+++ b/README.md
@@ -52,19 +52,19 @@ For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
 
 	$ sudo apt-get install build-essential clang bison flex \
-		libreadline-dev gawk tcl-dev libffi-dev git mercurial \
+		libreadline-dev gawk tcl-dev libffi-dev git \
 		graphviz xdot pkg-config python3
 
 Similarily, on Mac OS X MacPorts or Homebrew can be used to install dependencies:
 
 	$ brew tap Homebrew/bundle && brew bundle
 	$ sudo port install bison flex readline gawk libffi \
-		git mercurial graphviz pkgconfig python36
+		git graphviz pkgconfig python36
 
 On FreeBSD use the following command to install all prerequisites:
 
 	# pkg install bison flex readline gawk libffi\
-		git mercurial graphviz pkgconfig python3 python36 tcl-wrapper
+		git graphviz pkgconfig python3 python36 tcl-wrapper
 
 On FreeBSD system use gmake instead of make. To run tests use:
     % MAKE=gmake CC=cc gmake test
@@ -418,7 +418,9 @@ Non-standard or SystemVerilog features for formal verification
   supported in any clocked block.
 
 - The syntax ``@($global_clock)`` can be used to create FFs that have no
-  explicit clock input ($ff cells).
+  explicit clock input ($ff cells). The same can be achieved by using
+  ``@(posedge <netname>)`` or ``@(negedge <netname>)`` when ``<netname>``
+  is marked with the ``(* gclk *)`` Verilog attribute.
 
 
 Supported features from SystemVerilog
diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore
new file mode 100644
index 000000000..849b38d45
--- /dev/null
+++ b/backends/protobuf/.gitignore
@@ -0,0 +1,2 @@
+yosys.pb.cc
+yosys.pb.h
diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
new file mode 100644
index 000000000..834cad42c
--- /dev/null
+++ b/backends/protobuf/Makefile.inc
@@ -0,0 +1,8 @@
+ifeq ($(ENABLE_PROTOBUF),1)
+
+backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto
+	$(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
+
+OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o
+
+endif
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
new file mode 100644
index 000000000..9a6fedee7
--- /dev/null
+++ b/backends/protobuf/protobuf.cc
@@ -0,0 +1,370 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
+ *
+ *  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 <google/protobuf/text_format.h>
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include "yosys.pb.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct ProtobufDesignSerializer
+{
+	bool aig_mode_;
+	bool use_selection_;
+	yosys::pb::Design *pb_;
+
+	Design *design_;
+	Module *module_;
+
+	SigMap sigmap_;
+	int sigidcounter_;
+	dict<SigBit, uint64_t> sigids_;
+	pool<Aig> aig_models_;
+
+
+	ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
+			aig_mode_(aig_mode), use_selection_(use_selection) { }
+	
+	string get_name(IdString name)
+	{
+		return RTLIL::unescape_id(name);
+	}
+
+
+	void serialize_parameters(google::protobuf::Map<std::string, yosys::pb::Parameter> *out,
+		const dict<IdString, Const> &parameters)
+	{
+		for (auto &param : parameters) {
+			std::string key = get_name(param.first);
+			
+
+			yosys::pb::Parameter pb_param;
+
+			if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
+				pb_param.set_str(param.second.decode_string());
+			} else if (GetSize(param.second.bits) > 64) {
+				pb_param.set_str(param.second.as_string());
+			} else {
+				pb_param.set_int_(param.second.as_int());
+			}
+
+			(*out)[key] = pb_param;
+		}
+	}
+
+	void get_bits(yosys::pb::BitVector *out, SigSpec sig)
+	{
+		for (auto bit : sigmap_(sig)) {
+			auto sig = out->add_signal();
+
+			// Constant driver.
+			if (bit.wire == nullptr) {
+				if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW);
+				else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH);
+				else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z);
+				else sig->set_constant(sig->CONSTANT_DRIVER_X);
+				continue;
+			}
+
+			// Signal - give it a unique identifier.
+			if (sigids_.count(bit) == 0) {
+				sigids_[bit] = sigidcounter_++;
+			}
+			sig->set_id(sigids_[bit]);
+		}
+	}
+
+	void serialize_module(yosys::pb::Module* out, Module *module)
+	{
+		module_ = module;
+		log_assert(module_->design == design_);
+		sigmap_.set(module_);
+		sigids_.clear();
+		sigidcounter_ = 0;
+
+		serialize_parameters(out->mutable_attribute(), module_->attributes);
+
+		for (auto n : module_->ports) {
+			Wire *w = module->wire(n);
+			if (use_selection_ && !module_->selected(w))
+				continue;
+
+			yosys::pb::Module::Port pb_port;
+			pb_port.set_direction(w->port_input ? w->port_output ?
+				yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT);
+			get_bits(pb_port.mutable_bits(), w);
+			(*out->mutable_port())[get_name(n)] = pb_port;
+		}
+
+		for (auto c : module_->cells()) {
+			if (use_selection_ && !module_->selected(c))
+				continue;
+
+			yosys::pb::Module::Cell pb_cell;
+			pb_cell.set_hide_name(c->name[0] == '$');
+			pb_cell.set_type(get_name(c->type));
+
+			if (aig_mode_) {
+				Aig aig(c);
+				if (aig.name.empty())
+					continue;
+				pb_cell.set_model(aig.name);
+				aig_models_.insert(aig);
+			}
+			serialize_parameters(pb_cell.mutable_parameter(), c->parameters);
+			serialize_parameters(pb_cell.mutable_attribute(), c->attributes);
+
+			if (c->known()) {
+				for (auto &conn : c->connections()) {
+					yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT;
+					if (c->input(conn.first))
+						direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT;
+					(*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction;
+				}
+			}
+			for (auto &conn : c->connections()) {
+				yosys::pb::BitVector vec;
+				get_bits(&vec, conn.second);
+				(*pb_cell.mutable_connection())[get_name(conn.first)] = vec;
+			}
+
+			(*out->mutable_cell())[get_name(c->name)] = pb_cell;
+		}
+
+		for (auto w : module_->wires()) {
+			if (use_selection_ && !module_->selected(w))
+				continue;
+
+			auto netname = out->add_netname();
+			netname->set_hide_name(w->name[0] == '$');
+			get_bits(netname->mutable_bits(), w);
+			serialize_parameters(netname->mutable_attributes(), w->attributes);
+		}
+	}
+
+
+	void serialize_models(google::protobuf::Map<string, yosys::pb::Model> *models)
+	{
+		for (auto &aig : aig_models_) {
+			yosys::pb::Model pb_model;
+			for (auto &node : aig.nodes) {
+				auto pb_node = pb_model.add_node();
+				if (node.portbit >= 0) {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_NPORT);
+					} else {
+						pb_node->set_type(pb_node->TYPE_PORT);
+					}
+					auto port = pb_node->mutable_port();
+					port->set_portname(log_id(node.portname));
+					port->set_bitindex(node.portbit);
+				} else if (node.left_parent < 0 && node.right_parent < 0) {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_TRUE);
+					} else {
+						pb_node->set_type(pb_node->TYPE_FALSE);
+					}
+				} else {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_NAND);
+					} else {
+						pb_node->set_type(pb_node->TYPE_AND);
+					}
+					auto gate = pb_node->mutable_gate();
+					gate->set_left(node.left_parent);
+					gate->set_right(node.right_parent);
+				}
+				for (auto &op : node.outports) {
+					auto pb_op = pb_node->add_out_port();
+					pb_op->set_name(log_id(op.first));
+					pb_op->set_bit_index(op.second);
+				}
+			}
+			(*models)[aig.name] = pb_model;
+		}
+	}
+	
+	void serialize_design(yosys::pb::Design *pb, Design *design)
+	{
+		GOOGLE_PROTOBUF_VERIFY_VERSION;
+		pb_ = pb;
+		pb_->Clear();
+		pb_->set_creator(yosys_version_str);
+
+		design_ = design;
+		design_->sort();
+
+		auto modules = use_selection_ ? design_->selected_modules() : design_->modules();
+		for (auto mod : modules) {
+			yosys::pb::Module pb_mod;
+			serialize_module(&pb_mod, mod);
+			(*pb->mutable_modules())[mod->name.str()] = pb_mod;
+		}
+
+		serialize_models(pb_->mutable_models());
+	}
+};
+
+struct ProtobufBackend : public Backend {
+	ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_protobuf [options] [filename]\n");
+		log("\n");
+		log("Write a JSON netlist of the current design.\n");
+		log("\n");
+		log("    -aig\n");
+		log("        include AIG models for the different gate types\n");
+		log("\n");
+		log("    -text\n");
+		log("        output protobuf in Text/ASCII representation\n");
+		log("\n");
+		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
+		log("Yosys source code distribution.\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		bool aig_mode = false;
+		bool text_mode = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-aig") {
+				aig_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-text") {
+				text_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		log_header(design, "Executing Protobuf backend.\n");
+
+		yosys::pb::Design pb;
+		ProtobufDesignSerializer serializer(false, aig_mode);
+		serializer.serialize_design(&pb, design);
+
+		if (text_mode) {
+			string out;
+			google::protobuf::TextFormat::PrintToString(pb, &out);
+			*f << out;
+		} else {
+			pb.SerializeToOstream(f);
+		}
+	}
+} ProtobufBackend;
+
+struct ProtobufPass : public Pass {
+	ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    protobuf [options] [selection]\n");
+		log("\n");
+		log("Write a JSON netlist of all selected objects.\n");
+		log("\n");
+		log("    -o <filename>\n");
+		log("        write to the specified file.\n");
+		log("\n");
+		log("    -aig\n");
+		log("        include AIG models for the different gate types\n");
+		log("\n");
+		log("    -text\n");
+		log("        output protobuf in Text/ASCII representation\n");
+		log("\n");
+		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
+		log("Yosys source code distribution.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		std::string filename;
+		bool aig_mode = false;
+		bool text_mode = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-o" && argidx+1 < args.size()) {
+				filename = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-aig") {
+				aig_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-text") {
+				text_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		std::ostream *f;
+		std::stringstream buf;
+
+		if (!filename.empty()) {
+			std::ofstream *ff = new std::ofstream;
+			ff->open(filename.c_str(), std::ofstream::trunc);
+			if (ff->fail()) {
+				delete ff;
+				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+			}
+			f = ff;
+		} else {
+			f = &buf;
+		}
+
+		yosys::pb::Design pb;
+		ProtobufDesignSerializer serializer(true, aig_mode);
+		serializer.serialize_design(&pb, design);
+
+		if (text_mode) {
+			string out;
+			google::protobuf::TextFormat::PrintToString(pb, &out);
+			*f << out;
+		} else {
+			pb.SerializeToOstream(f);
+		}
+
+		if (!filename.empty()) {
+			delete f;
+		} else {
+			log("%s", buf.str().c_str());
+		}
+	}
+} ProtobufPass;
+
+PRIVATE_NAMESPACE_END;
diff --git a/examples/cmos/counter.ys b/examples/cmos/counter.ys
index a784f3465..d0b093667 100644
--- a/examples/cmos/counter.ys
+++ b/examples/cmos/counter.ys
@@ -1,11 +1,12 @@
-
 read_verilog counter.v
 read_verilog -lib cmos_cells.v
 
-proc;; memory;; techmap;;
-
+synth
 dfflibmap -liberty cmos_cells.lib
-abc -liberty cmos_cells.lib;;
+abc -liberty cmos_cells.lib
+opt_clean
+
+stat -liberty cmos_cells.lib
 
 # http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/latest/cadence/lib/tsmc025/signalstorm/osu025_stdcells.lib
 # dfflibmap -liberty osu025_stdcells.lib
@@ -13,4 +14,3 @@ abc -liberty cmos_cells.lib;;
 
 write_verilog synth.v
 write_spice synth.sp
-
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 57ba9668d..d9f0039af 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -223,12 +223,18 @@ struct AST_INTERNAL::ProcessGenerator
 		bool found_global_syncs = false;
 		bool found_anyedge_syncs = false;
 		for (auto child : always->children)
+		{
+			if ((child->type == AST_POSEDGE || child->type == AST_NEGEDGE) && GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER &&
+					child->children.at(0)->id2ast && child->children.at(0)->id2ast->type == AST_WIRE && child->children.at(0)->id2ast->get_bool_attribute("\\gclk")) {
+				found_global_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)
@@ -242,6 +248,9 @@ struct AST_INTERNAL::ProcessGenerator
 		bool found_clocked_sync = false;
 		for (auto child : always->children)
 			if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) {
+				if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->id2ast &&
+						child->children.at(0)->id2ast->type == AST_WIRE && child->children.at(0)->id2ast->get_bool_attribute("\\gclk"))
+					continue;
 				found_clocked_sync = true;
 				if (found_global_syncs || found_anyedge_syncs)
 					log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
@@ -1291,6 +1300,9 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 			cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(0);
 			cell->parameters["\\TRANSPARENT"] = RTLIL::Const(0);
 
+			if (!sign_hint)
+				is_signed = false;
+
 			return RTLIL::SigSpec(wire);
 		}
 
diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc
index c9b6a54b2..b9e53a4be 100644
--- a/frontends/liberty/liberty.cc
+++ b/frontends/liberty/liberty.cc
@@ -148,7 +148,7 @@ static bool parse_func_reduce(RTLIL::Module *module, std::vector<token_t> &stack
 	}
 
 	if (0 <= top && stack[top].type == 2) {
-		if (next_token.type == '*' || next_token.type == '&' || next_token.type == 0 || next_token.type == '(')
+		if (next_token.type == '*' || next_token.type == '&' || next_token.type == 0 || next_token.type == '(' || next_token.type == '!')
 			return false;
 		stack[top].type = 3;
 		return true;
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index ee09c7523..62a8028b8 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -62,6 +62,7 @@ using namespace Verific;
 YOSYS_NAMESPACE_BEGIN
 
 int verific_verbose;
+bool verific_import_pending;
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
@@ -189,12 +190,12 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
 	}
 }
 
-RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
+RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
 {
 	RTLIL::SigSpec sig;
 	RTLIL::Wire *dummy_wire = NULL;
 	for (int i = int(inst->OutputSize())-1; i >= 0; i--)
-		if (inst->GetOutputBit(i)) {
+		if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
 			sig.append(net_map_at(inst->GetOutputBit(i)));
 			dummy_wire = NULL;
 		} else {
@@ -244,7 +245,9 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 	}
 
 	if (inst->Type() == PRIM_BUF) {
-		module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		auto outnet = inst->GetOutput();
+		if (!any_all_nets.count(outnet))
+			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
 		return true;
 	}
 
@@ -394,6 +397,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 	#define IN1 operatorInput1(inst)
 	#define IN2 operatorInput2(inst)
 	#define OUT operatorOutput(inst)
+	#define FILTERED_OUT operatorOutput(inst, &any_all_nets)
 	#define SIGNED inst->View()->IsSigned()
 
 	if (inst->Type() == OPER_ADDER) {
@@ -525,7 +529,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 	}
 
 	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(inst_name, IN, OUT, SIGNED);
+		module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
 		return true;
 	}
 
@@ -791,6 +795,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	dict<Net*, char, hash_ptr_ops> init_nets;
 	pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
 	pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
+	any_all_nets.clear();
 
 	FOREACH_NET_OF_NETLIST(nl, mi, net)
 	{
@@ -871,23 +876,30 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		const char *allconst_attr = net->GetAttValue("allconst");
 		const char *allseq_attr = net->GetAttValue("allseq");
 
-		if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
+		if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
 			anyconst_nets.insert(net);
-
-		else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
+			any_all_nets.insert(net);
+		}
+		else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
 			anyseq_nets.insert(net);
-
-		else if (anyconst_attr != nullptr && !strcmp(anyconst_attr, "1"))
+			any_all_nets.insert(net);
+		}
+		else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
 			anyconst_nets.insert(net);
-
-		else if (anyseq_attr != nullptr && !strcmp(anyseq_attr, "1"))
+			any_all_nets.insert(net);
+		}
+		else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
 			anyseq_nets.insert(net);
-
-		else if (allconst_attr != nullptr && !strcmp(allconst_attr, "1"))
+			any_all_nets.insert(net);
+		}
+		else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
 			allconst_nets.insert(net);
-
-		else if (allseq_attr != nullptr && !strcmp(allseq_attr, "1"))
+			any_all_nets.insert(net);
+		}
+		else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
 			allseq_nets.insert(net);
+			any_all_nets.insert(net);
+		}
 
 		if (net_map.count(net)) {
 			if (verific_verbose)
@@ -1064,7 +1076,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		}
 
 		if (inst->Type() == PRIM_BUF) {
-			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+			auto outnet = inst->GetOutput();
+			if (!any_all_nets.count(outnet))
+				module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
 			continue;
 		}
 
@@ -1382,7 +1396,8 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 			return;
 	}
 
-	if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
+	// Use while() instead of if() to work around VIPER #13453
+	while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
 	{
 		net = inst->GetInput();
 		inst = net->Driver();;
@@ -1456,6 +1471,10 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 
 	clock_net = net;
 	clock_sig = importer->net_map_at(clock_net);
+
+	const char *gclk_attr = clock_net->GetAttValue("gclk");
+	if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
+		gclk = true;
 }
 
 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
@@ -1478,15 +1497,20 @@ Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const
 		sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
 
 	if (disable_sig != State::S0) {
+		log_assert(gclk == false);
 		log_assert(GetSize(sig_q) == GetSize(init_value));
 		return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
 	}
 
+	if (gclk)
+		return module->addFf(name, sig_d, sig_q);
+
 	return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
 }
 
 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
 {
+	log_assert(gclk == false);
 	log_assert(disable_sig == State::S0);
 
 	if (enable_sig != State::S1)
@@ -1497,6 +1521,7 @@ Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec s
 
 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
 {
+	log_assert(gclk == false);
 	log_assert(disable_sig == State::S0);
 
 	if (enable_sig != State::S1)
@@ -1589,11 +1614,71 @@ struct VerificExtNets
 	}
 };
 
+void verific_import(Design *design, std::string top)
+{
+	std::set<Netlist*> nl_todo, nl_done;
+
+	{
+		VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+		VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+
+		Array veri_libs, vhdl_libs;
+		if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+		if (veri_lib) veri_libs.InsertLast(veri_lib);
+
+		Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+		Netlist *nl;
+		int i;
+
+		FOREACH_ARRAY_ITEM(netlists, i, nl) {
+			if (top.empty() || nl->Owner()->Name() == top)
+				nl_todo.insert(nl);
+		}
+
+		delete netlists;
+	}
+
+	if (!verific_error_msg.empty())
+		log_error("%s\n", verific_error_msg.c_str());
+
+	VerificExtNets worker;
+	for (auto nl : nl_todo)
+		worker.run(nl);
+
+	while (!nl_todo.empty()) {
+		Netlist *nl = *nl_todo.begin();
+		if (nl_done.count(nl) == 0) {
+			VerificImporter importer(false, false, false, false, false, false);
+			importer.import_netlist(design, nl, nl_todo);
+		}
+		nl_todo.erase(nl);
+		nl_done.insert(nl);
+	}
+
+	veri_file::Reset();
+	vhdl_file::Reset();
+	Libset::Reset();
+	verific_import_pending = false;
+
+	if (!verific_error_msg.empty())
+		log_error("%s\n", verific_error_msg.c_str());
+}
+
 YOSYS_NAMESPACE_END
 #endif /* YOSYS_ENABLE_VERIFIC */
 
 PRIVATE_NAMESPACE_BEGIN
 
+bool check_noverific_env()
+{
+	const char *e = getenv("YOSYS_NOVERIFIC");
+	if (e == nullptr)
+		return false;
+	if (atoi(e) == 0)
+		return false;
+	return true;
+}
+
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
 	virtual void help()
@@ -1608,6 +1693,14 @@ struct VerificPass : public Pass {
 		log("Files passed to different calls to this command are treated as belonging to\n");
 		log("different compilation units.\n");
 		log("\n");
+		log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+		log("the language version (and before file names) to set additional verilog defines.\n");
+		log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
+		log("\n");
+		log("\n");
+		log("    verific -formal <verilog-file>..\n");
+		log("\n");
+		log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
 		log("\n");
 		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
@@ -1627,7 +1720,12 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("    verific -vlog-define <macro>[=<value>]..\n");
 		log("\n");
-		log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
+		log("Add Verilog defines.\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-undef <macro>..\n");
+		log("\n");
+		log("Remove Verilog defines previously set with -vlog-define.\n");
 		log("\n");
 		log("\n");
 		log("    verific -import [options] <top-module>..\n");
@@ -1684,6 +1782,9 @@ struct VerificPass : public Pass {
 #ifdef YOSYS_ENABLE_VERIFIC
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
+		if (check_noverific_env())
+			log_cmd_error("This version of Yosys is built without Verific support.\n");
+
 		log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
 
 		Message::SetConsoleOutput(0);
@@ -1694,8 +1795,6 @@ struct VerificPass : public Pass {
 		RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
 		RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
 		RuntimeFlags::SetVar("db_infer_wide_operators", 1);
-		veri_file::DefineCmdLineMacro("VERIFIC");
-		veri_file::DefineCmdLineMacro("SYNTHESIS");
 
 		verific_verbose = 0;
 
@@ -1740,8 +1839,16 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				string name = args[argidx];
+				veri_file::UndefineMacro(name.c_str());
+			}
+			goto check_error;
+		}
+
 		if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
-				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv"))
+				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
 		{
 			Array file_names;
 			unsigned verilog_mode;
@@ -1754,17 +1861,38 @@ struct VerificPass : public Pass {
 				verilog_mode = veri_file::SYSTEM_VERILOG_2005;
 			else if (args[argidx] == "-sv2009")
 				verilog_mode = veri_file::SYSTEM_VERILOG_2009;
-			else if (args[argidx] == "-sv2012" || args[argidx] == "-sv")
+			else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
 				verilog_mode = veri_file::SYSTEM_VERILOG;
 			else
 				log_abort();
 
-			for (argidx++; argidx < GetSize(args); argidx++)
-				file_names.Insert(args[argidx].c_str());
+			veri_file::DefineMacro("VERIFIC");
+			veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
+
+			for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
+				std::string name = args[argidx].substr(2);
+				if (args[argidx] == "-D") {
+					if (++argidx >= GetSize(args))
+						break;
+					name = args[argidx];
+				}
+				size_t equal = name.find('=');
+				if (equal != std::string::npos) {
+					string value = name.substr(equal+1);
+					name = name.substr(0, equal);
+					veri_file::DefineMacro(name.c_str(), value.c_str());
+				} else {
+					veri_file::DefineMacro(name.c_str());
+				}
+			}
+
+			while (argidx < GetSize(args))
+				file_names.Insert(args[argidx++].c_str());
 
 			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
 					log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
 
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1773,6 +1901,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
 					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1781,6 +1910,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
 					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1789,6 +1919,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
 					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1797,6 +1928,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
 					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -2007,6 +2139,7 @@ struct VerificPass : public Pass {
 			veri_file::Reset();
 			vhdl_file::Reset();
 			Libset::Reset();
+			verific_import_pending = false;
 			goto check_error;
 		}
 
@@ -2024,5 +2157,114 @@ struct VerificPass : public Pass {
 #endif
 } VerificPass;
 
-PRIVATE_NAMESPACE_END
+struct ReadPass : public Pass {
+	ReadPass() : Pass("read", "load HDL designs") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
+		log("\n");
+		log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
+		log("is only available via Verific.)\n");
+		log("\n");
+		log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+		log("the language version (and before file names) to set additional verilog defines.\n");
+		log("\n");
+		log("\n");
+		log("    read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
+		log("\n");
+		log("Load the specified VHDL files. (Requires Verific.)\n");
+		log("\n");
+		log("\n");
+		log("    read -define <macro>[=<value>]..\n");
+		log("\n");
+		log("Set global Verilog/SystemVerilog defines.\n");
+		log("\n");
+		log("\n");
+		log("    read -undef <macro>..\n");
+		log("\n");
+		log("Unset global Verilog/SystemVerilog defines.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		if (args.size() < 2)
+			log_cmd_error("Missing mode parameter.\n");
 
+		if (args.size() < 3)
+			log_cmd_error("Missing file name parameter.\n");
+
+#ifdef YOSYS_ENABLE_VERIFIC
+		bool use_verific = !check_noverific_env();
+#else
+		bool use_verific = false;
+#endif
+
+		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
+			if (use_verific) {
+				args[0] = "verific";
+			} else {
+				args[0] = "read_verilog";
+				args.erase(args.begin()+1, args.begin()+2);
+			}
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
+			if (use_verific) {
+				args[0] = "verific";
+			} else {
+				args[0] = "read_verilog";
+				if (args[1] == "-formal")
+					args.insert(args.begin()+1, std::string());
+				args[1] = "-sv";
+			}
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
+			if (use_verific) {
+				args[0] = "verific";
+				Pass::call(design, args);
+			} else {
+				log_cmd_error("This version of Yosys is built without Verific support.\n");
+			}
+			return;
+		}
+
+		if (args[1] == "-define") {
+			if (use_verific) {
+				args[0] = "verific";
+				args[1] = "-vlog-define";
+				Pass::call(design, args);
+			}
+			args[0] = "verilog_defines";
+			args.erase(args.begin()+1, args.begin()+2);
+			for (int i = 1; i < GetSize(args); i++)
+				args[i] = "-D" + args[i];
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-undef") {
+			if (use_verific) {
+				args[0] = "verific";
+				args[1] = "-vlog-undef";
+				Pass::call(design, args);
+			}
+			args[0] = "verilog_defines";
+			args.erase(args.begin()+1, args.begin()+2);
+			for (int i = 1; i < GetSize(args); i++)
+				args[i] = "-U" + args[i];
+			Pass::call(design, args);
+			return;
+		}
+
+		log_cmd_error("Missing or unsupported mode parameter.\n");
+	}
+} ReadPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 2dd688e0d..cbd9314db 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -25,6 +25,9 @@ YOSYS_NAMESPACE_BEGIN
 
 extern int verific_verbose;
 
+extern bool verific_import_pending;
+extern void verific_import(Design *design, std::string top = std::string());
+
 extern pool<int> verific_sva_prims;
 
 struct VerificImporter;
@@ -40,6 +43,7 @@ struct VerificClocking {
 	SigBit enable_sig = State::S1;
 	SigBit disable_sig = State::S0;
 	bool posedge = true;
+	bool gclk = false;
 
 	VerificClocking() { }
 	VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
@@ -65,6 +69,7 @@ struct VerificImporter
 
 	std::map<Verific::Net*, RTLIL::SigBit> net_map;
 	std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
+	pool<Verific::Net*, hash_ptr_ops> any_all_nets;
 
 	bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
 	bool mode_autocover;
@@ -79,7 +84,7 @@ struct VerificImporter
 	RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
-	RTLIL::SigSpec operatorOutput(Verific::Instance *inst);
+	RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr);
 
 	bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
 	bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4ca..8e985c3a6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -980,7 +980,6 @@ struct VerificSvaImporter
 	bool mode_assume = false;
 	bool mode_cover = false;
 	bool mode_trigger = false;
-	bool eventually = false;
 
 	Instance *net_to_ast_driver(Net *n)
 	{
@@ -1487,6 +1486,70 @@ struct VerificSvaImporter
 			fsm.getFirstAcceptReject(accept_p, reject_p);
 	}
 
+	bool eventually_property(Net *&net, SigBit &trig)
+	{
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr)
+			return false;
+
+		if (clocking.cond_net != nullptr)
+			trig = importer->net_map_at(clocking.cond_net);
+		else
+			trig = State::S1;
+
+		if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
+		{
+			if (mode_cover || mode_trigger)
+				parser_error(inst);
+
+			net = inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			return true;
+		}
+
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			Net *antecedent_net = inst->GetInput1();
+			Net *consequent_net = inst->GetInput2();
+
+			Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+			if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) {
+				return false;
+			}
+
+			if (mode_cover || mode_trigger)
+				parser_error(consequent_inst);
+
+			int node;
+
+			SvaFsm antecedent_fsm(clocking, trig);
+			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
+			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
+				int next_node = antecedent_fsm.createNode();
+				antecedent_fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+			trig = antecedent_fsm.getAccept();
+			net = consequent_inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			if (verific_verbose) {
+				log("    Eventually Antecedent FSM:\n");
+				antecedent_fsm.dump();
+			}
+
+			return true;
+		}
+
+		return false;
+	}
+
 	void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
 	{
 		Instance *inst = net_to_ast_driver(net);
@@ -1620,10 +1683,46 @@ struct VerificSvaImporter
 			}
 			else
 			{
-				if (mode_assert || mode_assume) {
-					parse_property(clocking.body_net, nullptr, &reject_bit);
-				} else {
-					parse_property(clocking.body_net, &accept_bit, nullptr);
+				Net *net = clocking.body_net;
+				SigBit trig;
+
+				if (eventually_property(net, trig))
+				{
+					SigBit sig_a, sig_en = trig;
+					parse_property(net, &sig_a, nullptr);
+
+					// add final FF stage
+
+					SigBit sig_a_q, sig_en_q;
+
+					if (clocking.body_net == nullptr) {
+						sig_a_q = sig_a;
+						sig_en_q = sig_en;
+					} else {
+						sig_a_q = module->addWire(NEW_ID);
+						sig_en_q = module->addWire(NEW_ID);
+						clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+						clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+					}
+
+					// generate fair/live cell
+
+					RTLIL::Cell *c = nullptr;
+
+					if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
+					if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
+
+					importer->import_attributes(c->attributes, root);
+
+					return;
+				}
+				else
+				{
+					if (mode_assert || mode_assume) {
+						parse_property(net, nullptr, &reject_bit);
+					} else {
+						parse_property(net, &accept_bit, nullptr);
+					}
 				}
 			}
 
diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index c43ff4e3a..dea22ee8a 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -183,8 +183,9 @@ static std::string next_token(bool pass_newline = false)
 		const char *ok = "abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ$0123456789";
 		if (ch == '`' || strchr(ok, ch) != NULL)
 		{
+			char first = ch;
 			ch = next_char();
-			if (ch == '"') {
+			if (first == '`' && (ch == '"' || ch == '`')) {
 				token += ch;
 			} else do {
 					if (strchr(ok, ch) == NULL) {
@@ -244,6 +245,7 @@ static bool try_expand_macro(std::set<std::string> &defines_with_args,
 				args.push_back(std::string());
 				while (1)
 				{
+					skip_spaces();
 					tok = next_token(true);
 					if (tok == ")" || tok == "}" || tok == "]")
 						level--;
@@ -264,6 +266,9 @@ static bool try_expand_macro(std::set<std::string> &defines_with_args,
 			}
 			insert_input(defines_map[name]);
 			return true;
+	} else if (tok == "``") {
+		// Swallow `` in macro expansion
+		return true;
 	} else return false;
 }
 
diff --git a/kernel/driver.cc b/kernel/driver.cc
index bec872c24..178641101 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -85,20 +85,37 @@ USING_YOSYS_NAMESPACE
 #ifdef EMSCRIPTEN
 #  include <sys/stat.h>
 #  include <sys/types.h>
+#  include <emscripten.h>
 
 extern "C" int main(int, char**);
 extern "C" void run(const char*);
 extern "C" const char *errmsg();
 extern "C" const char *prompt();
 
-int main(int, char**)
+int main(int argc, char **argv)
 {
+	EM_ASM(
+		if (ENVIRONMENT_IS_NODE)
+		{
+			FS.mkdir('/hostcwd');
+			FS.mount(NODEFS, { root: '.' }, '/hostcwd');
+			FS.mkdir('/hostfs');
+			FS.mount(NODEFS, { root: '/' }, '/hostfs');
+		}
+	);
+
 	mkdir("/work", 0777);
 	chdir("/work");
 	log_files.push_back(stdout);
 	log_error_stderr = true;
 	yosys_banner();
 	yosys_setup();
+
+	if (argc == 2)
+	{
+		// Run the first argument as a script file
+		run_frontend(argv[1], "script", 0, 0, 0);
+	}
 }
 
 void run(const char *command)
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index aa5901271..750a154e6 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -739,7 +739,7 @@ std::string proc_self_dirname()
 #ifdef EMSCRIPTEN
 std::string proc_share_dirname()
 {
-	return "/share";
+	return "/share/";
 }
 #else
 std::string proc_share_dirname()
diff --git a/misc/yosys.proto b/misc/yosys.proto
new file mode 100644
index 000000000..2870176cb
--- /dev/null
+++ b/misc/yosys.proto
@@ -0,0 +1,175 @@
+//
+// yosys -- Yosys Open SYnthesis Suite
+// 
+// Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
+// 
+// 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.
+//
+
+/// Protobuf definition of Yosys RTLIL dump/restore format for RTL designs.
+
+syntax = "proto3";
+
+package yosys.pb;
+
+// Port direction.
+enum Direction {
+    DIRECTION_INVALID = 0;
+    DIRECTION_INPUT = 1;
+    DIRECTION_OUTPUT = 2;
+    DIRECTION_INOUT = 3;
+}
+
+// A freeform parameter/attribute value.
+message Parameter {
+    oneof value {
+        int64 int = 1;
+        string str = 2;
+    }
+}
+
+// A signal in the design - either a unique identifier for one, or a constant
+// driver (low or high).
+message Signal {
+    // A constant signal driver in the design.
+    enum ConstantDriver {
+        CONSTANT_DRIVER_INVALID = 0;
+        CONSTANT_DRIVER_LOW = 1;
+        CONSTANT_DRIVER_HIGH = 2;
+        CONSTANT_DRIVER_Z = 3;
+        CONSTANT_DRIVER_X = 4;
+    }
+    oneof type {
+        // Signal uniquely identified by ID number.
+        int64 id = 1;
+        // Constant driver.
+        ConstantDriver constant = 2;
+    }
+}
+
+// A vector of signals.
+message BitVector {
+    repeated Signal signal = 1;
+}
+
+// A netlist module.
+message Module {
+    // Freeform attributes.
+    map<string, Parameter> attribute = 1;
+
+    // Named ports in this module.
+    message Port {
+        Direction direction = 1;
+        BitVector bits = 2;
+    }
+    map<string, Port> port = 2;
+    
+    // Named cells in this module.
+    message Cell {
+        // Set to true when the name of this cell is automatically created and
+        // likely not of interest for a regular user.
+        bool hide_name = 1;
+        string type = 2;
+        // Set if this module has an AIG model available.
+        string model = 3;
+        // Freeform parameters.
+        map<string, Parameter> parameter = 4;
+        // Freeform attributes.
+        map<string, Parameter> attribute = 5;
+
+        /// Ports of the cell.
+        // Direction of the port, if interface is known.
+        map<string, Direction> port_direction = 6;
+        // Connection of named port to signal(s).
+        map<string, BitVector> connection = 7;
+    }
+    map<string, Cell> cell = 3;
+
+    // Nets in this module.
+    message Netname {
+        // Set to true when the name of this net is automatically created and
+        // likely not of interest for a regular user.
+        bool hide_name = 1;
+        // Signal(s) that make up this net.
+        BitVector bits = 2;
+        // Freeform attributes.
+        map<string, Parameter> attributes = 3;
+    }
+    repeated Netname netname = 4;
+}
+
+// And-Inverter-Graph model.
+message Model {
+    message Node {
+        // Type of AIG node - or, what its' value is.
+        enum Type {
+            TYPE_INVALID = 0;
+            // The node's value is the value of the specified input port bit.
+            TYPE_PORT = 1;
+            // The node's value is the inverted value of the specified input
+            // port bit.
+            TYPE_NPORT = 2;
+            // The node's value is the ANDed value of specified nodes.
+            TYPE_AND = 3;
+            // The node's value is the NANDed value of specified nodes.
+            TYPE_NAND = 4;
+            // The node's value is a constant 1.
+            TYPE_TRUE = 5;
+            // The node's value is a constant 0.
+            TYPE_FALSE = 6;
+        };
+        Type type = 1;
+    
+        message Port {
+            // Name of port.
+            string portname = 1;
+            // Bit index in port.
+            int64 bitindex = 2;
+        }
+        message Gate {
+            // Node index of left side of operation.
+            int64 left = 1;
+            // Node index of right side of operation.
+            int64 right = 2;
+        }
+        oneof node {
+            // Set for PORT, NPORT
+            Port port = 2;
+            // Set for AND, NAND.
+            Gate gate = 3;
+        }
+    
+        // Set when the node drives given output port(s).
+        message OutPort {
+            // Name of port.
+            string name = 1;
+            // Bit index in port.
+            int64 bit_index = 2;
+        }
+        repeated OutPort out_port = 4;
+    }
+
+    // List of  AIG nodes - each is explicitely numbered by its' index in this
+    // array.
+    repeated Node node = 1;
+}
+
+// A Yosys design netlist dumped from RTLIL.
+message Design {
+    // Human-readable freeform 'remark' string.
+    string creator = 1;
+    // List of named modules in design.
+    map<string, Module> modules = 2;
+    // List of named AIG models in design (if AIG export enabled).
+    map<string, Model> models = 3;
+}
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index c67953976..1cd942796 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -23,6 +23,13 @@
 #include "kernel/rtlil.h"
 #include "kernel/log.h"
 
+#define MODE_ZERO     0
+#define MODE_ONE      1
+#define MODE_UNDEF    2
+#define MODE_RANDOM   3
+#define MODE_ANYSEQ   4
+#define MODE_ANYCONST 5
+
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
@@ -97,30 +104,32 @@ struct SetundefWorker
 
 	RTLIL::State next_bit()
 	{
-		if (next_bit_mode == 0)
+		if (next_bit_mode == MODE_ZERO)
 			return RTLIL::State::S0;
 
-		if (next_bit_mode == 1)
+		if (next_bit_mode == MODE_ONE)
 			return RTLIL::State::S1;
 
-		if (next_bit_mode == 2)
-			log_abort();
-
-		if (next_bit_mode == 4)
+		if (next_bit_mode == MODE_UNDEF)
 			return RTLIL::State::Sx;
 
-		// xorshift32
-		next_bit_state ^= next_bit_state << 13;
-		next_bit_state ^= next_bit_state >> 17;
-		next_bit_state ^= next_bit_state << 5;
-		log_assert(next_bit_state != 0);
+		if (next_bit_mode == MODE_RANDOM)
+		{
+			// xorshift32
+			next_bit_state ^= next_bit_state << 13;
+			next_bit_state ^= next_bit_state >> 17;
+			next_bit_state ^= next_bit_state << 5;
+			log_assert(next_bit_state != 0);
+
+			return ((next_bit_state >> (next_bit_state & 15)) & 16) ? RTLIL::State::S0 : RTLIL::State::S1;
+		}
 
-		return ((next_bit_state >> (next_bit_state & 15)) & 16) ? RTLIL::State::S0 : RTLIL::State::S1;
+		log_abort();
 	}
 
 	void operator()(RTLIL::SigSpec &sig)
 	{
-		if (next_bit_mode == 2) {
+		if (next_bit_mode == MODE_ANYSEQ || next_bit_mode == MODE_ANYCONST) {
 			siglist.push_back(&sig);
 			return;
 		}
@@ -145,7 +154,7 @@ struct SetundefPass : public Pass {
 		log("        also set undriven nets to constant values\n");
 		log("\n");
 		log("    -expose\n");
-		log("        also expose undriven nets as inputs\n");
+		log("        also expose undriven nets as inputs (use with -undriven)\n");
 		log("\n");
 		log("    -zero\n");
 		log("        replace with bits cleared (0)\n");
@@ -159,6 +168,9 @@ struct SetundefPass : public Pass {
 		log("    -anyseq\n");
 		log("        replace with $anyseq drivers (for formal)\n");
 		log("\n");
+		log("    -anyconst\n");
+		log("        replace with $anyconst drivers (for formal)\n");
+		log("\n");
 		log("    -random <seed>\n");
 		log("        replace with random bits using the specified integer als seed\n");
 		log("        value for the random number generator.\n");
@@ -191,25 +203,31 @@ struct SetundefPass : public Pass {
 			}
 			if (args[argidx] == "-zero") {
 				got_value = true;
-				worker.next_bit_mode = 0;
+				worker.next_bit_mode = MODE_ZERO;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-one") {
 				got_value = true;
-				worker.next_bit_mode = 1;
+				worker.next_bit_mode = MODE_ONE;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-anyseq") {
 				got_value = true;
-				worker.next_bit_mode = 2;
+				worker.next_bit_mode = MODE_ANYSEQ;
+				worker.next_bit_state = 0;
+				continue;
+			}
+			if (args[argidx] == "-anyconst") {
+				got_value = true;
+				worker.next_bit_mode = MODE_ANYCONST;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-undef") {
 				got_value = true;
-				worker.next_bit_mode = 4;
+				worker.next_bit_mode = MODE_UNDEF;
 				worker.next_bit_state = 0;
 				continue;
 			}
@@ -219,7 +237,7 @@ struct SetundefPass : public Pass {
 			}
 			if (args[argidx] == "-random" && !got_value && argidx+1 < args.size()) {
 				got_value = true;
-				worker.next_bit_mode = 3;
+				worker.next_bit_mode = MODE_RANDOM;
 				worker.next_bit_state = atoi(args[++argidx].c_str()) + 1;
 				for (int i = 0; i < 10; i++)
 					worker.next_bit();
@@ -232,7 +250,10 @@ struct SetundefPass : public Pass {
 		if (expose_mode && !undriven_mode)
 			log_cmd_error("Option -expose must be used with option -undriven.\n");
 		if (!got_value)
-			log_cmd_error("One of the options -zero, -one, -anyseq, or -random <seed> must be specified.\n");
+			log_cmd_error("One of the options -zero, -one, -anyseq, -anyconst, or -random <seed> must be specified.\n");
+
+		if (init_mode && (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST))
+			log_cmd_error("The options -init and -anyseq / -anyconst are exclusive.\n");
 
 		for (auto module : design->selected_modules())
 		{
@@ -419,7 +440,7 @@ struct SetundefPass : public Pass {
 
 			module->rewrite_sigspecs(worker);
 
-			if (worker.next_bit_mode == 2)
+			if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
 			{
 				vector<SigSpec*> siglist;
 				siglist.swap(worker.siglist);
@@ -436,7 +457,10 @@ struct SetundefPass : public Pass {
 							width++;
 
 						if (width > 0) {
-							sig.replace(cursor, module->Anyseq(NEW_ID, width));
+							if (worker.next_bit_mode == MODE_ANYSEQ)
+								sig.replace(cursor, module->Anyseq(NEW_ID, width));
+							else
+								sig.replace(cursor, module->Anyconst(NEW_ID, width));
 							cursor += width;
 						} else {
 							cursor++;
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index e52a192db..f1d958a1a 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -142,7 +142,7 @@ struct statdata_t
 		}
 	}
 
-	void log_data()
+	void log_data(RTLIL::IdString mod_name, bool top_mod)
 	{
 		log("   Number of wires:             %6d\n", num_wires);
 		log("   Number of wire bits:         %6d\n", num_wire_bits);
@@ -163,7 +163,7 @@ struct statdata_t
 
 		if (area != 0) {
 			log("\n");
-			log("   Chip area for this module: %f\n", area);
+			log("   Chip area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), area);
 		}
 	}
 };
@@ -275,7 +275,7 @@ struct StatPass : public Pass {
 			log("\n");
 			log("=== %s%s ===\n", RTLIL::id2cstr(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)");
 			log("\n");
-			data.log_data();
+			data.log_data(mod->name, false);
 		}
 
 		if (top_mod != NULL && GetSize(mod_stat) > 1)
@@ -288,7 +288,7 @@ struct StatPass : public Pass {
 			statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0);
 
 			log("\n");
-			data.log_data();
+			data.log_data(top_mod->name, true);
 		}
 
 		log("\n");
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 18dfa7184..e61851481 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -18,6 +18,7 @@
  */
 
 #include "kernel/yosys.h"
+#include "frontends/verific/verific.h"
 #include <stdlib.h>
 #include <stdio.h>
 #include <set>
@@ -258,7 +259,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 			if (mod->wires_.count(portname) == 0)
 				log_error("Array cell `%s.%s' connects to unknown port `%s'.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name), RTLIL::id2cstr(conn.first));
 			int port_size = mod->wires_.at(portname)->width;
-			if (conn_size == port_size)
+			if (conn_size == port_size || conn_size == 0)
 				continue;
 			if (conn_size != port_size*num)
 				log_error("Array cell `%s.%s' has invalid port vs. signal size for port `%s'.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name), RTLIL::id2cstr(conn.first));
@@ -421,6 +422,7 @@ struct HierarchyPass : public Pass {
 		bool flag_simcheck = false;
 		bool purge_lib = false;
 		RTLIL::Module *top_mod = NULL;
+		std::string load_top_mod;
 		std::vector<std::string> libdirs;
 
 		bool auto_top_mode = false;
@@ -511,7 +513,7 @@ struct HierarchyPass : public Pass {
 					top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
 				}
 				if (top_mod == NULL)
-					log_cmd_error("Module `%s' not found!\n", args[argidx].c_str());
+					load_top_mod = args[argidx];
 				continue;
 			}
 			if (args[argidx] == "-auto-top") {
@@ -522,6 +524,22 @@ struct HierarchyPass : public Pass {
 		}
 		extra_args(args, argidx, design, false);
 
+		if (!load_top_mod.empty()) {
+#ifdef YOSYS_ENABLE_VERIFIC
+			if (verific_import_pending) {
+				verific_import(design, load_top_mod);
+				top_mod = design->module(RTLIL::escape_id(load_top_mod));
+			}
+#endif
+			if (top_mod == NULL)
+				log_cmd_error("Module `%s' not found!\n", load_top_mod.c_str());
+		} else {
+#ifdef YOSYS_ENABLE_VERIFIC
+			if (verific_import_pending)
+				verific_import(design);
+#endif
+		}
+
 		if (generate_mode) {
 			generate(design, generate_cells, generate_ports);
 			return;
diff --git a/passes/memory/memory_dff.cc b/passes/memory/memory_dff.cc
index 40691d160..6e036397d 100644
--- a/passes/memory/memory_dff.cc
+++ b/passes/memory/memory_dff.cc
@@ -33,8 +33,20 @@ struct MemoryDffWorker
 	dict<SigBit, int> sigbit_users_count;
 	dict<SigSpec, Cell*> mux_cells_a, mux_cells_b;
 	pool<Cell*> forward_merged_dffs, candidate_dffs;
+	pool<SigBit> init_bits;
 
-	MemoryDffWorker(Module *module) : module(module), sigmap(module) { }
+	MemoryDffWorker(Module *module) : module(module), sigmap(module)
+	{
+		for (auto wire : module->wires()) {
+			if (wire->attributes.count("\\init") == 0)
+				continue;
+			SigSpec sig = sigmap(wire);
+			Const initval = wire->attributes.count("\\init");
+			for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
+				if (initval[i] == State::S0 || initval[i] == State::S1)
+					init_bits.insert(sig[i]);
+		}
+	}
 
 	bool find_sig_before_dff(RTLIL::SigSpec &sig, RTLIL::SigSpec &clk, bool &clk_polarity, bool after = false)
 	{
@@ -45,6 +57,9 @@ struct MemoryDffWorker
 			if (bit.wire == NULL)
 				continue;
 
+			if (!after && init_bits.count(sigmap(bit)))
+				return false;
+
 			for (auto cell : dff_cells)
 			{
 				if (after && forward_merged_dffs.count(cell))
@@ -72,6 +87,9 @@ struct MemoryDffWorker
 				if (d.size() != 1)
 					continue;
 
+				if (after && init_bits.count(d))
+					return false;
+
 				bit = d;
 				clk = this_clk;
 				clk_polarity = this_clk_polarity;
diff --git a/passes/memory/memory_nordff.cc b/passes/memory/memory_nordff.cc
index 5f87e8b79..87ab7c623 100644
--- a/passes/memory/memory_nordff.cc
+++ b/passes/memory/memory_nordff.cc
@@ -61,49 +61,59 @@ struct MemoryNordffPass : public Pass {
 
 			SigSpec rd_addr = cell->getPort("\\RD_ADDR");
 			SigSpec rd_data = cell->getPort("\\RD_DATA");
+			SigSpec rd_clk = cell->getPort("\\RD_CLK");
+			SigSpec rd_en = cell->getPort("\\RD_EN");
 			Const rd_clk_enable = cell->getParam("\\RD_CLK_ENABLE");
+			Const rd_clk_polarity = cell->getParam("\\RD_CLK_POLARITY");
 
 			for (int i = 0; i < rd_ports; i++)
 			{
 				bool clk_enable = rd_clk_enable[i] == State::S1;
 
-				if (!clk_enable)
-					continue;
+				if (clk_enable)
+				{
+					bool clk_polarity = cell->getParam("\\RD_CLK_POLARITY")[i] == State::S1;
+					bool transparent = cell->getParam("\\RD_TRANSPARENT")[i] == State::S1;
 
-				bool clk_polarity = cell->getParam("\\RD_CLK_POLARITY")[i] == State::S1;
-				bool transparent = cell->getParam("\\RD_TRANSPARENT")[i] == State::S1;
+					SigSpec clk = cell->getPort("\\RD_CLK")[i] ;
+					SigSpec en = cell->getPort("\\RD_EN")[i];
+					Cell *c;
 
-				SigSpec clk = cell->getPort("\\RD_CLK")[i] ;
-				SigSpec en = cell->getPort("\\RD_EN")[i];
-				Cell *c;
+					if (transparent)
+					{
+						SigSpec sig_q = module->addWire(NEW_ID, abits);
+						SigSpec sig_d = rd_addr.extract(abits * i, abits);
+						rd_addr.replace(abits * i, sig_q);
+						if (en != State::S1)
+							sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
+						c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					}
+					else
+					{
+						SigSpec sig_d = module->addWire(NEW_ID, width);
+						SigSpec sig_q = rd_data.extract(width * i, width);
+						rd_data.replace(width *i, sig_d);
+						if (en != State::S1)
+							sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
+						c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					}
 
-				if (transparent)
-				{
-					SigSpec sig_q = module->addWire(NEW_ID, abits);
-					SigSpec sig_d = rd_addr.extract(abits * i, abits);
-					rd_addr.replace(abits * i, sig_q);
-					if (en != State::S1)
-						sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
-					c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
-				}
-				else
-				{
-					SigSpec sig_d = module->addWire(NEW_ID, width);
-					SigSpec sig_q = rd_data.extract(width * i, width);
-					rd_data.replace(width *i, sig_d);
-					if (en != State::S1)
-						sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
-					c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					log("Extracted %s FF from read port %d of %s.%s: %s\n", transparent ? "addr" : "data",
+							i, log_id(module), log_id(cell), log_id(c));
 				}
 
-				log("Extracted %s FF from read port %d of %s.%s: %s\n", transparent ? "addr" : "data",
-						i, log_id(module), log_id(cell), log_id(c));
+				rd_en[i] = State::S1;
+				rd_clk[i] = State::S0;
 				rd_clk_enable[i] = State::S0;
+				rd_clk_polarity[i] = State::S1;
 			}
 
 			cell->setPort("\\RD_ADDR", rd_addr);
 			cell->setPort("\\RD_DATA", rd_data);
+			cell->setPort("\\RD_CLK", rd_clk);
+			cell->setPort("\\RD_EN", rd_en);
 			cell->setParam("\\RD_CLK_ENABLE", rd_clk_enable);
+			cell->setParam("\\RD_CLK_POLARITY", rd_clk_polarity);
 		}
 	}
 } MemoryNordffPass;
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 009ba6b97..18868c6d7 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -60,6 +60,10 @@
 
 #include "frontends/blif/blifparse.h"
 
+#ifdef YOSYS_LINK_ABC
+extern "C" int Abc_RealMain(int argc, char *argv[]);
+#endif
+
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
@@ -546,11 +550,13 @@ std::string replace_tempdir(std::string text, std::string tempdir_name, bool sho
 	}
 
 	std::string  selfdir_name = proc_self_dirname();
-	while (1) {
-		size_t pos = text.find(selfdir_name);
-		if (pos == std::string::npos)
-			break;
-		text = text.substr(0, pos) + "<yosys-exe-dir>/" + text.substr(pos + GetSize(selfdir_name));
+	if (selfdir_name != "/") {
+		while (1) {
+			size_t pos = text.find(selfdir_name);
+			if (pos == std::string::npos)
+				break;
+			text = text.substr(0, pos) + "<yosys-exe-dir>/" + text.substr(pos + GetSize(selfdir_name));
+		}
 	}
 
 	return text;
@@ -943,8 +949,24 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 		buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
 		log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str());
 
+#ifndef YOSYS_LINK_ABC
 		abc_output_filter filt(tempdir_name, show_tempdir);
 		int ret = run_command(buffer, std::bind(&abc_output_filter::next_line, filt, std::placeholders::_1));
+#else
+		// These needs to be mutable, supposedly due to getopt
+		char *abc_argv[5];
+		string tmp_script_name = stringf("%s/abc.script", tempdir_name.c_str());
+		abc_argv[0] = strdup(exe_file.c_str());
+		abc_argv[1] = strdup("-s");
+		abc_argv[2] = strdup("-f");
+		abc_argv[3] = strdup(tmp_script_name.c_str());
+		abc_argv[4] = 0;
+		int ret = Abc_RealMain(4, abc_argv);
+		free(abc_argv[0]);
+		free(abc_argv[1]);
+		free(abc_argv[2]);
+		free(abc_argv[3]);
+#endif
 		if (ret != 0)
 			log_error("ABC: execution of command \"%s\" failed: return code %d.\n", buffer.c_str(), ret);
 
diff --git a/passes/techmap/deminout.cc b/passes/techmap/deminout.cc
index ed4e45762..0b8fd5246 100644
--- a/passes/techmap/deminout.cc
+++ b/passes/techmap/deminout.cc
@@ -57,7 +57,7 @@ struct DeminoutPass : public Pass {
 			for (auto module : design->selected_modules())
 			{
 				SigMap sigmap(module);
-				pool<SigBit> bits_written, bits_used, bits_inout;
+				pool<SigBit> bits_written, bits_used, bits_inout, bits_tribuf;
 				dict<SigBit, int> bits_numports;
 
 				for (auto wire : module->wires())
@@ -82,6 +82,25 @@ struct DeminoutPass : public Pass {
 					if (cellport_in)
 						for (auto bit : sigmap(conn.second))
 							bits_used.insert(bit);
+
+					if (conn.first == "\\Y" && cell->type.in("$mux", "$pmux", "$_MUX_", "$_TBUF_"))
+					{
+						bool tribuf = (cell->type == "$_TBUF_");
+
+						if (!tribuf) {
+							for (auto &c : cell->connections()) {
+								if (!c.first.in("\\A", "\\B"))
+									continue;
+								for (auto b : sigmap(c.second))
+									if (b == State::Sz)
+										tribuf = true;
+							}
+						}
+
+						if (tribuf)
+							for (auto bit : sigmap(conn.second))
+								bits_tribuf.insert(bit);
+					}
 				}
 
 				for (auto wire : module->selected_wires())
@@ -95,10 +114,15 @@ struct DeminoutPass : public Pass {
 							if (bits_numports[bit] > 1 || bits_inout.count(bit))
 								new_input = true, new_output = true;
 
-							if (bits_written.count(bit))
+							if (bits_written.count(bit)) {
 								new_output = true;
-							else if (bits_used.count(bit))
-								new_input = true;
+								if (bits_tribuf.count(bit))
+									goto tribuf_bit;
+							} else {
+						tribuf_bit:
+								if (bits_used.count(bit))
+									new_input = true;
+							}
 						}
 
 						if (new_input != new_output) {
diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc
index 4acbf7c0d..690ba87ed 100644
--- a/passes/techmap/iopadmap.cc
+++ b/passes/techmap/iopadmap.cc
@@ -146,11 +146,37 @@ struct IopadmapPass : public Pass {
 		for (auto module : design->selected_modules())
 		{
 			dict<IdString, pool<int>> skip_wires;
+			pool<SigBit> skip_wire_bits;
+			SigMap sigmap(module);
+
+			for (auto cell : module->cells())
+			{
+				if (cell->type == RTLIL::escape_id(inpad_celltype) && cell->hasPort(RTLIL::escape_id(inpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(inpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(outpad_celltype) && cell->hasPort(RTLIL::escape_id(outpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(outpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(inoutpad_celltype) && cell->hasPort(RTLIL::escape_id(inoutpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(inoutpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(toutpad_celltype) && cell->hasPort(RTLIL::escape_id(toutpad_portname3)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(toutpad_portname3))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(tinoutpad_celltype) && cell->hasPort(RTLIL::escape_id(tinoutpad_portname4)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(tinoutpad_portname4))))
+						skip_wire_bits.insert(bit);
+			}
 
 			if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty())
 			{
-				SigMap sigmap(module);
 				dict<SigBit, pair<IdString, pool<IdString>>> tbuf_bits;
+				pool<pair<IdString, IdString>> norewrites;
+				SigMap rewrites;
 
 				for (auto cell : module->cells())
 					if (cell->type == "$_TBUF_") {
@@ -177,6 +203,9 @@ struct IopadmapPass : public Pass {
 						if (tbuf_bits.count(mapped_wire_bit) == 0)
 							continue;
 
+						if (skip_wire_bits.count(mapped_wire_bit))
+							continue;
+
 						auto &tbuf_cache = tbuf_bits.at(mapped_wire_bit);
 						Cell *tbuf_cell = module->cell(tbuf_cache.first);
 
@@ -219,6 +248,9 @@ struct IopadmapPass : public Pass {
 
 							module->remove(tbuf_cell);
 							skip_wires[wire->name].insert(i);
+
+							norewrites.insert(make_pair(cell->name, RTLIL::escape_id(tinoutpad_portname4)));
+							rewrites.add(sigmap(wire_bit), owire);
 							continue;
 						}
 
@@ -256,6 +288,22 @@ struct IopadmapPass : public Pass {
 						}
 					}
 				}
+
+				if (GetSize(norewrites))
+				{
+					for (auto cell : module->cells())
+					for (auto port : cell->connections())
+					{
+						if (norewrites.count(make_pair(cell->name, port.first)))
+							continue;
+
+						SigSpec orig_sig = sigmap(port.second);
+						SigSpec new_sig = rewrites(orig_sig);
+
+						if (orig_sig != new_sig)
+							cell->setPort(port.first, new_sig);
+					}
+				}
 			}
 
 			for (auto wire : module->selected_wires())
@@ -272,6 +320,13 @@ struct IopadmapPass : public Pass {
 					skip_bit_indices = skip_wires.at(wire->name);
 				}
 
+				for (int i = 0; i < GetSize(wire); i++)
+					if (skip_wire_bits.count(sigmap(SigBit(wire, i))))
+						skip_bit_indices.insert(i);
+
+				if (GetSize(wire) == GetSize(skip_bit_indices))
+					continue;
+
 				if (wire->port_input && !wire->port_output) {
 					if (inpad_celltype.empty()) {
 						log("Don't map input port %s.%s: Missing option -inpad.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire->name));
diff --git a/techlibs/common/prep.cc b/techlibs/common/prep.cc
index 3dfc60383..cc977f97e 100644
--- a/techlibs/common/prep.cc
+++ b/techlibs/common/prep.cc
@@ -55,13 +55,14 @@ struct PrepPass : public ScriptPass
 		log("\n");
 		log("    -memx\n");
 		log("        simulate verilog simulation behavior for out-of-bounds memory accesses\n");
-		log("        using the 'memory_memx' pass. This option implies -nordff.\n");
+		log("        using the 'memory_memx' pass.\n");
 		log("\n");
 		log("    -nomem\n");
 		log("        do not run any of the memory_* passes\n");
 		log("\n");
-		log("    -nordff\n");
-		log("        passed to 'memory_dff'. prohibits merging of FFs into memory read ports\n");
+		log("    -rdff\n");
+		log("        do not pass -nordff to 'memory_dff'. This enables merging of FFs into\n");
+		log("        memory read ports.\n");
 		log("\n");
 		log("    -nokeepdc\n");
 		log("        do not call opt_* with -keepdc\n");
@@ -77,13 +78,12 @@ struct PrepPass : public ScriptPass
 		log("\n");
 	}
 
-	string top_module, fsm_opts, memory_opts;
-	bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc;
+	string top_module, fsm_opts;
+	bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc, nordff;
 
 	virtual void clear_flags() YS_OVERRIDE
 	{
 		top_module.clear();
-		memory_opts.clear();
 
 		autotop = false;
 		flatten = false;
@@ -91,6 +91,7 @@ struct PrepPass : public ScriptPass
 		memxmode = false;
 		nomemmode = false;
 		nokeepdc = false;
+		nordff = true;
 	}
 
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -129,7 +130,6 @@ struct PrepPass : public ScriptPass
 			}
 			if (args[argidx] == "-memx") {
 				memxmode = true;
-				memory_opts += " -nordff";
 				continue;
 			}
 			if (args[argidx] == "-nomem") {
@@ -137,7 +137,11 @@ struct PrepPass : public ScriptPass
 				continue;
 			}
 			if (args[argidx] == "-nordff") {
-				memory_opts += " -nordff";
+				nordff = true;
+				continue;
+			}
+			if (args[argidx] == "-rdff") {
+				nordff = false;
 				continue;
 			}
 			if (args[argidx] == "-nokeepdc") {
@@ -196,7 +200,7 @@ struct PrepPass : public ScriptPass
 					run(memxmode ? "wreduce -memx" : "wreduce");
 			}
 			if (!nomemmode) {
-				run("memory_dff" + (help_mode ? " [-nordff]" : memory_opts));
+				run(string("memory_dff") + (help_mode ? " [-nordff]" : nordff ? " -nordff" : ""));
 				if (help_mode || memxmode)
 					run("memory_memx", "(if -memx)");
 				run("opt_clean");
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index 814895e70..45a02111f 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -1,6 +1,6 @@
 
-`define SB_DFF_REG reg Q = 0;
-// `define SB_DFF_REG reg Q;
+`define SB_DFF_REG reg Q = 0
+// `define SB_DFF_REG reg Q
 
 // SiliconBlue IO Cells
 
@@ -132,21 +132,18 @@ endmodule
 
 // Positive Edge SiliconBlue FF Cells
 
-module SB_DFF (output Q, input C, D);
-	`SB_DFF_REG
+module SB_DFF (output `SB_DFF_REG, input C, D);
 	always @(posedge C)
 		Q <= D;
 endmodule
 
-module SB_DFFE (output Q, input C, E, D);
-	`SB_DFF_REG
+module SB_DFFE (output `SB_DFF_REG, input C, E, D);
 	always @(posedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-module SB_DFFSR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFSR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C)
 		if (R)
 			Q <= 0;
@@ -154,8 +151,7 @@ module SB_DFFSR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -163,8 +159,7 @@ module SB_DFFR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFSS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFSS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C)
 		if (S)
 			Q <= 1;
@@ -172,8 +167,7 @@ module SB_DFFSS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -181,8 +175,7 @@ module SB_DFFS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFESR (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C)
 		if (E) begin
 			if (R)
@@ -192,8 +185,7 @@ module SB_DFFESR (output Q, input C, E, R, D);
 		end
 endmodule
 
-module SB_DFFER (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFER (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -201,8 +193,7 @@ module SB_DFFER (output Q, input C, E, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFESS (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C)
 		if (E) begin
 			if (S)
@@ -212,8 +203,7 @@ module SB_DFFESS (output Q, input C, E, S, D);
 		end
 endmodule
 
-module SB_DFFES (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFES (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -223,21 +213,18 @@ endmodule
 
 // Negative Edge SiliconBlue FF Cells
 
-module SB_DFFN (output Q, input C, D);
-	`SB_DFF_REG
+module SB_DFFN (output `SB_DFF_REG, input C, D);
 	always @(negedge C)
 		Q <= D;
 endmodule
 
-module SB_DFFNE (output Q, input C, E, D);
-	`SB_DFF_REG
+module SB_DFFNE (output `SB_DFF_REG, input C, E, D);
 	always @(negedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-module SB_DFFNSR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFNSR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C)
 		if (R)
 			Q <= 0;
@@ -245,8 +232,7 @@ module SB_DFFNSR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFNR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -254,8 +240,7 @@ module SB_DFFNR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNSS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFNSS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C)
 		if (S)
 			Q <= 1;
@@ -263,8 +248,7 @@ module SB_DFFNSS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFNS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -272,8 +256,7 @@ module SB_DFFNS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNESR (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFNESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C)
 		if (E) begin
 			if (R)
@@ -283,8 +266,7 @@ module SB_DFFNESR (output Q, input C, E, R, D);
 		end
 endmodule
 
-module SB_DFFNER (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFNER (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -292,8 +274,7 @@ module SB_DFFNER (output Q, input C, E, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNESS (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFNESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C)
 		if (E) begin
 			if (S)
@@ -303,8 +284,7 @@ module SB_DFFNESS (output Q, input C, E, S, D);
 		end
 endmodule
 
-module SB_DFFNES (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFNES (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -677,7 +657,7 @@ module ICESTORM_LC (
 	parameter [0:0] SET_NORESET  = 0;
 	parameter [0:0] ASYNC_SR     = 0;
 
-	wire COUT = CARRY_ENABLE ? (I1 && I2) || ((I1 || I2) && CIN) : 1'bx;
+	assign COUT = CARRY_ENABLE ? (I1 && I2) || ((I1 || I2) && CIN) : 1'bx;
 
 	wire [7:0] lut_s3 = I3 ? LUT_INIT[15:8] : LUT_INIT[7:0];
 	wire [3:0] lut_s2 = I2 ?   lut_s3[ 7:4] :   lut_s3[3:0];
diff --git a/techlibs/ice40/ice40_opt.cc b/techlibs/ice40/ice40_opt.cc
index ae72f5d64..7af60f297 100644
--- a/techlibs/ice40/ice40_opt.cc
+++ b/techlibs/ice40/ice40_opt.cc
@@ -26,6 +26,13 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static SigBit get_bit_or_zero(const SigSpec &sig)
+{
+	if (GetSize(sig) == 0)
+		return State::S0;
+	return sig[0];
+}
+
 static void run_ice40_opts(Module *module, bool unlut_mode)
 {
 	pool<SigBit> optimized_co;
@@ -45,7 +52,11 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 			SigSpec non_const_inputs, replacement_output;
 			int count_zeros = 0, count_ones = 0;
 
-			SigBit inbit[3] = {cell->getPort("\\I0"), cell->getPort("\\I1"), cell->getPort("\\CI")};
+			SigBit inbit[3] = {
+				get_bit_or_zero(cell->getPort("\\I0")),
+				get_bit_or_zero(cell->getPort("\\I1")),
+				get_bit_or_zero(cell->getPort("\\CI"))
+			};
 			for (int i = 0; i < 3; i++)
 				if (inbit[i].wire == nullptr) {
 					if (inbit[i] == State::S1)
@@ -63,8 +74,8 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 				replacement_output = non_const_inputs;
 
 			if (GetSize(replacement_output)) {
-				optimized_co.insert(sigmap(cell->getPort("\\CO")));
-				module->connect(cell->getPort("\\CO"), replacement_output);
+				optimized_co.insert(sigmap(cell->getPort("\\CO")[0]));
+				module->connect(cell->getPort("\\CO")[0], replacement_output);
 				module->design->scratchpad_set_bool("opt.did_something", true);
 				log("Optimized away SB_CARRY cell %s.%s: CO=%s\n",
 						log_id(module), log_id(cell), log_signal(replacement_output));
@@ -78,10 +89,10 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 	{
 		SigSpec inbits;
 
-		inbits.append(cell->getPort("\\I0"));
-		inbits.append(cell->getPort("\\I1"));
-		inbits.append(cell->getPort("\\I2"));
-		inbits.append(cell->getPort("\\I3"));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I0")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I1")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I2")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I3")));
 		sigmap.apply(inbits);
 
 		if (unlut_mode)
@@ -104,8 +115,13 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 		cell->setParam("\\LUT", cell->getParam("\\LUT_INIT"));
 		cell->unsetParam("\\LUT_INIT");
 
-		cell->setPort("\\A", SigSpec({cell->getPort("\\I3"), cell->getPort("\\I2"), cell->getPort("\\I1"), cell->getPort("\\I0")}));
-		cell->setPort("\\Y", cell->getPort("\\O"));
+		cell->setPort("\\A", SigSpec({
+			get_bit_or_zero(cell->getPort("\\I3")),
+			get_bit_or_zero(cell->getPort("\\I2")),
+			get_bit_or_zero(cell->getPort("\\I1")),
+			get_bit_or_zero(cell->getPort("\\I0"))
+		}));
+		cell->setPort("\\Y", cell->getPort("\\O")[0]);
 		cell->unsetPort("\\I0");
 		cell->unsetPort("\\I1");
 		cell->unsetPort("\\I2");
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 177581d53..abd890a56 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -45,7 +45,11 @@ struct SynthIce40Pass : public ScriptPass
 		log("        is omitted if this parameter is not specified.\n");
 		log("\n");
 		log("    -edif <file>\n");
-		log("        write the design to the specified edif file. writing of an output file\n");
+		log("        write the design to the specified EDIF file. writing of an output file\n");
+		log("        is omitted if this parameter is not specified.\n");
+		log("\n");
+		log("    -json <file>\n");
+		log("        write the design to the specified JSON file. writing of an output file\n");
 		log("        is omitted if this parameter is not specified.\n");
 		log("\n");
 		log("    -run <from_label>:<to_label>\n");
@@ -81,7 +85,7 @@ struct SynthIce40Pass : public ScriptPass
 		log("\n");
 	}
 
-	string top_opt, blif_file, edif_file;
+	string top_opt, blif_file, edif_file, json_file;
 	bool nocarry, nodffe, nobram, flatten, retime, abc2, vpr;
 
 	virtual void clear_flags() YS_OVERRIDE
@@ -89,6 +93,7 @@ struct SynthIce40Pass : public ScriptPass
 		top_opt = "-auto-top";
 		blif_file = "";
 		edif_file = "";
+		json_file = "";
 		nocarry = false;
 		nodffe = false;
 		nobram = false;
@@ -118,6 +123,10 @@ struct SynthIce40Pass : public ScriptPass
 				edif_file = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-json" && argidx+1 < args.size()) {
+				json_file = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-run" && argidx+1 < args.size()) {
 				size_t pos = args[argidx+1].find(':');
 				if (pos == std::string::npos)
@@ -260,17 +269,15 @@ struct SynthIce40Pass : public ScriptPass
 			if (!blif_file.empty() || help_mode) {
 				if (vpr || help_mode) {
 					run(stringf("opt_clean -purge"),
-						"                                        "
-						" (vpr mode)");
+							"                                 (vpr mode)");
 					run(stringf("write_blif -attr -cname -conn -param %s",
-								help_mode ? "<file-name>" : blif_file.c_str()),
-						" (vpr mode)");
+							help_mode ? "<file-name>" : blif_file.c_str()),
+							" (vpr mode)");
 				}
 				if (!vpr)
 					run(stringf("write_blif -gates -attr -param %s",
-								help_mode ? "<file-name>" : blif_file.c_str()),
-						"              "
-						" (non-vpr mode)");
+							help_mode ? "<file-name>" : blif_file.c_str()),
+							"       (non-vpr mode)");
 			}
 		}
 
@@ -279,6 +286,12 @@ struct SynthIce40Pass : public ScriptPass
 			if (!edif_file.empty() || help_mode)
 				run(stringf("write_edif %s", help_mode ? "<file-name>" : edif_file.c_str()));
 		}
+
+		if (check_label("json"))
+		{
+			if (!json_file.empty() || help_mode)
+				run(stringf("write_json %s", help_mode ? "<file-name>" : json_file.c_str()));
+		}
 	}
 } SynthIce40Pass;
 
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 31a6ae8ab..d6216244f 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -100,7 +100,7 @@ do
 		echo -n "Test: $bn "
 	fi
 
-	rm -f ${bn}.{err,log,sikp}
+	rm -f ${bn}.{err,log,skip}
 	mkdir -p ${bn}.out
 	rm -rf ${bn}.out/*