Merge branch 'next'

9 files changed, 3646 insertions, 305 deletions

diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc
index 68ef9aed..972f4f9f 100644
--- a/frontends/verific/Makefile.inc
+++ b/frontends/verific/Makefile.inc
@@ -3,6 +3,8 @@ OBJS += frontends/verific/verific.o
 
 ifeq ($(ENABLE_VERIFIC),1)
 
+OBJS += frontends/verific/verificsva.o
+
 EXTRA_TARGETS += share/verific
 
 share/verific:
@@ -11,6 +13,7 @@ share/verific:
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1987/. share/verific.new/vhdl_vdbs_1987
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_1993/. share/verific.new/vhdl_vdbs_1993
 	$(Q) cp -r $(VERIFIC_DIR)/vhdl_packages/vdbs_2008/. share/verific.new/vhdl_vdbs_2008
+	$(Q) chmod -R a+rX share/verific.new
 	$(Q) mv share/verific.new share/verific
 
 endif
diff --git a/frontends/verific/README b/frontends/verific/README
new file mode 100644
index 00000000..b4c436a3
--- /dev/null
+++ b/frontends/verific/README
@@ -0,0 +1,62 @@
+
+
+This directory contains Verific bindings for Yosys.
+See http://www.verific.com/ for details.
+
+
+Building Yosys with the 32 bit Verific eval library on amd64:
+=============================================================
+
+1.) Use a Makefile.conf like the following one:
+
+--snip--
+CONFIG := gcc
+ENABLE_TCL := 0
+ENABLE_PLUGINS := 0
+ENABLE_VERIFIC := 1
+CXXFLAGS += -m32
+LDFLAGS += -m32
+VERIFIC_DIR = /usr/local/src/verific_lib_eval
+--snap--
+
+
+2.) Install the necessary multilib packages
+
+Hint: On debian/ubuntu the multilib packages have names such as
+libreadline-dev:i386 or lib32readline6-dev, depending on the
+exact version of debian/ubuntu you are working with.
+
+
+3.) Build and test
+
+make -j8
+./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top'
+
+
+Verific Features that should be enabled in your Verific library
+===============================================================
+
+database/DBCompileFlags.h:
+	DB_PRESERVE_INITIAL_VALUE
+
+
+Testing Verific+Yosys+SymbiYosys for formal verification
+========================================================
+
+Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions:
+http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing
+
+Then run in the following command in this directory:
+
+	sby -f example.sby
+
+This will generate approximately one page of text outpout. The last lines
+should be something like this:
+
+	SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
+	SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
+	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase
+	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction
+	SBY [example] summary: successful proof by k-induction.
+	SBY [example] DONE (PASS, rc=0)
+
diff --git a/frontends/verific/build_amd64.txt b/frontends/verific/build_amd64.txt
deleted file mode 100644
index d6952820..00000000
--- a/frontends/verific/build_amd64.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-
-Notes on building yosys with verific support on amd64 when you
-only have the i386 eval version of Verific:
-
-
-1.) Use a Makefile.conf like the following one:
-
---snip--
-CONFIG := clang
-ENABLE_TCL := 0
-ENABLE_PLUGINS := 0
-ENABLE_VERIFIC := 1
-CXXFLAGS += -m32
-LDFLAGS += -m32
-VERIFIC_DIR = /usr/local/src/verific_lib_eval
---snap--
-
-
-2.) Install the necessary multilib packages
-
-Hint: On debian/ubuntu the multilib packages have names such as
-libreadline-dev:i386 or lib32readline6-dev, depending on the
-exact version of debian/ubuntu you are working with.
-
-
-3.) Build and test
-
-make -j8
-./yosys frontends/verific/test_navre.ys
-
diff --git a/frontends/verific/example.sby b/frontends/verific/example.sby
new file mode 100644
index 00000000..ffbf33ca
--- /dev/null
+++ b/frontends/verific/example.sby
@@ -0,0 +1,16 @@
+# Simple SymbiYosys example job utilizing Verific
+
+[options]
+mode prove
+depth 10
+
+[engines]
+smtbmc yices
+
+[script]
+verific -sv example.sv
+verific -import top
+prep -top top
+
+[files]
+example.sv
diff --git a/frontends/verific/example.sv b/frontends/verific/example.sv
new file mode 100644
index 00000000..21a5d42c
--- /dev/null
+++ b/frontends/verific/example.sv
@@ -0,0 +1,18 @@
+module top (
+  input clk, rst,
+  output reg [3:0] cnt
+);
+  initial cnt = 0;
+
+  always @(posedge clk) begin
+    if (rst)
+      cnt <= 0;
+    else
+      cnt <= cnt + 4'd 1;
+  end
+
+  always @(posedge clk) begin
+    assume (cnt != 10);
+    assert (cnt != 15);
+  end
+endmodule
diff --git a/frontends/verific/test_navre.ys b/frontends/verific/test_navre.ys
deleted file mode 100644
index a56b725a..00000000
--- a/frontends/verific/test_navre.ys
+++ /dev/null
@@ -1,18 +0,0 @@
-verific -vlog2k ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
-verific -import softusb_navre
-
-memory softusb_navre
-flatten softusb_navre
-rename softusb_navre gate
-
-read_verilog ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
-cd softusb_navre; proc; opt; memory; opt; cd ..
-rename softusb_navre gold
-
-expose -dff -shared gold gate
-miter -equiv -ignore_gold_x -make_assert -make_outputs -make_outcmp gold gate miter
-
-cd miter
-flatten; opt -undriven
-sat -verify -maxsteps 5 -set-init-undef -set-def-inputs -prove-asserts -tempinduct-def \
-    -seq 1 -set-at 1 in_rst 1 # -show-inputs -show-outputs
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7dd36a74..c5fa5831 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -29,29 +29,48 @@
 #  include <dirent.h>
 #endif
 
+#include "frontends/verific/verific.h"
+
 USING_YOSYS_NAMESPACE
 
 #ifdef YOSYS_ENABLE_VERIFIC
 
+#ifdef __clang__
 #pragma clang diagnostic push
 #pragma clang diagnostic ignored "-Woverloaded-virtual"
+#endif
 
 #include "veri_file.h"
 #include "vhdl_file.h"
+#include "hier_tree.h"
 #include "VeriModule.h"
+#include "VeriWrite.h"
 #include "VhdlUnits.h"
-#include "DataBase.h"
 #include "Message.h"
 
+#ifdef __clang__
 #pragma clang diagnostic pop
+#endif
 
 #ifdef VERIFIC_NAMESPACE
-using namespace Verific ;
+using namespace Verific;
+#endif
+
 #endif
 
-static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
+#ifdef YOSYS_ENABLE_VERIFIC
+YOSYS_NAMESPACE_BEGIN
+
+int verific_verbose;
+bool verific_import_pending;
+string verific_error_msg;
+int verific_sva_fsm_limit;
+
+vector<string> verific_incdirs, verific_libdirs;
+
+void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
 {
-	log("VERIFIC-%s [%s] ",
+	string message_prefix = stringf("VERIFIC-%s [%s] ",
 			msg_type == VERIFIC_NONE ? "NONE" :
 			msg_type == VERIFIC_ERROR ? "ERROR" :
 			msg_type == VERIFIC_WARNING ? "WARNING" :
@@ -59,13 +78,47 @@ static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type
 			msg_type == VERIFIC_INFO ? "INFO" :
 			msg_type == VERIFIC_COMMENT ? "COMMENT" :
 			msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id);
-	if (linefile)
-		log("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile));
-	logv(msg, args);
-	log("\n");
+
+	string message = linefile ? stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)) : "";
+	message += vstringf(msg, args);
+
+	if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR)
+		log_warning_noprefix("%s%s\n", message_prefix.c_str(), message.c_str());
+	else
+		log("%s%s\n", message_prefix.c_str(), message.c_str());
+
+	if (verific_error_msg.empty() && (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_PROGRAM_ERROR))
+		verific_error_msg = message;
 }
 
-static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+string get_full_netlist_name(Netlist *nl)
+{
+	if (nl->NumOfRefs() == 1) {
+		Instance *inst = (Instance*)nl->GetReferences()->GetLast();
+		return get_full_netlist_name(inst->Owner()) + "." + inst->Name();
+	}
+
+	return nl->CellBaseName();
+}
+
+// ==================================================================
+
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover) :
+		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+		mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover)
+{
+}
+
+RTLIL::SigBit VerificImporter::net_map_at(Net *net)
+{
+	if (net->IsExternalTo(netlist))
+		log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
+				get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
+
+	return net_map.at(net);
+}
+
+void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
 {
 	MapIter mi;
 	Att *attr;
@@ -74,44 +127,47 @@ static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, D
 		attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
 
 	// FIXME: Parse numeric attributes
-	FOREACH_ATTRIBUTE(obj, mi, attr)
+	FOREACH_ATTRIBUTE(obj, mi, attr) {
+		if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
+			continue;
 		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+	}
 }
 
-static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
+RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
 {
 	RTLIL::SigSpec sig;
 	for (int i = int(inst->InputSize())-1; i >= 0; i--)
 		if (inst->GetInputBit(i))
-			sig.append(net_map.at(inst->GetInputBit(i)));
+			sig.append(net_map_at(inst->GetInputBit(i)));
 		else
 			sig.append(RTLIL::State::Sz);
 	return sig;
 }
 
-static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
+RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
 {
 	RTLIL::SigSpec sig;
 	for (int i = int(inst->Input1Size())-1; i >= 0; i--)
 		if (inst->GetInput1Bit(i))
-			sig.append(net_map.at(inst->GetInput1Bit(i)));
+			sig.append(net_map_at(inst->GetInput1Bit(i)));
 		else
 			sig.append(RTLIL::State::Sz);
 	return sig;
 }
 
-static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
+RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
 {
 	RTLIL::SigSpec sig;
 	for (int i = int(inst->Input2Size())-1; i >= 0; i--)
 		if (inst->GetInput2Bit(i))
-			sig.append(net_map.at(inst->GetInput2Bit(i)));
+			sig.append(net_map_at(inst->GetInput2Bit(i)));
 		else
 			sig.append(RTLIL::State::Sz);
 	return sig;
 }
 
-static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::map<Net*, RTLIL::SigBit> &net_map)
+RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
 {
 	PortBus *portbus = inst->View()->GetPortBus(portname);
 	if (portbus) {
@@ -124,7 +180,7 @@ static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::
 				else if (net->IsPwr())
 					sig.append(RTLIL::State::S1);
 				else
-					sig.append(net_map.at(net));
+					sig.append(net_map_at(net));
 			} else
 				sig.append(RTLIL::State::Sz);
 		}
@@ -133,17 +189,17 @@ static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::
 		Port *port = inst->View()->GetPort(portname);
 		log_assert(port != NULL);
 		Net *net = inst->GetNet(port);
-		return net_map.at(net);
+		return net_map_at(net);
 	}
 }
 
-static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map, RTLIL::Module *module)
+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)) {
-			sig.append(net_map.at(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 {
 			if (dummy_wire == NULL)
@@ -155,72 +211,74 @@ static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBi
 	return sig;
 }
 
-static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
+bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
 {
 	if (inst->Type() == PRIM_AND) {
-		module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NAND) {
 		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+		module->addAndGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_OR) {
-		module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NOR) {
 		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+		module->addOrGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XOR) {
-		module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XNOR) {
-		module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_BUF) {
-		module->addBufGate(RTLIL::escape_id(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;
 	}
 
 	if (inst->Type() == PRIM_INV) {
-		module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+		module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_MUX) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+		module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_TRI) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+		module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_FADD)
 	{
-		RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin());
-		RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID);
-		RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
+		RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
+		RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(NEW_ID);
+		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
 		RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
 		RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
 		RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
 		module->addXorGate(NEW_ID, a, b, tmp1);
-		module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y);
+		module->addXorGate(inst_name, tmp1, c, y);
 		module->addAndGate(NEW_ID, tmp1, c, tmp2);
 		module->addAndGate(NEW_ID, a, b, tmp3);
 		module->addOrGate(NEW_ID, tmp2, tmp3, x);
@@ -229,163 +287,168 @@ static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*,
 
 	if (inst->Type() == PRIM_DFFRS)
 	{
+		VerificClocking clocking(this, inst->GetClock());
+		log_assert(clocking.disable_sig == State::S0);
+		log_assert(clocking.body_net == nullptr);
+
 		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		else if (inst->GetSet()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false);
+			clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0);
 		else if (inst->GetReset()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true);
+			clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1);
 		else
-			module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	return false;
 }
 
-static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
+bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
 {
 	if (inst->Type() == PRIM_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NAND) {
 		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+		module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NOR) {
 		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+		module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+		module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+		module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+		module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+		module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_FADD)
 	{
 		RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
-		RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
+		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
 		if (inst->GetCout())
-			y.append(net_map.at(inst->GetCout()));
-		module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b);
-		module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y);
+			y.append(net_map_at(inst->GetCout()));
+		module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
+		module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_DFFRS)
 	{
+		VerificClocking clocking(this, inst->GetClock());
+		log_assert(clocking.disable_sig == State::S0);
+		log_assert(clocking.body_net == nullptr);
+
 		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		else if (inst->GetSet()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0);
+			clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
 		else if (inst->GetReset()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1);
+			clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
 		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == PRIM_DLATCHRS)
 	{
 		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		else
-			module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		return true;
 	}
 
-	#define IN  operatorInput(inst, net_map)
-	#define IN1 operatorInput1(inst, net_map)
-	#define IN2 operatorInput2(inst, net_map)
-	#define OUT operatorOutput(inst, net_map, module)
+	#define IN  operatorInput(inst)
+	#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) {
 		RTLIL::SigSpec out = OUT;
 		if (inst->GetCout() != NULL)
-			out.append(net_map.at(inst->GetCout()));
+			out.append(net_map_at(inst->GetCout()));
 		if (inst->GetCin()->IsGnd()) {
-			module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
+			module->addAdd(inst_name, IN1, IN2, out, SIGNED);
 		} else {
 			RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
 			module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
-			module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false);
+			module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
 		}
 		return true;
 	}
 
 	if (inst->Type() == OPER_MULTIPLIER) {
-		module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_DIVIDER) {
-		module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_MODULO) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REMAINDER) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_SHIFT_LEFT) {
-		module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+		module->addShl(inst_name, IN1, IN2, OUT, false);
 		return true;
 	}
 
 	if (inst->Type() == OPER_ENABLED_DECODER) {
 		RTLIL::SigSpec vec;
-		vec.append(net_map.at(inst->GetControl()));
+		vec.append(net_map_at(inst->GetControl()));
 		for (unsigned i = 1; i < inst->OutputSize(); i++) {
 			vec.append(RTLIL::State::S0);
 		}
-		module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+		module->addShl(inst_name, vec, IN, OUT, false);
 		return true;
 	}
 
@@ -395,7 +458,7 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
 		for (unsigned i = 1; i < inst->OutputSize(); i++) {
 			vec.append(RTLIL::State::S0);
 		}
-		module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+		module->addShl(inst_name, vec, IN, OUT, false);
 		return true;
 	}
 
@@ -403,112 +466,163 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
 		Net *net_cin = inst->GetCin();
 		Net *net_a_msb = inst->GetInput1Bit(0);
 		if (net_cin->IsGnd())
-			module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+			module->addShr(inst_name, IN1, IN2, OUT, false);
 		else if (net_cin == net_a_msb)
-			module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true);
+			module->addSshr(inst_name, IN1, IN2, OUT, true);
 		else
 			log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_AND) {
-		module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+		module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_OR) {
-		module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+		module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_XOR) {
-		module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+		module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_XNOR) {
-		module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+		module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
+
+	if (inst->Type() == OPER_REDUCE_NOR) {
+		SigSpec t = module->ReduceOr(NEW_ID, IN, SIGNED);
+		module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
 		return true;
 	}
 
 	if (inst->Type() == OPER_LESSTHAN) {
 		Net *net_cin = inst->GetCin();
 		if (net_cin->IsGnd())
-			module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		else if (net_cin->IsPwr())
-			module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		else
 			log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+		module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+		module->addNot(inst_name, IN, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_MINUS) {
-		module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+		module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_UMINUS) {
-		module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+		module->addNeg(inst_name, IN, OUT, SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_EQUAL) {
-		module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+		module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_NEQUAL) {
-		module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+		module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT);
+		module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+		return true;
+	}
+
+	if (inst->Type() == OPER_NTO1MUX) {
+		module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+		return true;
+	}
+
+	if (inst->Type() == OPER_WIDE_NTO1MUX)
+	{
+		SigSpec data = IN2, out = OUT;
+
+		int wordsize_bits = ceil_log2(GetSize(out));
+		int wordsize = 1 << wordsize_bits;
+
+		SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};
+
+		SigSpec padded_data;
+		for (int i = 0; i < GetSize(data); i += GetSize(out)) {
+			SigSpec d = data.extract(i, GetSize(out));
+			d.extend_u0(wordsize);
+			padded_data.append(d);
+		}
+
+		module->addShr(inst_name, padded_data, sel, out);
+		return true;
+	}
+
+	if (inst->Type() == OPER_SELECTOR)
+	{
+		module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
+		return true;
+	}
+
+	if (inst->Type() == OPER_WIDE_SELECTOR)
+	{
+		SigSpec out = OUT;
+		module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT);
+		module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
 		return true;
 	}
 
-	if (inst->Type() == OPER_WIDE_DFFRS) {
-		RTLIL::SigSpec sig_set = operatorInport(inst, "set", net_map);
-		RTLIL::SigSpec sig_reset = operatorInport(inst, "reset", net_map);
+	if (inst->Type() == OPER_WIDE_DFFRS)
+	{
+		VerificClocking clocking(this, inst->GetClock());
+		log_assert(clocking.disable_sig == State::S0);
+		log_assert(clocking.body_net == nullptr);
+
+		RTLIL::SigSpec sig_set = operatorInport(inst, "set");
+		RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
+
 		if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT);
+			clocking.addDff(inst_name, IN, OUT);
 		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
+			clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
+
 		return true;
 	}
 
@@ -521,23 +635,95 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
 	return false;
 }
 
-static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
+void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
+{
+	bool keep_running = true;
+	SigMap sigmap;
+
+	while (keep_running)
+	{
+		keep_running = false;
+
+		dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
+		SigSpec dbits;
+
+		for (auto cell : candidates) {
+			SigBit bit = sigmap(cell->getPort("\\D"));
+			dbits_db[bit].insert(cell);
+			dbits.append(bit);
+		}
+
+		dbits.sort_and_unify();
+
+		for (auto chunk : dbits.chunks())
+		{
+			SigSpec sig_d = chunk;
+
+			if (chunk.wire == nullptr || GetSize(sig_d) == 1)
+				continue;
+
+			SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
+			RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
+
+			if (verific_verbose)
+				log("  merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
+
+			for (int i = 0; i < GetSize(sig_d); i++)
+				for (auto old_ff : dbits_db[sig_d[i]])
+				{
+					if (verific_verbose)
+						log("    replacing old ff %s on bit %d.\n", log_id(old_ff), i);
+
+					SigBit old_q = old_ff->getPort("\\Q");
+					SigBit new_q = sig_q[i];
+
+					sigmap.add(old_q, new_q);
+					module->connect(old_q, new_q);
+					candidates.erase(old_ff);
+					module->remove(old_ff);
+					keep_running = true;
+				}
+		}
+	}
+}
+
+void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
+{
+	dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
+
+	for (auto cell : candidates)
+	{
+		SigBit clock = cell->getPort("\\CLK");
+		bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
+		database[make_pair(clock, int(clock_pol))].insert(cell);
+	}
+
+	for (auto it : database)
+		merge_past_ffs_clock(it.second, it.first.first, it.first.second);
+}
+
+void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
 {
 	std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
 
+	netlist = nl;
+
 	if (design->has(module_name)) {
 		if (!nl->IsOperator())
 			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
 		return;
 	}
 
-	RTLIL::Module *module = new RTLIL::Module;
+	module = new RTLIL::Module;
 	module->name = module_name;
 	design->add(module);
 
-	log("Importing module %s.\n", RTLIL::id2cstr(module->name));
-
-	std::map<Net*, RTLIL::SigBit> net_map;
+	if (nl->IsBlackBox()) {
+		log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
+		module->set_bool_attribute("\\blackbox");
+	} else {
+		log("Importing module %s.\n", RTLIL::id2cstr(module->name));
+	}
 
 	SetIter si;
 	MapIter mi, mi2;
@@ -553,7 +739,8 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 		if (port->Bus())
 			continue;
 
-		// log("  importing port %s.\n", port->Name());
+		if (verific_verbose)
+			log("  importing port %s.\n", port->Name());
 
 		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
 		import_attributes(wire->attributes, port);
@@ -570,15 +757,16 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 			if (net_map.count(net) == 0)
 				net_map[net] = wire;
 			else if (wire->port_input)
-				module->connect(net_map.at(net), wire);
+				module->connect(net_map_at(net), wire);
 			else
-				module->connect(wire, net_map.at(net));
+				module->connect(wire, net_map_at(net));
 		}
 	}
 
 	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
 	{
-		// log("  importing portbus %s.\n", portbus->Name());
+		if (verific_verbose)
+			log("  importing portbus %s.\n", portbus->Name());
 
 		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
 		wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
@@ -596,9 +784,9 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 				if (net_map.count(net) == 0)
 					net_map[net] = bit;
 				else if (wire->port_input)
-					module->connect(net_map.at(net), bit);
+					module->connect(net_map_at(net), bit);
 				else
-					module->connect(bit, net_map.at(net));
+					module->connect(bit, net_map_at(net));
 			}
 			if (i == portbus->RightIndex())
 				break;
@@ -607,6 +795,11 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 
 	module->fixup_ports();
 
+	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)
 	{
 		if (net->IsRamNet())
@@ -633,20 +826,98 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 
 			memory->width = bits_in_word;
 			memory->size = number_of_bits / bits_in_word;
+
+			const char *ascii_initdata = net->GetWideInitialValue();
+			if (ascii_initdata) {
+				while (*ascii_initdata != 0 && *ascii_initdata != '\'')
+					ascii_initdata++;
+				if (*ascii_initdata == '\'')
+					ascii_initdata++;
+				if (*ascii_initdata != 0) {
+					log_assert(*ascii_initdata == 'b');
+					ascii_initdata++;
+				}
+				for (int word_idx = 0; word_idx < memory->size; word_idx++) {
+					Const initval = Const(State::Sx, memory->width);
+					bool initval_valid = false;
+					for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
+						if (*ascii_initdata == 0)
+							break;
+						if (*ascii_initdata == '0' || *ascii_initdata == '1') {
+							initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
+							initval_valid = true;
+						}
+						ascii_initdata++;
+					}
+					if (initval_valid) {
+						RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
+						cell->parameters["\\WORDS"] = 1;
+						if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
+							cell->setPort("\\ADDR", word_idx);
+						else
+							cell->setPort("\\ADDR", memory->size - word_idx - 1);
+						cell->setPort("\\DATA", initval);
+						cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
+						cell->parameters["\\ABITS"] = 32;
+						cell->parameters["\\WIDTH"] = memory->width;
+						cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
+					}
+				}
+			}
 			continue;
 		}
 
+		if (net->GetInitialValue())
+			init_nets[net] = net->GetInitialValue();
+
+		const char *rand_const_attr = net->GetAttValue(" rand_const");
+		const char *rand_attr = net->GetAttValue(" rand");
+
+		const char *anyconst_attr = net->GetAttValue("anyconst");
+		const char *anyseq_attr = net->GetAttValue("anyseq");
+
+		const char *allconst_attr = net->GetAttValue("allconst");
+		const char *allseq_attr = net->GetAttValue("allseq");
+
+		if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
+			anyconst_nets.insert(net);
+			any_all_nets.insert(net);
+		}
+		else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
+			anyseq_nets.insert(net);
+			any_all_nets.insert(net);
+		}
+		else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
+			anyconst_nets.insert(net);
+			any_all_nets.insert(net);
+		}
+		else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
+			anyseq_nets.insert(net);
+			any_all_nets.insert(net);
+		}
+		else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
+			allconst_nets.insert(net);
+			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)) {
-			// log("  skipping net %s.\n", net->Name());
+			if (verific_verbose)
+				log("  skipping net %s.\n", net->Name());
 			continue;
 		}
 
 		if (net->Bus())
 			continue;
 
-		// log("  importing net %s.\n", net->Name());
+		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
+
+		if (verific_verbose)
+			log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));
 
-		RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
 		RTLIL::Wire *wire = module->addWire(wire_name);
 		import_attributes(wire->attributes, net);
 
@@ -666,81 +937,191 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 
 		if (found_new_net)
 		{
-			// log("  importing netbus %s.\n", netbus->Name());
+			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
+
+			if (verific_verbose)
+				log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
 
-			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
 			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
 			wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
 			import_attributes(wire->attributes, netbus);
 
-			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
-				if (netbus->ElementAtIndex(i)) {
+			RTLIL::Const initval = Const(State::Sx, GetSize(wire));
+			bool initval_valid = false;
+
+			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
+			{
+				if (netbus->ElementAtIndex(i))
+				{
+					int bitidx = i - wire->start_offset;
 					net = netbus->ElementAtIndex(i);
-					RTLIL::SigBit bit(wire, i - wire->start_offset);
+					RTLIL::SigBit bit(wire, bitidx);
+
+					if (init_nets.count(net)) {
+						if (init_nets.at(net) == '0')
+							initval.bits.at(bitidx) = State::S0;
+						if (init_nets.at(net) == '1')
+							initval.bits.at(bitidx) = State::S1;
+						initval_valid = true;
+						init_nets.erase(net);
+					}
+
 					if (net_map.count(net) == 0)
 						net_map[net] = bit;
 					else
-						module->connect(bit, net_map.at(net));
+						module->connect(bit, net_map_at(net));
 				}
+
 				if (i == netbus->RightIndex())
 					break;
 			}
+
+			if (initval_valid)
+				wire->attributes["\\init"] = initval;
 		}
 		else
 		{
-			// log("  skipping netbus %s.\n", netbus->Name());
+			if (verific_verbose)
+				log("  skipping netbus %s.\n", netbus->Name());
+		}
+
+		SigSpec anyconst_sig;
+		SigSpec anyseq_sig;
+		SigSpec allconst_sig;
+		SigSpec allseq_sig;
+
+		for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
+			net = netbus->ElementAtIndex(i);
+			if (net != nullptr && anyconst_nets.count(net)) {
+				anyconst_sig.append(net_map_at(net));
+				anyconst_nets.erase(net);
+			}
+			if (net != nullptr && anyseq_nets.count(net)) {
+				anyseq_sig.append(net_map_at(net));
+				anyseq_nets.erase(net);
+			}
+			if (net != nullptr && allconst_nets.count(net)) {
+				allconst_sig.append(net_map_at(net));
+				allconst_nets.erase(net);
+			}
+			if (net != nullptr && allseq_nets.count(net)) {
+				allseq_sig.append(net_map_at(net));
+				allseq_nets.erase(net);
+			}
+			if (i == netbus->LeftIndex())
+				break;
 		}
+
+		if (GetSize(anyconst_sig))
+			module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
+
+		if (GetSize(anyseq_sig))
+			module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
+
+		if (GetSize(allconst_sig))
+			module->connect(allconst_sig, module->Allconst(NEW_ID, GetSize(allconst_sig)));
+
+		if (GetSize(allseq_sig))
+			module->connect(allseq_sig, module->Allseq(NEW_ID, GetSize(allseq_sig)));
 	}
 
+	for (auto it : init_nets)
+	{
+		Const initval;
+		SigBit bit = net_map_at(it.first);
+		log_assert(bit.wire);
+
+		if (bit.wire->attributes.count("\\init"))
+			initval = bit.wire->attributes.at("\\init");
+
+		while (GetSize(initval) < GetSize(bit.wire))
+			initval.bits.push_back(State::Sx);
+
+		if (it.second == '0')
+			initval.bits.at(bit.offset) = State::S0;
+		if (it.second == '1')
+			initval.bits.at(bit.offset) = State::S1;
+
+		bit.wire->attributes["\\init"] = initval;
+	}
+
+	for (auto net : anyconst_nets)
+		module->connect(net_map_at(net), module->Anyconst(NEW_ID));
+
+	for (auto net : anyseq_nets)
+		module->connect(net_map_at(net), module->Anyseq(NEW_ID));
+
+	pool<Instance*, hash_ptr_ops> sva_asserts;
+	pool<Instance*, hash_ptr_ops> sva_assumes;
+	pool<Instance*, hash_ptr_ops> sva_covers;
+	pool<Instance*, hash_ptr_ops> sva_triggers;
+
+	pool<RTLIL::Cell*> past_ffs;
+
 	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
 	{
-		// log("  importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
+		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
+
+		if (verific_verbose)
+			log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
+
+		if (mode_verific)
+			goto import_verific_cells;
 
 		if (inst->Type() == PRIM_PWR) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1);
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
 			continue;
 		}
 
 		if (inst->Type() == PRIM_GND) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0);
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
 			continue;
 		}
 
 		if (inst->Type() == PRIM_BUF) {
-			module->addBufGate(RTLIL::escape_id(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;
 		}
 
 		if (inst->Type() == PRIM_X) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx);
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
 			continue;
 		}
 
 		if (inst->Type() == PRIM_Z) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
 			continue;
 		}
 
 		if (inst->Type() == OPER_READ_PORT)
 		{
 			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
-			if (memory->width != int(inst->OutputSize()))
-				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+			int numchunks = int(inst->OutputSize()) / memory->width;
+			int chunksbits = ceil_log2(numchunks);
 
-			RTLIL::SigSpec addr = operatorInput1(inst, net_map);
-			RTLIL::SigSpec data = operatorOutput(inst, net_map, module);
+			if ((numchunks * memory->width) != int(inst->OutputSize()) || (numchunks & (numchunks - 1)) != 0)
+				log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
 
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd");
-			cell->parameters["\\MEMID"] = memory->name.str();
-			cell->parameters["\\CLK_ENABLE"] = false;
-			cell->parameters["\\CLK_POLARITY"] = true;
-			cell->parameters["\\TRANSPARENT"] = false;
-			cell->parameters["\\ABITS"] = GetSize(addr);
-			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\CLK", RTLIL::State::Sx);
-			cell->setPort("\\EN", RTLIL::State::Sx);
-			cell->setPort("\\ADDR", addr);
-			cell->setPort("\\DATA", data);
+			for (int i = 0; i < numchunks; i++)
+			{
+				RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
+				RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
+
+				RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
+						RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memrd");
+				cell->parameters["\\MEMID"] = memory->name.str();
+				cell->parameters["\\CLK_ENABLE"] = false;
+				cell->parameters["\\CLK_POLARITY"] = true;
+				cell->parameters["\\TRANSPARENT"] = false;
+				cell->parameters["\\ABITS"] = GetSize(addr);
+				cell->parameters["\\WIDTH"] = GetSize(data);
+				cell->setPort("\\CLK", RTLIL::State::Sx);
+				cell->setPort("\\EN", RTLIL::State::Sx);
+				cell->setPort("\\ADDR", addr);
+				cell->setPort("\\DATA", data);
+			}
 			continue;
 		}
 
@@ -748,52 +1129,197 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 		{
 			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
 			if (memory->width != int(inst->Input2Size()))
-				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+				log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
 
-			RTLIL::SigSpec addr = operatorInput1(inst, net_map);
-			RTLIL::SigSpec data = operatorInput2(inst, net_map);
+			RTLIL::SigSpec addr = operatorInput1(inst);
+			RTLIL::SigSpec data = operatorInput2(inst);
 
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr");
+			RTLIL::Cell *cell = module->addCell(inst_name, "$memwr");
 			cell->parameters["\\MEMID"] = memory->name.str();
 			cell->parameters["\\CLK_ENABLE"] = false;
 			cell->parameters["\\CLK_POLARITY"] = true;
 			cell->parameters["\\PRIORITY"] = 0;
 			cell->parameters["\\ABITS"] = GetSize(addr);
 			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data)));
+			cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
 			cell->setPort("\\CLK", RTLIL::State::S0);
 			cell->setPort("\\ADDR", addr);
 			cell->setPort("\\DATA", data);
 
 			if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
 				cell->parameters["\\CLK_ENABLE"] = true;
-				cell->setPort("\\CLK", net_map.at(inst->GetClock()));
+				cell->setPort("\\CLK", net_map_at(inst->GetClock()));
 			}
 			continue;
 		}
 
 		if (!mode_gates) {
-			if (import_netlist_instance_cells(module, net_map, inst))
+			if (import_netlist_instance_cells(inst, inst_name))
 				continue;
-			if (inst->IsOperator())
+			if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
 				log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
 		} else {
-			if (import_netlist_instance_gates(module, net_map, inst))
+			if (import_netlist_instance_gates(inst, inst_name))
+				continue;
+		}
+
+		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
+			sva_asserts.insert(inst);
+
+		if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
+			sva_assumes.insert(inst);
+
+		if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
+			sva_covers.insert(inst);
+
+		if (inst->Type() == PRIM_SVA_TRIGGERED)
+			sva_triggers.insert(inst);
+
+		if (inst->Type() == OPER_SVA_STABLE)
+		{
+			VerificClocking clocking(this, inst->GetInput2Bit(0));
+			log_assert(clocking.disable_sig == State::S0);
+			log_assert(clocking.body_net == nullptr);
+
+			log_assert(inst->Input1Size() == inst->OutputSize());
+
+			SigSpec sig_d, sig_q, sig_o;
+			sig_q = module->addWire(NEW_ID, inst->Input1Size());
+
+			for (int i = int(inst->Input1Size())-1; i >= 0; i--){
+				sig_d.append(net_map_at(inst->GetInput1Bit(i)));
+				sig_o.append(net_map_at(inst->GetOutputBit(i)));
+			}
+
+			if (verific_verbose) {
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+				log("    XNOR with A=%s, B=%s, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+			}
+
+			clocking.addDff(NEW_ID, sig_d, sig_q);
+			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+
+			if (!mode_keep)
 				continue;
 		}
 
+		if (inst->Type() == PRIM_SVA_STABLE)
+		{
+			VerificClocking clocking(this, inst->GetInput2());
+			log_assert(clocking.disable_sig == State::S0);
+			log_assert(clocking.body_net == nullptr);
+
+			SigSpec sig_d = net_map_at(inst->GetInput1());
+			SigSpec sig_o = net_map_at(inst->GetOutput());
+			SigSpec sig_q = module->addWire(NEW_ID);
+
+			if (verific_verbose) {
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+				log("    XNOR with A=%s, B=%s, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+			}
+
+			clocking.addDff(NEW_ID, sig_d, sig_q);
+			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+
+			if (!mode_keep)
+				continue;
+		}
+
+		if (inst->Type() == PRIM_SVA_PAST)
+		{
+			VerificClocking clocking(this, inst->GetInput2());
+			log_assert(clocking.disable_sig == State::S0);
+			log_assert(clocking.body_net == nullptr);
+
+			SigBit sig_d = net_map_at(inst->GetInput1());
+			SigBit sig_q = net_map_at(inst->GetOutput());
+
+			if (verific_verbose)
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+
+			past_ffs.insert(clocking.addDff(NEW_ID, sig_d, sig_q));
+
+			if (!mode_keep)
+				continue;
+		}
+
+		if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
+		{
+			VerificClocking clocking(this, inst->GetInput2());
+			log_assert(clocking.disable_sig == State::S0);
+			log_assert(clocking.body_net == nullptr);
+
+			SigBit sig_d = net_map_at(inst->GetInput1());
+			SigBit sig_o = net_map_at(inst->GetOutput());
+			SigBit sig_q = module->addWire(NEW_ID);
+
+			if (verific_verbose)
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
+
+			clocking.addDff(NEW_ID, sig_d, sig_q);
+			module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
+
+			if (!mode_keep)
+				continue;
+		}
+
+		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
+			if (verific_verbose)
+				log("    skipping SVA cell in non k-mode\n");
+			continue;
+		}
+
+		if (inst->Type() == PRIM_HDL_ASSERTION)
+		{
+			SigBit cond = net_map_at(inst->GetInput());
+
+			if (verific_verbose)
+				log("    assert condition %s.\n", log_signal(cond));
+
+			const char *assume_attr = nullptr; // inst->GetAttValue("assume");
+
+			Cell *cell = nullptr;
+			if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
+				cell = module->addAssume(NEW_ID, cond, State::S1);
+			else
+				cell = module->addAssert(NEW_ID, cond, State::S1);
+
+			import_attributes(cell->attributes, inst);
+			continue;
+		}
+
 		if (inst->IsPrimitive())
-			log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+		{
+			if (!mode_keep)
+				log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
 
+			if (!verific_sva_prims.count(inst->Type()))
+				log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+		}
+
+	import_verific_cells:
 		nl_todo.insert(inst->View());
 
-		RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ?
+		RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
 				std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
 
+		if (inst->IsPrimitive() && mode_keep)
+			cell->attributes["\\keep"] = 1;
+
 		dict<IdString, vector<SigBit>> cell_port_conns;
 
+		if (verific_verbose)
+			log("    ports in verific db:\n");
+
 		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
-			// log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
+			if (verific_verbose)
+				log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
 			const char *port_name = pr->GetPort()->Name();
 			int port_offset = 0;
 			if (pr->GetPort()->Bus()) {
@@ -808,127 +1334,691 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
 				for (auto bit : zwires)
 					sigvec.push_back(bit);
 			}
-			sigvec[port_offset] = net_map.at(pr->GetNet());
+			sigvec[port_offset] = net_map_at(pr->GetNet());
 		}
 
+		if (verific_verbose)
+			log("    ports in yosys db:\n");
+
 		for (auto &it : cell_port_conns) {
-			// log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
+			if (verific_verbose)
+				log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
 			cell->setPort(it.first, it.second);
 		}
 	}
+
+	if (!mode_nosva)
+	{
+		for (auto inst : sva_asserts) {
+			if (mode_autocover)
+				verific_import_sva_cover(this, inst);
+			verific_import_sva_assert(this, inst);
+		}
+
+		for (auto inst : sva_assumes)
+			verific_import_sva_assume(this, inst);
+
+		for (auto inst : sva_covers)
+			verific_import_sva_cover(this, inst);
+
+		for (auto inst : sva_triggers)
+			verific_import_sva_trigger(this, inst);
+
+		merge_past_ffs(past_ffs);
+	}
 }
 
+// ==================================================================
+
+VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
+{
+	module = importer->module;
+
+	log_assert(importer != nullptr);
+	log_assert(net != nullptr);
+
+	Instance *inst = net->Driver();
+
+	if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
+	{
+		net = inst->GetInput1();
+		body_net = inst->GetInput2();
+
+		inst = net->Driver();
+
+		Instance *body_inst = body_net->Driver();
+		if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
+			disable_net = body_inst->GetInput1();
+			disable_sig = importer->net_map_at(disable_net);
+			body_net = body_inst->GetInput2();
+		}
+	}
+	else
+	{
+		if (sva_at_only)
+			return;
+	}
+
+	// Use while() instead of if() to work around VIPER #13453
+	while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
+	{
+		net = inst->GetInput();
+		inst = net->Driver();;
+	}
+
+	if (inst != nullptr && inst->Type() == PRIM_INV)
+	{
+		net = inst->GetInput();
+		inst = net->Driver();;
+		posedge = false;
+	}
+
+	// Detect clock-enable circuit
+	do {
+		if (inst == nullptr || inst->Type() != PRIM_AND)
+			break;
+
+		Net *net_dlatch = inst->GetInput1();
+		Instance *inst_dlatch = net_dlatch->Driver();
+
+		if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
+			break;
+
+		if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
+			break;
+
+		Net *net_enable = inst_dlatch->GetInput();
+		Net *net_not_clock = inst_dlatch->GetControl();
+
+		if (net_enable == nullptr || net_not_clock == nullptr)
+			break;
+
+		Instance *inst_not_clock = net_not_clock->Driver();
+
+		if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
+			break;
+
+		Net *net_clock1 = inst_not_clock->GetInput();
+		Net *net_clock2 = inst->GetInput2();
+
+		if (net_clock1 == nullptr || net_clock1 != net_clock2)
+			break;
+
+		enable_net = net_enable;
+		enable_sig = importer->net_map_at(enable_net);
+
+		net = net_clock1;
+		inst = net->Driver();;
+	} while (0);
+
+	// Detect condition expression
+	do {
+		if (body_net == nullptr)
+			break;
+
+		Instance *inst_mux = body_net->Driver();
+
+		if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
+			break;
+
+		if (!inst_mux->GetInput1()->IsPwr())
+			break;
+
+		Net *sva_net = inst_mux->GetInput2();
+		if (!verific_is_sva_net(importer, sva_net))
+			break;
+
+		body_net = sva_net;
+		cond_net = inst_mux->GetControl();
+	} while (0);
+
+	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)
+{
+	log_assert(GetSize(sig_d) == GetSize(sig_q));
+
+	if (GetSize(init_value) != 0) {
+		log_assert(GetSize(sig_q) == GetSize(init_value));
+		if (sig_q.is_wire()) {
+			sig_q.as_wire()->attributes["\\init"] = init_value;
+		} else {
+			Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
+			w->attributes["\\init"] = init_value;
+			module->connect(sig_q, w);
+			sig_q = w;
+		}
+	}
+
+	if (enable_sig != State::S1)
+		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)
+		sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
+
+	return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
+}
+
+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)
+		sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
+
+	return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
+}
+
+// ==================================================================
+
+struct VerificExtNets
+{
+	int portname_cnt = 0;
+
+	// a map from Net to the same Net one level up in the design hierarchy
+	std::map<Net*, Net*> net_level_up;
+
+	Net *get_net_level_up(Net *net)
+	{
+		if (net_level_up.count(net) == 0)
+		{
+			Netlist *nl = net->Owner();
+
+			// Simply return if Netlist is not unique
+			if (nl->NumOfRefs() != 1)
+				return net;
+
+			Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
+			Netlist *up_nl = up_inst->Owner();
+
+			// create new Port
+			string name = stringf("___extnets_%d", portname_cnt++);
+			Port *new_port = new Port(name.c_str(), DIR_OUT);
+			nl->Add(new_port);
+			net->Connect(new_port);
+
+			// create new Net in up Netlist
+			Net *new_net = new Net(name.c_str());
+			up_nl->Add(new_net);
+			up_inst->Connect(new_port, new_net);
+
+			net_level_up[net] = new_net;
+		}
+
+		return net_level_up.at(net);
+	}
+
+	void run(Netlist *nl)
+	{
+		MapIter mi, mi2;
+		Instance *inst;
+		PortRef *pr;
+
+		vector<tuple<Instance*, Port*, Net*>> todo_connect;
+
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+			run(inst->View());
+
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+		FOREACH_PORTREF_OF_INST(inst, mi2, pr)
+		{
+			Port *port = pr->GetPort();
+			Net *net = pr->GetNet();
+
+			if (!net->IsExternalTo(nl))
+				continue;
+
+			if (verific_verbose)
+				log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
+
+			while (net->IsExternalTo(nl))
+			{
+				Net *newnet = get_net_level_up(net);
+				if (newnet == net) break;
+
+				if (verific_verbose)
+					log("  external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
+				net = newnet;
+			}
+
+			if (verific_verbose)
+				log("  final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
+			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
+		}
+
+		for (auto it : todo_connect) {
+			get<0>(it)->Disconnect(get<1>(it));
+			get<0>(it)->Connect(get<1>(it), get<2>(it));
+		}
+	}
+};
+
+void verific_import(Design *design, std::string top)
+{
+	verific_sva_fsm_limit = 16;
+
+	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_incdirs.clear();
+	verific_libdirs.clear();
+	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 */
 
-YOSYS_NAMESPACE_BEGIN
+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()
+	void help() YS_OVERRIDE
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..\n");
+		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
 		log("\n");
 		log("Load the specified Verilog/SystemVerilog files into Verific.\n");
 		log("\n");
+		log("All files specified in one call to this command are one compilation unit.\n");
+		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 {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>..\n");
+		log("    verific -formal <verilog-file>..\n");
+		log("\n");
+		log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
+		log("\n");
+		log("\n");
+		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
 		log("\n");
-		log("    verific -import [-gates] {-all | <top-module>..}\n");
+		log("    verific -work <libname> {-sv|-vhdl|...} <hdl-file>\n");
+		log("\n");
+		log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
+		log("(default library when -work is not present: \"work\")\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-incdir <directory>..\n");
+		log("\n");
+		log("Add Verilog include directories.\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-libdir <directory>..\n");
+		log("\n");
+		log("Add Verilog library directories. Verific will search in this directories to\n");
+		log("find undefined modules.\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-define <macro>[=<value>]..\n");
+		log("\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 -set-error <msg_id>..\n");
+		log("    verific -set-warning <msg_id>..\n");
+		log("    verific -set-info <msg_id>..\n");
+		log("    verific -set-ignore <msg_id>..\n");
+		log("\n");
+		log("Set message severity. <msg_id> is the string in square brackets when a message\n");
+		log("is printed, such as VERI-1209.\n");
+		log("\n");
+		log("\n");
+		log("    verific -import [options] <top-module>..\n");
 		log("\n");
 		log("Elaborate the design for the specified top modules, import to Yosys and\n");
-		log("reset the internal state of Verific. A gate-level netlist is created\n");
-		log("when called with -gates.\n");
+		log("reset the internal state of Verific.\n");
+		log("\n");
+		log("Import options:\n");
+		log("\n");
+		log("  -all\n");
+		log("    Elaborate all modules, not just the hierarchy below the given top\n");
+		log("    modules. With this option the list of modules to import is optional.\n");
+		log("\n");
+		log("  -gates\n");
+		log("    Create a gate-level netlist.\n");
+		log("\n");
+		log("  -flatten\n");
+		log("    Flatten the design in Verific before importing.\n");
+		log("\n");
+		log("  -extnets\n");
+		log("    Resolve references to external nets by adding module ports as needed.\n");
+		log("\n");
+		log("  -autocover\n");
+		log("    Generate automatic cover statements for all asserts\n");
+		log("\n");
+		log("  -v, -vv\n");
+		log("    Verbose log messages. (-vv is even more verbose than -v.)\n");
+		log("\n");
+		log("The following additional import options are useful for debugging the Verific\n");
+		log("bindings (for Yosys and/or Verific developers):\n");
+		log("\n");
+		log("  -k\n");
+		log("    Keep going after an unsupported verific primitive is found. The\n");
+		log("    unsupported primitive is added as blockbox module to the design.\n");
+		log("    This will also add all SVA related cells to the design parallel to\n");
+		log("    the checker logic inferred by it.\n");
+		log("\n");
+		log("  -V\n");
+		log("    Import Verific netlist as-is without translating to Yosys cell types. \n");
+		log("\n");
+		log("  -nosva\n");
+		log("    Ignore SVA properties, do not infer checker logic.\n");
+		log("\n");
+		log("  -L <int>\n");
+		log("    Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+		log("\n");
+		log("  -n\n");
+		log("    Keep all Verific names on instances and nets. By default only\n");
+		log("    user-declared names are preserved.\n");
+		log("\n");
+		log("  -d <dump_file>\n");
+		log("    Dump the Verific netlist as a verilog file.\n");
 		log("\n");
 		log("Visit http://verific.com/ for more information on Verific.\n");
 		log("\n");
 	}
 #ifdef YOSYS_ENABLE_VERIFIC
-	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		log_header(design, "Executing VERIFIC (loading Verilog and VHDL designs using Verific).\n");
+		static bool set_verific_global_flags = true;
 
-		Message::SetConsoleOutput(0);
-		Message::RegisterCallBackMsg(msg_func);
+		if (check_noverific_env())
+			log_cmd_error("This version of Yosys is built without Verific support.\n");
 
-		if (args.size() > 1 && args[1] == "-vlog95") {
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95))
-					log_cmd_error("Reading `%s' in VERILOG_95 mode failed.\n", args[argidx].c_str());
-			return;
+		log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
+
+		if (set_verific_global_flags)
+		{
+			Message::SetConsoleOutput(0);
+			Message::RegisterCallBackMsg(msg_func);
+			RuntimeFlags::SetVar("db_preserve_user_nets", 1);
+			RuntimeFlags::SetVar("db_allow_external_nets", 1);
+			RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+			RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
+			RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
+			RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+
+			// Workaround for VIPER #13851
+			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
+
+			// WARNING: instantiating unknown module 'XYZ' (VERI-1063)
+			Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
+
+			set_verific_global_flags = false;
 		}
 
-		if (args.size() > 1 && args[1] == "-vlog2k") {
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_2K))
-					log_cmd_error("Reading `%s' in VERILOG_2K mode failed.\n", args[argidx].c_str());
-			return;
+		verific_verbose = 0;
+		verific_sva_fsm_limit = 16;
+
+		const char *release_str = Message::ReleaseString();
+		time_t release_time = Message::ReleaseDate();
+		char *release_tmstr = ctime(&release_time);
+
+		if (release_str == nullptr)
+			release_str = "(no release string)";
+
+		for (char *p = release_tmstr; *p; p++)
+			if (*p == '\n') *p = 0;
+
+		log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
+
+		int argidx = 1;
+		std::string work = "work";
+
+		if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
+				args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
+		{
+			msg_type_t new_type;
+
+			if (args[argidx] == "-set-error")
+				new_type = VERIFIC_ERROR;
+			else if (args[argidx] == "-set-warning")
+				new_type = VERIFIC_WARNING;
+			else if (args[argidx] == "-set-info")
+				new_type = VERIFIC_INFO;
+			else if (args[argidx] == "-set-ignore")
+				new_type = VERIFIC_IGNORE;
+			else
+				log_abort();
+
+			for (argidx++; argidx < GetSize(args); argidx++)
+				Message::SetMessageType(args[argidx].c_str(), new_type);
+
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-sv2005") {
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2005))
-					log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2005 mode failed.\n", args[argidx].c_str());
-			return;
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
+			for (argidx++; argidx < GetSize(args); argidx++)
+				verific_incdirs.push_back(args[argidx]);
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-sv2009") {
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2009))
-					log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2009 mode failed.\n", args[argidx].c_str());
-			return;
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
+			for (argidx++; argidx < GetSize(args); argidx++)
+				verific_libdirs.push_back(args[argidx]);
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-sv") {
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG))
-					log_cmd_error("Reading `%s' in SYSTEM_VERILOG mode failed.\n", args[argidx].c_str());
-			return;
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				string 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::DefineCmdLineMacro(name.c_str(), value.c_str());
+				} else {
+					veri_file::DefineCmdLineMacro(name.c_str());
+				}
+			}
+			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 (args.size() > 1 && args[1] == "-vhdl87") {
+		for (; argidx < GetSize(args); argidx++)
+		{
+			if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
+				work = args[++argidx];
+				continue;
+			}
+			break;
+		}
+
+		if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
+				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
+		{
+			Array file_names;
+			unsigned verilog_mode;
+
+			if (args[argidx] == "-vlog95")
+				verilog_mode = veri_file::VERILOG_95;
+			else if (args[argidx] == "-vlog2k")
+				verilog_mode = veri_file::VERILOG_2K;
+			else if (args[argidx] == "-sv2005")
+				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" || args[argidx] == "-formal")
+				verilog_mode = veri_file::SYSTEM_VERILOG;
+			else
+				log_abort();
+
+			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());
+				}
+			}
+
+			for (auto &dir : verific_incdirs)
+				veri_file::AddIncludeDir(dir.c_str());
+			for (auto &dir : verific_libdirs)
+				veri_file::AddYDir(dir.c_str());
+
+			while (argidx < GetSize(args))
+				file_names.Insert(args[argidx++].c_str());
+
+			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
+					log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
+
+			verific_import_pending = true;
+			goto check_error;
+		}
+
+		if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
+			for (argidx++; argidx < GetSize(args); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
 					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
-			return;
+			verific_import_pending = true;
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-vhdl93") {
+		if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
+			for (argidx++; argidx < GetSize(args); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
 					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
-			return;
+			verific_import_pending = true;
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-vhdl2k") {
+		if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
+			for (argidx++; argidx < GetSize(args); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
 					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
-			return;
+			verific_import_pending = true;
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-vhdl2008") {
+		if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
-			for (size_t argidx = 2; argidx < args.size(); argidx++)
-				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
+			for (argidx++; argidx < GetSize(args); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
 					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
-			return;
+			verific_import_pending = true;
+			goto check_error;
 		}
 
-		if (args.size() > 1 && args[1] == "-import")
+		if (GetSize(args) > argidx && args[argidx] == "-import")
 		{
 			std::set<Netlist*> nl_todo, nl_done;
-			bool mode_all = false, mode_gates = false;
+			bool mode_all = false, mode_gates = false, mode_keep = false;
+			bool mode_nosva = false, mode_names = false, mode_verific = false;
+			bool mode_autocover = false;
+			bool flatten = false, extnets = false;
+			string dumpfile;
 
-			size_t argidx = 2;
-			for (; argidx < args.size(); argidx++) {
+			for (argidx++; argidx < GetSize(args); argidx++) {
 				if (args[argidx] == "-all") {
 					mode_all = true;
 					continue;
@@ -937,69 +2027,346 @@ struct VerificPass : public Pass {
 					mode_gates = true;
 					continue;
 				}
+				if (args[argidx] == "-flatten") {
+					flatten = true;
+					continue;
+				}
+				if (args[argidx] == "-extnets") {
+					extnets = true;
+					continue;
+				}
+				if (args[argidx] == "-k") {
+					mode_keep = true;
+					continue;
+				}
+				if (args[argidx] == "-nosva") {
+					mode_nosva = true;
+					continue;
+				}
+				if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+					verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+					continue;
+				}
+				if (args[argidx] == "-n") {
+					mode_names = true;
+					continue;
+				}
+				if (args[argidx] == "-autocover") {
+					mode_autocover = true;
+					continue;
+				}
+				if (args[argidx] == "-V") {
+					mode_verific = true;
+					continue;
+				}
+				if (args[argidx] == "-v") {
+					verific_verbose = 1;
+					continue;
+				}
+				if (args[argidx] == "-vv") {
+					verific_verbose = 2;
+					continue;
+				}
+				if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
+					dumpfile = args[++argidx];
+					continue;
+				}
 				break;
 			}
 
-			if (argidx > args.size() && args[argidx].substr(0, 1) == "-")
+			if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-")
 				cmd_error(args, argidx, "unknown option");
 
 			if (mode_all)
 			{
-				if (argidx != args.size())
-					log_cmd_error("Got -all and an explicit list of top modules.\n");
-
-				MapIter m1, m2, m3;
-				VeriModule *mod;
-				FOREACH_VERILOG_MODULE(m1, mod)
-					args.push_back(mod->Name());
-
-				VhdlLibrary *lib;
-				VhdlPrimaryUnit *primunit;
-				FOREACH_VHDL_LIBRARY(m1, lib)
-				FOREACH_VHDL_PRIMARY_UNIT(lib, m2, primunit) {
-					if (primunit->IsPackageDecl())
-						continue;
-					args.push_back(primunit->Name());
+#if 0
+				log("Running veri_file::ElaborateAll().\n");
+				if (!veri_file::ElaborateAll())
+					log_cmd_error("Elaboration of Verilog modules failed.\n");
+
+				log("Running vhdl_file::ElaborateAll().\n");
+				if (!vhdl_file::ElaborateAll())
+					log_cmd_error("Elaboration of VHDL modules failed.\n");
+
+				Library *lib = Netlist::PresentDesign()->Owner()->Owner();
+
+				if (argidx == GetSize(args))
+				{
+					MapIter iter;
+					char *iter_name;
+					Verific::Cell *iter_cell;
+
+					FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) {
+						if (*iter_name != '$')
+							nl_todo.insert(iter_cell->GetFirstNetlist());
+					}
+				}
+				else
+				{
+					for (; argidx < GetSize(args); argidx++)
+					{
+						Verific::Cell *cell = lib->GetCell(args[argidx].c_str());
+
+						if (cell == nullptr)
+							log_cmd_error("Module not found: %s\n", args[argidx].c_str());
+
+						nl_todo.insert(cell->GetFirstNetlist());
+						cell->GetFirstNetlist()->SetPresentDesign();
+					}
 				}
+#else
+				log("Running hier_tree::ElaborateAll().\n");
+
+				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+				VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+
+				Array veri_libs, vhdl_libs;
+				if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+				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)
+					nl_todo.insert(nl);
+				delete netlists;
+#endif
 			}
 			else
-				if (argidx == args.size())
+			{
+				if (argidx == GetSize(args))
 					log_cmd_error("No top module specified.\n");
 
-			for (; argidx < args.size(); argidx++) {
-				if (veri_file::GetModule(args[argidx].c_str())) {
-					log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
-					if (!veri_file::Elaborate(args[argidx].c_str()))
-						log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
-					nl_todo.insert(Netlist::PresentDesign());
-				} else {
-					log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
-					if (!vhdl_file::Elaborate(args[argidx].c_str()))
-						log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
-					nl_todo.insert(Netlist::PresentDesign());
+#if 0
+				for (; argidx < GetSize(args); argidx++) {
+					if (veri_file::GetModule(args[argidx].c_str())) {
+						log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
+						if (!veri_file::Elaborate(args[argidx].c_str()))
+							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
+						nl_todo.insert(Netlist::PresentDesign());
+					} else {
+						log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
+						if (!vhdl_file::Elaborate(args[argidx].c_str()))
+							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
+						nl_todo.insert(Netlist::PresentDesign());
+					}
+				}
+#else
+				Array veri_modules, vhdl_units;
+				for (; argidx < GetSize(args); argidx++)
+				{
+					const char *name = args[argidx].c_str();
+
+					VeriModule *veri_module = veri_file::GetModule(name);
+					if (veri_module) {
+						log("Adding Verilog module '%s' to elaboration queue.\n", name);
+						veri_modules.InsertLast(veri_module);
+						continue;
+					}
+
+					VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+					VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
+					if (vhdl_unit) {
+						log("Adding VHDL unit '%s' to elaboration queue.\n", name);
+						vhdl_units.InsertLast(vhdl_unit);
+						continue;
+					}
+
+					log_error("Can't find module/unit '%s'.\n", name);
 				}
+
+				log("Running hier_tree::Elaborate().\n");
+				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units);
+				Netlist *nl;
+				int i;
+
+				FOREACH_ARRAY_ITEM(netlists, i, nl)
+					nl_todo.insert(nl);
+				delete netlists;
+#endif
+			}
+
+			if (!verific_error_msg.empty())
+				goto check_error;
+
+			if (flatten) {
+				for (auto nl : nl_todo)
+					nl->Flatten();
+			}
+
+			if (extnets) {
+				VerificExtNets worker;
+				for (auto nl : nl_todo)
+					worker.run(nl);
+			}
+
+			if (!dumpfile.empty()) {
+				VeriWrite veri_writer;
+				veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
 			}
 
 			while (!nl_todo.empty()) {
 				Netlist *nl = *nl_todo.begin();
-				if (nl_done.count(nl) == 0)
-					import_netlist(design, nl, nl_todo, mode_gates);
+				if (nl_done.count(nl) == 0) {
+					VerificImporter importer(mode_gates, mode_keep, mode_nosva,
+							mode_names, mode_verific, mode_autocover);
+					importer.import_netlist(design, nl, nl_todo);
+				}
 				nl_todo.erase(nl);
 				nl_done.insert(nl);
 			}
 
+			veri_file::Reset();
+			vhdl_file::Reset();
 			Libset::Reset();
-			return;
+			verific_incdirs.clear();
+			verific_libdirs.clear();
+			verific_import_pending = false;
+			goto check_error;
 		}
 
 		log_cmd_error("Missing or unsupported mode parameter.\n");
+
+	check_error:
+		if (!verific_error_msg.empty())
+			log_error("%s\n", verific_error_msg.c_str());
+
 	}
 #else /* YOSYS_ENABLE_VERIFIC */
-	virtual void execute(std::vector<std::string>, RTLIL::Design *) {
+	void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
 		log_cmd_error("This version of Yosys is built without Verific support.\n");
 	}
 #endif
 } VerificPass;
 
-YOSYS_NAMESPACE_END
+struct ReadPass : public Pass {
+	ReadPass() : Pass("read", "load HDL designs") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---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");
+		log("\n");
+		log("    read -incdir <directory>\n");
+		log("\n");
+		log("Add directory to global Verilog/SystemVerilog include directories.\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		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;
+		}
+
+		if (args[1] == "-incdir") {
+			if (use_verific) {
+				args[0] = "verific";
+				args[1] = "-vlog-incdir";
+				Pass::call(design, args);
+			}
+			args[0] = "verilog_defaults";
+			args[1] = "-add";
+			for (int i = 2; i < GetSize(args); i++)
+				args[i] = "-I" + 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
new file mode 100644
index 00000000..334a436a
--- /dev/null
+++ b/frontends/verific/verific.h
@@ -0,0 +1,108 @@
+/*
+ *  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.
+ *
+ */
+
+#ifdef YOSYS_ENABLE_VERIFIC
+
+#include "DataBase.h"
+
+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;
+
+struct VerificClocking {
+	RTLIL::Module *module = nullptr;
+	Verific::Net *clock_net = nullptr;
+	Verific::Net *enable_net = nullptr;
+	Verific::Net *disable_net = nullptr;
+	Verific::Net *body_net = nullptr;
+	Verific::Net *cond_net = nullptr;
+	SigBit clock_sig = State::Sx;
+	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);
+	RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
+	RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
+	RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
+
+	bool property_matches_sequence(const VerificClocking &seq) const {
+		if (clock_net != seq.clock_net)
+			return false;
+		if (enable_net != seq.enable_net)
+			return false;
+		if (posedge != seq.posedge)
+			return false;
+		return true;
+	}
+};
+
+struct VerificImporter
+{
+	RTLIL::Module *module;
+	Verific::Netlist *netlist;
+
+	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;
+
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover);
+
+	RTLIL::SigBit net_map_at(Verific::Net *net);
+
+	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj);
+
+	RTLIL::SigSpec operatorInput(Verific::Instance *inst);
+	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, 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);
+
+	void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
+	void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
+
+	void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
+};
+
+void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
+void verific_import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
+void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
+void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
+bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
+
+extern int verific_sva_fsm_limit;
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
new file mode 100644
index 00000000..cdc9ece8
--- /dev/null
+++ b/frontends/verific/verificsva.cc
@@ -0,0 +1,1815 @@
+/*
+ *  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.
+ *
+ */
+
+
+// Currently supported SVA sequence and property syntax:
+// http://symbiyosys.readthedocs.io/en/latest/verific.html
+//
+// Next gen property syntax:
+//   basic_property
+//   [antecedent_condition] property
+//   [antecedent_condition] always.. property
+//   [antecedent_condition] eventually.. basic_property
+//   [antecedent_condition] property until.. expression
+//   [antecedent_condition] basic_property until.. basic_property      (assert/assume only)
+//
+// antecedent_condition:
+//   sequence |->
+//   sequence |=>
+//
+// basic_property:
+//   sequence
+//   not basic_property
+//   sequence #-# basic_property
+//   sequence #=# basic_property
+//   basic_property or basic_property           (cover only)
+//   basic_property and basic_property          (assert/assume only)
+//   basic_property implies basic_property
+//   basic_property iff basic_property
+//
+// sequence:
+//   expression
+//   sequence ##N sequence
+//   sequence ##[*] sequence
+//   sequence ##[+] sequence
+//   sequence ##[N:M] sequence
+//   sequence ##[N:$] sequence
+//   expression [*]
+//   expression [+]
+//   expression [*N]
+//   expression [*N:M]
+//   expression [*N:$]
+//   sequence or sequence
+//   sequence and sequence
+//   expression throughout sequence
+//   sequence intersect sequence
+//   sequence within sequence
+//   first_match( sequence )
+//   expression [=N]
+//   expression [=N:M]
+//   expression [=N:$]
+//   expression [->N]
+//   expression [->N:M]
+//   expression [->N:$]
+
+
+#include "kernel/yosys.h"
+#include "frontends/verific/verific.h"
+
+USING_YOSYS_NAMESPACE
+
+#ifdef VERIFIC_NAMESPACE
+using namespace Verific;
+#endif
+
+PRIVATE_NAMESPACE_BEGIN
+
+// Non-deterministic FSM
+struct SvaNFsmNode
+{
+	// Edge: Activate the target node if ctrl signal is true, consumes clock cycle
+	// Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle
+	vector<pair<int, SigBit>> edges, links;
+	bool is_cond_node;
+};
+
+// Non-deterministic FSM after resolving links
+struct SvaUFsmNode
+{
+	// Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle
+	// Accept: This node functions as an accept node if all bits in ctrl signal are true
+	vector<pair<int, SigSpec>> edges;
+	vector<SigSpec> accept, cond;
+	bool reachable;
+};
+
+// Deterministic FSM
+struct SvaDFsmNode
+{
+	// A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors
+	// of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec.
+	SigSpec ctrl;
+	vector<pair<vector<int>, Const>> edges;
+	vector<Const> accept, reject;
+
+	// additional temp data for getReject()
+	Wire *ffoutwire;
+	SigBit statesig;
+	SigSpec nextstate;
+
+	// additional temp data for getDFsm()
+	int outnode;
+};
+
+struct SvaFsm
+{
+	Module *module;
+	VerificClocking clocking;
+
+	SigBit trigger_sig = State::S1, disable_sig;
+	SigBit throughout_sig = State::S1;
+	bool in_cond_mode = false;
+
+	vector<SigBit> disable_stack;
+	vector<SigBit> throughout_stack;
+
+	int startNode, acceptNode, condNode;
+	vector<SvaNFsmNode> nodes;
+
+	vector<SvaUFsmNode> unodes;
+	dict<vector<int>, SvaDFsmNode> dnodes;
+	dict<pair<SigSpec, SigSpec>, SigBit> cond_eq_cache;
+	bool materialized = false;
+
+	SigBit final_accept_sig = State::Sx;
+	SigBit final_reject_sig = State::Sx;
+
+	SvaFsm(const VerificClocking &clking, SigBit trig = State::S1)
+	{
+		module = clking.module;
+		clocking = clking;
+		trigger_sig = trig;
+
+		startNode = createNode();
+		acceptNode = createNode();
+
+		in_cond_mode = true;
+		condNode = createNode();
+		in_cond_mode = false;
+	}
+
+	void pushDisable(SigBit sig)
+	{
+		log_assert(!materialized);
+
+		disable_stack.push_back(disable_sig);
+
+		if (disable_sig == State::S0)
+			disable_sig = sig;
+		else
+			disable_sig = module->Or(NEW_ID, disable_sig, sig);
+	}
+
+	void popDisable()
+	{
+		log_assert(!materialized);
+		log_assert(!disable_stack.empty());
+
+		disable_sig = disable_stack.back();
+		disable_stack.pop_back();
+	}
+
+	void pushThroughout(SigBit sig)
+	{
+		log_assert(!materialized);
+
+		throughout_stack.push_back(throughout_sig);
+
+		if (throughout_sig == State::S1)
+			throughout_sig = sig;
+		else
+			throughout_sig = module->And(NEW_ID, throughout_sig, sig);
+	}
+
+	void popThroughout()
+	{
+		log_assert(!materialized);
+		log_assert(!throughout_stack.empty());
+
+		throughout_sig = throughout_stack.back();
+		throughout_stack.pop_back();
+	}
+
+	int createNode(int link_node = -1)
+	{
+		log_assert(!materialized);
+
+		int idx = GetSize(nodes);
+		nodes.push_back(SvaNFsmNode());
+		nodes.back().is_cond_node = in_cond_mode;
+		if (link_node >= 0)
+			createLink(link_node, idx);
+		return idx;
+	}
+
+	int createStartNode()
+	{
+		return createNode(startNode);
+	}
+
+	void createEdge(int from_node, int to_node, SigBit ctrl = State::S1)
+	{
+		log_assert(!materialized);
+		log_assert(0 <= from_node && from_node < GetSize(nodes));
+		log_assert(0 <= to_node && to_node < GetSize(nodes));
+		log_assert(from_node != acceptNode);
+		log_assert(to_node != acceptNode);
+		log_assert(from_node != condNode);
+		log_assert(to_node != condNode);
+		log_assert(to_node != startNode);
+
+		if (from_node != startNode)
+			log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);
+
+		if (throughout_sig != State::S1) {
+			if (ctrl != State::S1)
+				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
+			else
+				ctrl = throughout_sig;
+		}
+
+		nodes[from_node].edges.push_back(make_pair(to_node, ctrl));
+	}
+
+	void createLink(int from_node, int to_node, SigBit ctrl = State::S1)
+	{
+		log_assert(!materialized);
+		log_assert(0 <= from_node && from_node < GetSize(nodes));
+		log_assert(0 <= to_node && to_node < GetSize(nodes));
+		log_assert(from_node != acceptNode);
+		log_assert(from_node != condNode);
+		log_assert(to_node != startNode);
+
+		if (from_node != startNode)
+			log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);
+
+		if (throughout_sig != State::S1) {
+			if (ctrl != State::S1)
+				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
+			else
+				ctrl = throughout_sig;
+		}
+
+		nodes[from_node].links.push_back(make_pair(to_node, ctrl));
+	}
+
+	void make_link_order(vector<int> &order, int node, int min)
+	{
+		order[node] = std::max(order[node], min);
+		for (auto &it : nodes[node].links)
+			make_link_order(order, it.first, order[node]+1);
+	}
+
+	// ----------------------------------------------------
+	// Generating NFSM circuit to acquire accept signal
+
+	SigBit getAccept()
+	{
+		log_assert(!materialized);
+		materialized = true;
+
+		vector<Wire*> state_wire(GetSize(nodes));
+		vector<SigBit> state_sig(GetSize(nodes));
+		vector<SigBit> next_state_sig(GetSize(nodes));
+
+		// Create state signals
+
+		{
+			SigBit not_disable = State::S1;
+
+			if (disable_sig != State::S0)
+				not_disable = module->Not(NEW_ID, disable_sig);
+
+			for (int i = 0; i < GetSize(nodes); i++)
+			{
+				Wire *w = module->addWire(NEW_ID);
+				state_wire[i] = w;
+				state_sig[i] = w;
+
+				if (i == startNode)
+					state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);
+
+				if (disable_sig != State::S0)
+					state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable);
+			}
+		}
+
+		// Follow Links
+
+		{
+			vector<int> node_order(GetSize(nodes));
+			vector<vector<int>> order_to_nodes;
+
+			for (int i = 0; i < GetSize(nodes); i++)
+				make_link_order(node_order, i, 0);
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				if (node_order[i] >= GetSize(order_to_nodes))
+					order_to_nodes.resize(node_order[i]+1);
+				order_to_nodes[node_order[i]].push_back(i);
+			}
+
+			for (int order = 0; order < GetSize(order_to_nodes); order++)
+			for (int node : order_to_nodes[order])
+			{
+				for (auto &it : nodes[node].links)
+				{
+					int target = it.first;
+					SigBit ctrl = state_sig[node];
+
+					if (it.second != State::S1)
+						ctrl = module->And(NEW_ID, ctrl, it.second);
+
+					state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl);
+				}
+			}
+		}
+
+		// Construct activations
+
+		{
+			vector<SigSpec> activate_sig(GetSize(nodes));
+			vector<SigBit> activate_bit(GetSize(nodes));
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				for (auto &it : nodes[i].edges)
+					activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second));
+			}
+
+			for (int i = 0; i < GetSize(nodes); i++) {
+				if (GetSize(activate_sig[i]) == 0)
+					next_state_sig[i] = State::S0;
+				else if (GetSize(activate_sig[i]) == 1)
+					next_state_sig[i] = activate_sig[i];
+				else
+					next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
+			}
+		}
+
+		// Create state FFs
+
+		for (int i = 0; i < GetSize(nodes); i++)
+		{
+			if (next_state_sig[i] != State::S0) {
+				clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], Const(0, 1));
+			} else {
+				module->connect(state_wire[i], State::S0);
+			}
+		}
+
+		final_accept_sig = state_sig[acceptNode];
+		return final_accept_sig;
+	}
+
+	// ----------------------------------------------------
+	// Generating quantifier-based NFSM circuit to acquire reject signal
+
+	SigBit getAnyAllRejectWorker(bool /* allMode */)
+	{
+		// FIXME
+		log_abort();
+	}
+
+	SigBit getAnyReject()
+	{
+		return getAnyAllRejectWorker(false);
+	}
+
+	SigBit getAllReject()
+	{
+		return getAnyAllRejectWorker(true);
+	}
+
+	// ----------------------------------------------------
+	// Generating DFSM circuit to acquire reject signal
+
+	void node_to_unode(int node, int unode, SigSpec ctrl)
+	{
+		if (node == acceptNode)
+			unodes[unode].accept.push_back(ctrl);
+
+		if (node == condNode)
+			unodes[unode].cond.push_back(ctrl);
+
+		for (auto &it : nodes[node].edges) {
+			if (it.second != State::S1) {
+				SigSpec s = {ctrl, it.second};
+				s.sort_and_unify();
+				unodes[unode].edges.push_back(make_pair(it.first, s));
+			} else {
+				unodes[unode].edges.push_back(make_pair(it.first, ctrl));
+			}
+		}
+
+		for (auto &it : nodes[node].links) {
+			if (it.second != State::S1) {
+				SigSpec s = {ctrl, it.second};
+				s.sort_and_unify();
+				node_to_unode(it.first, unode, s);
+			} else {
+				node_to_unode(it.first, unode, ctrl);
+			}
+		}
+	}
+
+	void mark_reachable_unode(int unode)
+	{
+		if (unodes[unode].reachable)
+			return;
+
+		unodes[unode].reachable = true;
+		for (auto &it : unodes[unode].edges)
+			mark_reachable_unode(it.first);
+	}
+
+	void usortint(vector<int> &vec)
+	{
+		vector<int> newvec;
+		std::sort(vec.begin(), vec.end());
+		for (int i = 0; i < GetSize(vec); i++)
+			if (i == GetSize(vec)-1 || vec[i] != vec[i+1])
+				newvec.push_back(vec[i]);
+		vec.swap(newvec);
+	}
+
+	bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl)
+	{
+		for (int i = 0; i < GetSize(ctrl); i++)
+			if (ctrl_bits.count(ctrl[i]) == 0)
+				return false;
+		return true;
+	}
+
+	void create_dnode(const vector<int> &state, bool firstmatch, bool condaccept)
+	{
+		if (dnodes.count(state) != 0)
+			return;
+
+		SvaDFsmNode dnode;
+		dnodes[state] = SvaDFsmNode();
+
+		for (int unode : state) {
+			log_assert(unodes[unode].reachable);
+			for (auto &it : unodes[unode].edges)
+				dnode.ctrl.append(it.second);
+			for (auto &it : unodes[unode].accept)
+				dnode.ctrl.append(it);
+			for (auto &it : unodes[unode].cond)
+				dnode.ctrl.append(it);
+		}
+
+		dnode.ctrl.sort_and_unify();
+
+		if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
+			if (verific_verbose >= 2) {
+				log("    detected state explosion in DFSM generation:\n");
+				dump();
+				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
+			}
+			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
+					GetSize(dnode.ctrl), verific_sva_fsm_limit);
+		}
+
+		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
+		{
+			Const ctrl_val(i, GetSize(dnode.ctrl));
+			pool<SigBit> ctrl_bits;
+
+			for (int i = 0; i < GetSize(dnode.ctrl); i++)
+				if (ctrl_val[i] == State::S1)
+					ctrl_bits.insert(dnode.ctrl[i]);
+
+			vector<int> new_state;
+			bool accept = false, cond = false;
+
+			for (int unode : state) {
+				for (auto &it : unodes[unode].accept)
+					if (cmp_ctrl(ctrl_bits, it))
+						accept = true;
+				for (auto &it : unodes[unode].cond)
+					if (cmp_ctrl(ctrl_bits, it))
+						cond = true;
+			}
+
+			bool new_state_cond = false;
+			bool new_state_noncond = false;
+
+			if (accept && condaccept)
+				accept = cond;
+
+			if (!accept || !firstmatch) {
+				for (int unode : state)
+				for (auto &it : unodes[unode].edges)
+					if (cmp_ctrl(ctrl_bits, it.second)) {
+						if (nodes.at(it.first).is_cond_node)
+							new_state_cond = true;
+						else
+							new_state_noncond = true;
+						new_state.push_back(it.first);
+					}
+			}
+
+			if (accept)
+				dnode.accept.push_back(ctrl_val);
+
+			if (condaccept && (!new_state_cond || !new_state_noncond))
+				new_state.clear();
+
+			if (new_state.empty()) {
+				if (!accept)
+					dnode.reject.push_back(ctrl_val);
+			} else {
+				usortint(new_state);
+				dnode.edges.push_back(make_pair(new_state, ctrl_val));
+				create_dnode(new_state, firstmatch, condaccept);
+			}
+		}
+
+		dnodes[state] = dnode;
+	}
+
+	void optimize_cond(vector<Const> &values)
+	{
+		bool did_something = true;
+
+		while (did_something)
+		{
+			did_something = false;
+
+			for (int i = 0; i < GetSize(values); i++)
+			for (int j = 0; j < GetSize(values); j++)
+			{
+				if (i == j)
+					continue;
+
+				log_assert(GetSize(values[i]) == GetSize(values[j]));
+
+				int delta_pos = -1;
+				bool i_within_j = true;
+				bool j_within_i = true;
+
+				for (int k = 0; k < GetSize(values[i]); k++) {
+					if (values[i][k] == State::Sa && values[j][k] != State::Sa) {
+						i_within_j = false;
+						continue;
+					}
+					if (values[i][k] != State::Sa && values[j][k] == State::Sa) {
+						j_within_i = false;
+						continue;
+					}
+					if (values[i][k] == values[j][k])
+						continue;
+					if (delta_pos >= 0)
+						goto next_pair;
+					delta_pos = k;
+				}
+
+				if (delta_pos >= 0 && i_within_j && j_within_i) {
+					did_something = true;
+					values[i][delta_pos] = State::Sa;
+					values[j] = values.back();
+					values.pop_back();
+					goto next_pair;
+				}
+
+				if (delta_pos < 0 && i_within_j) {
+					did_something = true;
+					values[i] = values.back();
+					values.pop_back();
+					goto next_pair;
+				}
+
+				if (delta_pos < 0 && j_within_i) {
+					did_something = true;
+					values[j] = values.back();
+					values.pop_back();
+					goto next_pair;
+				}
+		next_pair:;
+			}
+		}
+	}
+
+	SigBit make_cond_eq(const SigSpec &ctrl, const Const &value, SigBit enable = State::S1)
+	{
+		SigSpec sig_a, sig_b;
+
+		log_assert(GetSize(ctrl) == GetSize(value));
+
+		for (int i = 0; i < GetSize(ctrl); i++)
+			if (value[i] != State::Sa) {
+				sig_a.append(ctrl[i]);
+				sig_b.append(value[i]);
+			}
+
+		if (GetSize(sig_a) == 0)
+			return enable;
+
+		if (enable != State::S1) {
+			sig_a.append(enable);
+			sig_b.append(State::S1);
+		}
+
+		auto key = make_pair(sig_a, sig_b);
+
+		if (cond_eq_cache.count(key) == 0)
+		{
+			if (sig_b == State::S1)
+				cond_eq_cache[key] = sig_a;
+			else if (sig_b == State::S0)
+				cond_eq_cache[key] = module->Not(NEW_ID, sig_a);
+			else
+				cond_eq_cache[key] = module->Eq(NEW_ID, sig_a, sig_b);
+
+			if (verific_verbose >= 2) {
+				log("    Cond: %s := %s == %s\n", log_signal(cond_eq_cache[key]),
+						log_signal(sig_a), log_signal(sig_b));
+			}
+		}
+
+		return cond_eq_cache.at(key);
+	}
+
+	void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p)
+	{
+		log_assert(!materialized);
+		materialized = true;
+
+		// Create unlinked NFSM
+
+		unodes.resize(GetSize(nodes));
+
+		for (int node = 0; node < GetSize(nodes); node++)
+			node_to_unode(node, node, SigSpec());
+
+		mark_reachable_unode(startNode);
+
+		// Create DFSM
+
+		create_dnode(vector<int>{startNode}, true, false);
+		dnodes.sort();
+
+		// Create DFSM Circuit
+
+		SigSpec accept_sig, reject_sig;
+
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			dnode.ffoutwire = module->addWire(NEW_ID);
+			dnode.statesig = dnode.ffoutwire;
+
+			if (it.first == vector<int>{startNode})
+				dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig);
+		}
+
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			dict<vector<int>, vector<Const>> edge_cond;
+
+			for (auto &edge : dnode.edges)
+				edge_cond[edge.first].push_back(edge.second);
+
+			for (auto &it : edge_cond) {
+				optimize_cond(it.second);
+				for (auto &value : it.second)
+					dnodes.at(it.first).nextstate.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
+			}
+
+			if (accept_p) {
+				vector<Const> accept_cond = dnode.accept;
+				optimize_cond(accept_cond);
+				for (auto &value : accept_cond)
+					accept_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
+			}
+
+			if (reject_p) {
+				vector<Const> reject_cond = dnode.reject;
+				optimize_cond(reject_cond);
+				for (auto &value : reject_cond)
+					reject_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
+			}
+		}
+
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			if (GetSize(dnode.nextstate) == 0) {
+				module->connect(dnode.ffoutwire, State::S0);
+			} else
+			if (GetSize(dnode.nextstate) == 1) {
+				clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0);
+			} else {
+				SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate);
+				clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0);
+			}
+		}
+
+		if (accept_p)
+		{
+			if (GetSize(accept_sig) == 0)
+				final_accept_sig = State::S0;
+			else if (GetSize(accept_sig) == 1)
+				final_accept_sig = accept_sig;
+			else
+				final_accept_sig = module->ReduceOr(NEW_ID, accept_sig);
+			*accept_p = final_accept_sig;
+		}
+
+		if (reject_p)
+		{
+			if (GetSize(reject_sig) == 0)
+				final_reject_sig = State::S0;
+			else if (GetSize(reject_sig) == 1)
+				final_reject_sig = reject_sig;
+			else
+				final_reject_sig = module->ReduceOr(NEW_ID, reject_sig);
+			*reject_p = final_reject_sig;
+		}
+	}
+
+	SigBit getFirstAccept()
+	{
+		SigBit accept;
+		getFirstAcceptReject(&accept, nullptr);
+		return accept;
+	}
+
+	SigBit getReject()
+	{
+		SigBit reject;
+		getFirstAcceptReject(nullptr, &reject);
+		return reject;
+	}
+
+	void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node = -1, bool firstmatch = true, bool condaccept = false)
+	{
+		log_assert(!materialized);
+		materialized = true;
+
+		// Create unlinked NFSM
+
+		unodes.resize(GetSize(nodes));
+
+		for (int node = 0; node < GetSize(nodes); node++)
+			node_to_unode(node, node, SigSpec());
+
+		mark_reachable_unode(startNode);
+
+		// Create DFSM
+
+		create_dnode(vector<int>{startNode}, firstmatch, condaccept);
+		dnodes.sort();
+
+		// Create DFSM Graph
+
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			dnode.outnode = output_fsm.createNode();
+
+			if (it.first == vector<int>{startNode})
+				output_fsm.createLink(output_start_node, dnode.outnode);
+
+			if (output_accept_node >= 0) {
+				vector<Const> accept_cond = dnode.accept;
+				optimize_cond(accept_cond);
+				for (auto &value : accept_cond)
+					output_fsm.createLink(it.second.outnode, output_accept_node, make_cond_eq(dnode.ctrl, value));
+			}
+
+			if (output_reject_node >= 0) {
+				vector<Const> reject_cond = dnode.reject;
+				optimize_cond(reject_cond);
+				for (auto &value : reject_cond)
+					output_fsm.createLink(it.second.outnode, output_reject_node, make_cond_eq(dnode.ctrl, value));
+			}
+		}
+
+		for (auto &it : dnodes)
+		{
+			SvaDFsmNode &dnode = it.second;
+			dict<vector<int>, vector<Const>> edge_cond;
+
+			for (auto &edge : dnode.edges)
+				edge_cond[edge.first].push_back(edge.second);
+
+			for (auto &it : edge_cond) {
+				optimize_cond(it.second);
+				for (auto &value : it.second)
+					output_fsm.createEdge(dnode.outnode, dnodes.at(it.first).outnode, make_cond_eq(dnode.ctrl, value));
+			}
+		}
+	}
+
+	// ----------------------------------------------------
+	// State dump for verbose log messages
+
+	void dump_nodes()
+	{
+		if (nodes.empty())
+			return;
+
+		log("      non-deterministic encoding:\n");
+		for (int i = 0; i < GetSize(nodes); i++)
+		{
+			log("        node %d:%s\n", i,
+					i == startNode ? " [start]" :
+					i == acceptNode ? " [accept]" :
+					i == condNode ? " [cond]" : "");
+
+			for (auto &it : nodes[i].edges) {
+				if (it.second != State::S1)
+					log("          egde %s -> %d\n", log_signal(it.second), it.first);
+				else
+					log("          egde -> %d\n", it.first);
+			}
+
+			for (auto &it : nodes[i].links) {
+				if (it.second != State::S1)
+					log("          link %s -> %d\n", log_signal(it.second), it.first);
+				else
+					log("          link -> %d\n", it.first);
+			}
+		}
+	}
+
+	void dump_unodes()
+	{
+		if (unodes.empty())
+			return;
+
+		log("      unlinked non-deterministic encoding:\n");
+		for (int i = 0; i < GetSize(unodes); i++)
+		{
+			if (!unodes[i].reachable)
+				continue;
+
+			log("        unode %d:%s\n", i, i == startNode ? " [start]" : "");
+
+			for (auto &it : unodes[i].edges) {
+				if (!it.second.empty())
+					log("          egde %s -> %d\n", log_signal(it.second), it.first);
+				else
+					log("          egde -> %d\n", it.first);
+			}
+
+			for (auto &ctrl : unodes[i].accept) {
+				if (!ctrl.empty())
+					log("          accept %s\n", log_signal(ctrl));
+				else
+					log("          accept\n");
+			}
+
+			for (auto &ctrl : unodes[i].cond) {
+				if (!ctrl.empty())
+					log("          cond %s\n", log_signal(ctrl));
+				else
+					log("          cond\n");
+			}
+		}
+	}
+
+	void dump_dnodes()
+	{
+		if (dnodes.empty())
+			return;
+
+		log("      deterministic encoding:\n");
+		for (auto &it : dnodes)
+		{
+			log("        dnode {");
+			for (int i = 0; i < GetSize(it.first); i++)
+				log("%s%d", i ? "," : "", it.first[i]);
+			log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");
+
+			log("          ctrl %s\n", log_signal(it.second.ctrl));
+
+			for (auto &edge : it.second.edges) {
+				log("          edge %s -> {", log_signal(edge.second));
+				for (int i = 0; i < GetSize(edge.first); i++)
+					log("%s%d", i ? "," : "", edge.first[i]);
+				log("}\n");
+			}
+
+			for (auto &value : it.second.accept)
+				log("          accept %s\n", log_signal(value));
+
+			for (auto &value : it.second.reject)
+				log("          reject %s\n", log_signal(value));
+		}
+	}
+
+	void dump()
+	{
+		if (!nodes.empty())
+			log("      number of NFSM states: %d\n", GetSize(nodes));
+
+		if (!unodes.empty()) {
+			int count = 0;
+			for (auto &unode : unodes)
+				if (unode.reachable)
+					count++;
+			log("      number of reachable UFSM states: %d\n", count);
+		}
+
+		if (!dnodes.empty())
+			log("      number of DFSM states: %d\n", GetSize(dnodes));
+
+		if (verific_verbose >= 2) {
+			dump_nodes();
+			dump_unodes();
+			dump_dnodes();
+		}
+
+		if (trigger_sig != State::S1)
+			log("      trigger signal: %s\n", log_signal(trigger_sig));
+
+		if (final_accept_sig != State::Sx)
+			log("      accept signal: %s\n", log_signal(final_accept_sig));
+
+		if (final_reject_sig != State::Sx)
+			log("      reject signal: %s\n", log_signal(final_reject_sig));
+	}
+};
+
+PRIVATE_NAMESPACE_END
+
+YOSYS_NAMESPACE_BEGIN
+
+pool<int> verific_sva_prims = {
+	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
+	PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
+	PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
+	PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
+	PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
+	PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
+	PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
+	PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
+	PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
+	PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
+	PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
+	PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
+	PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
+	PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
+	PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
+	PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
+	PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
+	PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
+	PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
+	PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+};
+
+struct VerificSvaImporter
+{
+	VerificImporter *importer = nullptr;
+	Module *module = nullptr;
+
+	Netlist *netlist = nullptr;
+	Instance *root = nullptr;
+
+	VerificClocking clocking;
+
+	bool mode_assert = false;
+	bool mode_assume = false;
+	bool mode_cover = false;
+	bool mode_trigger = false;
+
+	Instance *net_to_ast_driver(Net *n)
+	{
+		if (n == nullptr)
+			return nullptr;
+
+		if (n->IsMultipleDriven())
+			return nullptr;
+
+		Instance *inst = n->Driver();
+
+		if (inst == nullptr)
+			return nullptr;
+
+		if (!verific_sva_prims.count(inst->Type()))
+			return nullptr;
+
+		if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
+				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE ||
+				inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED)
+			return nullptr;
+
+		return inst;
+	}
+
+	Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
+	Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
+	Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
+	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
+	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+
+	// ----------------------------------------------------------
+	// SVA Importer
+
+	struct ParserErrorException {
+	};
+
+	[[noreturn]] void parser_error(std::string errmsg)
+	{
+		if (!importer->mode_keep)
+			log_error("%s", errmsg.c_str());
+		log_warning("%s", errmsg.c_str());
+		throw ParserErrorException();
+	}
+
+	[[noreturn]] void parser_error(std::string errmsg, linefile_type loc)
+	{
+		parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)));
+	}
+
+	[[noreturn]] void parser_error(std::string errmsg, Instance *inst)
+	{
+		parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
+	}
+
+	[[noreturn]] void parser_error(Instance *inst)
+	{
+		parser_error(stringf("Verific SVA primitive %s (%s) is currently unsupported in this context",
+				inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
+	}
+
+	dict<Net*, bool, hash_ptr_ops> check_expression_cache;
+
+	bool check_expression(Net *net, bool raise_error = false)
+	{
+		while (!check_expression_cache.count(net))
+		{
+			Instance *inst = net_to_ast_driver(net);
+
+			if (inst == nullptr) {
+				check_expression_cache[net] = true;
+				break;
+			}
+
+			if (inst->Type() == PRIM_SVA_AT)
+			{
+				VerificClocking new_clocking(importer, net);
+				log_assert(new_clocking.cond_net == nullptr);
+				if (!clocking.property_matches_sequence(new_clocking))
+					parser_error("Mixed clocking is currently not supported", inst);
+				check_expression_cache[net] = check_expression(new_clocking.body_net, raise_error);
+				break;
+			}
+
+			if (inst->Type() == PRIM_SVA_FIRST_MATCH || inst->Type() == PRIM_SVA_NOT)
+			{
+				check_expression_cache[net] = check_expression(inst->GetInput(), raise_error);
+				break;
+			}
+
+			if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_INTERSECT ||
+					inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT ||
+					inst->Type() == PRIM_SVA_OR || inst->Type() == PRIM_SVA_AND)
+			{
+				check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
+				break;
+			}
+
+			if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
+			{
+				const char *sva_low_s = inst->GetAttValue("sva:low");
+				const char *sva_high_s = inst->GetAttValue("sva:high");
+
+				int sva_low = atoi(sva_low_s);
+				int sva_high = atoi(sva_high_s);
+				bool sva_inf = !strcmp(sva_high_s, "$");
+
+				if (sva_low == 0 && sva_high == 0 && !sva_inf)
+					check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
+				else
+					check_expression_cache[net] = false;
+				break;
+			}
+
+			check_expression_cache[net] = false;
+		}
+
+		if (raise_error && !check_expression_cache.at(net))
+			parser_error(net_to_ast_driver(net));
+		return check_expression_cache.at(net);
+	}
+
+	SigBit parse_expression(Net *net)
+	{
+		check_expression(net, true);
+
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr) {
+			return importer->net_map_at(net);
+		}
+
+		if (inst->Type() == PRIM_SVA_AT)
+		{
+			VerificClocking new_clocking(importer, net);
+			log_assert(new_clocking.cond_net == nullptr);
+			if (!clocking.property_matches_sequence(new_clocking))
+				parser_error("Mixed clocking is currently not supported", inst);
+			return parse_expression(new_clocking.body_net);
+		}
+
+		if (inst->Type() == PRIM_SVA_FIRST_MATCH)
+			return parse_expression(inst->GetInput());
+
+		if (inst->Type() == PRIM_SVA_NOT)
+			return module->Not(NEW_ID, parse_expression(inst->GetInput()));
+
+		if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
+			return module->Or(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));
+
+		if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND || inst->Type() == PRIM_SVA_INTERSECT ||
+				inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_SEQ_CONCAT)
+			return module->And(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));
+
+		log_abort();
+	}
+
+	bool check_zero_consecutive_repeat(Net *net)
+	{
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr)
+			return false;
+
+		if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT)
+			return false;
+
+		const char *sva_low_s = inst->GetAttValue("sva:low");
+		int sva_low = atoi(sva_low_s);
+
+		return sva_low == 0;
+	}
+
+	int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay)
+	{
+		Instance *inst = net_to_ast_driver(net);
+
+		log_assert(inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT);
+
+		const char *sva_low_s = inst->GetAttValue("sva:low");
+		const char *sva_high_s = inst->GetAttValue("sva:high");
+
+		int sva_low = atoi(sva_low_s);
+		int sva_high = atoi(sva_high_s);
+		bool sva_inf = !strcmp(sva_high_s, "$");
+
+		Net *body_net = inst->GetInput();
+
+		if (add_pre_delay || add_post_delay)
+			log_assert(sva_low == 0);
+
+		if (sva_low == 0) {
+			if (!add_pre_delay && !add_post_delay)
+				parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst);
+			sva_low++;
+		}
+
+		int node = fsm.createNode(start_node);
+		start_node = node;
+
+		if (add_pre_delay) {
+			node = fsm.createNode(start_node);
+			fsm.createEdge(start_node, node);
+		}
+
+		int prev_node = node;
+		node = parse_sequence(fsm, node, body_net);
+
+		for (int i = 1; i < sva_low; i++)
+		{
+			int next_node = fsm.createNode();
+			fsm.createEdge(node, next_node);
+
+			prev_node = node;
+			node = parse_sequence(fsm, next_node, body_net);
+		}
+
+		if (sva_inf)
+		{
+			log_assert(prev_node >= 0);
+			fsm.createEdge(node, prev_node);
+		}
+		else
+		{
+			for (int i = sva_low; i < sva_high; i++)
+			{
+				int next_node = fsm.createNode();
+				fsm.createEdge(node, next_node);
+
+				prev_node = node;
+				node = parse_sequence(fsm, next_node, body_net);
+
+				fsm.createLink(prev_node, node);
+			}
+		}
+
+		if (add_post_delay) {
+			int next_node = fsm.createNode();
+			fsm.createEdge(node, next_node);
+			node = next_node;
+		}
+
+		if (add_pre_delay || add_post_delay)
+			fsm.createLink(start_node, node);
+
+		return node;
+	}
+
+	int parse_sequence(SvaFsm &fsm, int start_node, Net *net)
+	{
+		if (check_expression(net)) {
+			int node = fsm.createNode();
+			fsm.createLink(start_node, node, parse_expression(net));
+			return node;
+		}
+
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst->Type() == PRIM_SVA_AT)
+		{
+			VerificClocking new_clocking(importer, net);
+			log_assert(new_clocking.cond_net == nullptr);
+			if (!clocking.property_matches_sequence(new_clocking))
+				parser_error("Mixed clocking is currently not supported", inst);
+			return parse_sequence(fsm, start_node, new_clocking.body_net);
+		}
+
+		if (inst->Type() == PRIM_SVA_FIRST_MATCH)
+		{
+			SvaFsm match_fsm(clocking);
+			match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode);
+
+			int node = fsm.createNode();
+			match_fsm.getDFsm(fsm, start_node, node);
+
+			if (verific_verbose) {
+				log("    First Match FSM:\n");
+				match_fsm.dump();
+			}
+
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
+		{
+			const char *sva_low_s = inst->GetAttValue("sva:low");
+			const char *sva_high_s = inst->GetAttValue("sva:high");
+
+			int sva_low = atoi(sva_low_s);
+			int sva_high = atoi(sva_high_s);
+			bool sva_inf = !strcmp(sva_high_s, "$");
+
+			int node = -1;
+			bool past_add_delay = false;
+
+			if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) {
+				node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true);
+				sva_low--, sva_high--;
+			} else {
+				node = parse_sequence(fsm, start_node, inst->GetInput1());
+			}
+
+			if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) {
+				past_add_delay = true;
+				sva_low--, sva_high--;
+			}
+
+			for (int i = 0; i < sva_low; i++) {
+				int next_node = fsm.createNode();
+				fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+
+			if (sva_inf)
+			{
+				fsm.createEdge(node, node);
+			}
+			else
+			{
+				for (int i = sva_low; i < sva_high; i++)
+				{
+					int next_node = fsm.createNode();
+					fsm.createEdge(node, next_node);
+					fsm.createLink(node, next_node);
+					node = next_node;
+				}
+			}
+
+			if (past_add_delay)
+				node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false);
+			else
+				node = parse_sequence(fsm, node, inst->GetInput2());
+
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
+		{
+			return parse_consecutive_repeat(fsm, start_node, net, false, false);
+		}
+
+		if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT)
+		{
+			const char *sva_low_s = inst->GetAttValue("sva:low");
+			const char *sva_high_s = inst->GetAttValue("sva:high");
+
+			int sva_low = atoi(sva_low_s);
+			int sva_high = atoi(sva_high_s);
+			bool sva_inf = !strcmp(sva_high_s, "$");
+
+			Net *body_net = inst->GetInput();
+			int node = fsm.createNode(start_node);
+
+			SigBit cond = parse_expression(body_net);
+			SigBit not_cond = module->Not(NEW_ID, cond);
+
+			for (int i = 0; i < sva_low; i++)
+			{
+				int wait_node = fsm.createNode();
+				fsm.createEdge(wait_node, wait_node, not_cond);
+
+				if (i == 0)
+					fsm.createLink(node, wait_node);
+				else
+					fsm.createEdge(node, wait_node);
+
+				int next_node = fsm.createNode();
+				fsm.createLink(wait_node, next_node, cond);
+
+				node = next_node;
+			}
+
+			if (sva_inf)
+			{
+				int wait_node = fsm.createNode();
+				fsm.createEdge(wait_node, wait_node, not_cond);
+				fsm.createEdge(node, wait_node);
+				fsm.createLink(wait_node, node, cond);
+			}
+			else
+			{
+				for (int i = sva_low; i < sva_high; i++)
+				{
+					int wait_node = fsm.createNode();
+					fsm.createEdge(wait_node, wait_node, not_cond);
+
+					if (i == 0)
+						fsm.createLink(node, wait_node);
+					else
+						fsm.createEdge(node, wait_node);
+
+					int next_node = fsm.createNode();
+					fsm.createLink(wait_node, next_node, cond);
+
+					fsm.createLink(node, next_node);
+					node = next_node;
+				}
+			}
+
+			if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT)
+				fsm.createEdge(node, node);
+
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
+		{
+			int node = parse_sequence(fsm, start_node, inst->GetInput1());
+			int node2 = parse_sequence(fsm, start_node, inst->GetInput2());
+			fsm.createLink(node2, node);
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND)
+		{
+			SvaFsm fsm1(clocking);
+			fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode);
+
+			SvaFsm fsm2(clocking);
+			fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode);
+
+			SvaFsm combined_fsm(clocking);
+			fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
+			fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
+
+			int node = fsm.createNode();
+			combined_fsm.getDFsm(fsm, start_node, -1, node);
+
+			if (verific_verbose)
+			{
+				log("    Left And FSM:\n");
+				fsm1.dump();
+
+				log("    Right And FSM:\n");
+				fsm1.dump();
+
+				log("    Combined And FSM:\n");
+				combined_fsm.dump();
+			}
+
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN)
+		{
+			SvaFsm intersect_fsm(clocking);
+
+			if (inst->Type() == PRIM_SVA_INTERSECT)
+			{
+				intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode);
+			}
+			else
+			{
+				int n = intersect_fsm.createNode();
+				intersect_fsm.createLink(intersect_fsm.createStartNode(), n);
+				intersect_fsm.createEdge(n, n);
+
+				n = parse_sequence(intersect_fsm, n, inst->GetInput1());
+
+				intersect_fsm.createLink(n, intersect_fsm.acceptNode);
+				intersect_fsm.createEdge(n, n);
+			}
+
+			intersect_fsm.in_cond_mode = true;
+			intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode);
+			intersect_fsm.in_cond_mode = false;
+
+			int node = fsm.createNode();
+			intersect_fsm.getDFsm(fsm, start_node, node, -1, false, true);
+
+			if (verific_verbose) {
+				log("    Intersect FSM:\n");
+				intersect_fsm.dump();
+			}
+
+			return node;
+		}
+
+		if (inst->Type() == PRIM_SVA_THROUGHOUT)
+		{
+			SigBit expr = parse_expression(inst->GetInput1());
+
+			fsm.pushThroughout(expr);
+			int node = parse_sequence(fsm, start_node, inst->GetInput2());
+			fsm.popThroughout();
+
+			return node;
+		}
+
+		parser_error(inst);
+	}
+
+	void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accept_reject = false)
+	{
+		log_assert(accept_p != nullptr || reject_p != nullptr);
+
+		if (swap_accept_reject)
+			get_fsm_accept_reject(fsm, reject_p, accept_p);
+		else if (reject_p == nullptr)
+			*accept_p = fsm.getAccept();
+		else if (accept_p == nullptr)
+			*reject_p = fsm.getReject();
+		else
+			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 == nullptr)
+				return false;
+
+			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);
+
+		SigBit trig = State::S1;
+
+		if (clocking.cond_net != nullptr)
+			trig = importer->net_map_at(clocking.cond_net);
+
+		if (inst == nullptr)
+		{
+			log_assert(trig == State::S1);
+
+			if (accept_p != nullptr)
+				*accept_p = importer->net_map_at(net);
+			if (reject_p != nullptr)
+				*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
+		}
+		else
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			Net *antecedent_net = inst->GetInput1();
+			Net *consequent_net = inst->GetInput2();
+			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;
+			}
+
+			Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+			if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
+					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
+			{
+				bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+
+				Net *until_net = consequent_inst->GetInput2();
+				consequent_net = consequent_inst->GetInput1();
+				consequent_inst = net_to_ast_driver(consequent_net);
+
+				SigBit until_sig = parse_expression(until_net);
+				SigBit not_until_sig = module->Not(NEW_ID, until_sig);
+				antecedent_fsm.createEdge(node, node, not_until_sig);
+
+				antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig);
+			}
+			else
+			{
+				antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+			}
+
+			SigBit antecedent_match = antecedent_fsm.getAccept();
+
+			if (verific_verbose) {
+				log("    Antecedent FSM:\n");
+				antecedent_fsm.dump();
+			}
+
+			bool consequent_not = false;
+			if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
+				consequent_not = true;
+				consequent_net = consequent_inst->GetInput();
+				consequent_inst = net_to_ast_driver(consequent_net);
+			}
+
+			SvaFsm consequent_fsm(clocking, antecedent_match);
+			node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net);
+			consequent_fsm.createLink(node, consequent_fsm.acceptNode);
+
+			get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not);
+
+			if (verific_verbose) {
+				log("    Consequent FSM:\n");
+				consequent_fsm.dump();
+			}
+		}
+		else
+		{
+			bool prop_not = inst->Type() == PRIM_SVA_NOT;
+			if (prop_not) {
+				net = inst->GetInput();
+				inst = net_to_ast_driver(net);
+			}
+
+			SvaFsm fsm(clocking, trig);
+			int node = parse_sequence(fsm, fsm.createStartNode(), net);
+			fsm.createLink(node, fsm.acceptNode);
+
+			get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not);
+
+			if (verific_verbose) {
+				log("    Sequence FSM:\n");
+				fsm.dump();
+			}
+		}
+	}
+
+	void import()
+	{
+		try
+		{
+			module = importer->module;
+			netlist = root->Owner();
+
+			if (verific_verbose)
+				log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
+						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
+
+			RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+
+			// parse SVA sequence into trigger signal
+
+			clocking = VerificClocking(importer, root->GetInput(), true);
+			SigBit accept_bit = State::S0, reject_bit = State::S0;
+
+			if (clocking.body_net == nullptr)
+			{
+				if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr ||  clocking.cond_net != nullptr)
+					parser_error(stringf("Failed to parse SVA clocking"), root);
+
+				if (mode_assert || mode_assume) {
+					reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
+				} else {
+					accept_bit = parse_expression(root->GetInput());
+				}
+			}
+			else
+			{
+				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);
+					}
+				}
+			}
+
+			if (mode_trigger)
+			{
+				module->connect(importer->net_map_at(root->GetOutput()), accept_bit);
+			}
+			else
+			{
+				SigBit sig_a = module->Not(NEW_ID, reject_bit);
+				SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit);
+
+				// 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 assert/assume/cover cell
+
+				RTLIL::Cell *c = nullptr;
+
+				if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q);
+				if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q);
+				if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q);
+
+				importer->import_attributes(c->attributes, root);
+			}
+		}
+		catch (ParserErrorException)
+		{
+		}
+	}
+};
+
+void verific_import_sva_assert(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assert = true;
+	worker.import();
+}
+
+void verific_import_sva_assume(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assume = true;
+	worker.import();
+}
+
+void verific_import_sva_cover(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_cover = true;
+	worker.import();
+}
+
+void verific_import_sva_trigger(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_trigger = true;
+	worker.import();
+}
+
+bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	return worker.net_to_ast_driver(net) != nullptr;
+}
+
+YOSYS_NAMESPACE_END