Move Verific SVA importer to extra C++ source file

Signed-off-by: Clifford Wolf <clifford@clifford.at>

4 files changed, 1370 insertions, 1279 deletions

diff --git a/frontends/verific/Makefile.inc b/frontends/verific/Makefile.inc
index debaac0c5..972f4f9f1 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:
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 12f572ae2..4925389ae 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -29,6 +29,8 @@
 #  include <dirent.h>
 #endif
 
+#include "frontends/verific/verific.h"
+
 USING_YOSYS_NAMESPACE
 
 #ifdef YOSYS_ENABLE_VERIFIC
@@ -43,7 +45,6 @@ USING_YOSYS_NAMESPACE
 #include "VeriModule.h"
 #include "VeriWrite.h"
 #include "VhdlUnits.h"
-#include "DataBase.h"
 #include "Message.h"
 
 #ifdef __clang__
@@ -51,14 +52,13 @@ USING_YOSYS_NAMESPACE
 #endif
 
 #ifdef VERIFIC_NAMESPACE
-using namespace Verific ;
+using namespace Verific;
 #endif
 
 #endif
 
-PRIVATE_NAMESPACE_BEGIN
-
 #ifdef YOSYS_ENABLE_VERIFIC
+YOSYS_NAMESPACE_BEGIN
 
 pool<int> verific_sva_prims = {
 	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
@@ -118,1529 +118,1152 @@ string get_full_netlist_name(Netlist *nl)
 	return nl->CellBaseName();
 }
 
-struct VerificImporter;
-void import_sva_assert(VerificImporter *importer, Instance *inst);
-void import_sva_assume(VerificImporter *importer, Instance *inst);
-void import_sva_cover(VerificImporter *importer, Instance *inst);
-void svapp_assert(Instance *inst);
-void svapp_assume(Instance *inst);
-void svapp_cover(Instance *inst);
-
-struct VerificClockEdge {
-	Net *clock_net = nullptr;
-	SigBit clock_sig = State::Sx;
-	bool posedge = false;
-	VerificClockEdge(VerificImporter *importer, Instance *inst);
-};
+// ==================================================================
 
-struct VerificImporter
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
+		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+		mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
 {
-	RTLIL::Module *module;
-	Netlist *netlist;
+}
 
-	std::map<Net*, RTLIL::SigBit> net_map;
-	std::map<Net*, Net*> sva_posedge_map;
+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());
 
-	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
+	return net_map.at(net);
+}
 
-	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
-			mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
-			mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
-	{
-	}
+void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+{
+	MapIter mi;
+	Att *attr;
 
-	RTLIL::SigBit 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());
+	if (obj->Linefile())
+		attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
 
-		return net_map.at(net);
-	}
+	// FIXME: Parse numeric attributes
+	FOREACH_ATTRIBUTE(obj, mi, attr)
+		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+}
 
-	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
-	{
-		MapIter mi;
-		Att *attr;
+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)));
+		else
+			sig.append(RTLIL::State::Sz);
+	return sig;
+}
 
-		if (obj->Linefile())
-			attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
+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)));
+		else
+			sig.append(RTLIL::State::Sz);
+	return sig;
+}
 
-		// FIXME: Parse numeric attributes
-		FOREACH_ATTRIBUTE(obj, mi, attr)
-			attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
-	}
+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)));
+		else
+			sig.append(RTLIL::State::Sz);
+	return sig;
+}
 
-	RTLIL::SigSpec operatorInput(Instance *inst)
-	{
+RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
+{
+	PortBus *portbus = inst->View()->GetPortBus(portname);
+	if (portbus) {
 		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)));
-			else
+		for (unsigned i = 0; i < portbus->Size(); i++) {
+			Net *net = inst->GetNet(portbus->ElementAtIndex(i));
+			if (net) {
+				if (net->IsGnd())
+					sig.append(RTLIL::State::S0);
+				else if (net->IsPwr())
+					sig.append(RTLIL::State::S1);
+				else
+					sig.append(net_map_at(net));
+			} else
 				sig.append(RTLIL::State::Sz);
+		}
 		return sig;
+	} else {
+		Port *port = inst->View()->GetPort(portname);
+		log_assert(port != NULL);
+		Net *net = inst->GetNet(port);
+		return net_map_at(net);
 	}
+}
 
-	RTLIL::SigSpec 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)));
+RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
+{
+	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)));
+			dummy_wire = NULL;
+		} else {
+			if (dummy_wire == NULL)
+				dummy_wire = module->addWire(NEW_ID);
 			else
-				sig.append(RTLIL::State::Sz);
-		return sig;
-	}
+				dummy_wire->width++;
+			sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
+		}
+	return sig;
+}
 
-	RTLIL::SigSpec 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)));
-			else
-				sig.append(RTLIL::State::Sz);
-		return sig;
+bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
+{
+	if (inst->Type() == PRIM_AND) {
+		module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		return true;
 	}
 
-	RTLIL::SigSpec operatorInport(Instance *inst, const char *portname)
-	{
-		PortBus *portbus = inst->View()->GetPortBus(portname);
-		if (portbus) {
-			RTLIL::SigSpec sig;
-			for (unsigned i = 0; i < portbus->Size(); i++) {
-				Net *net = inst->GetNet(portbus->ElementAtIndex(i));
-				if (net) {
-					if (net->IsGnd())
-						sig.append(RTLIL::State::S0);
-					else if (net->IsPwr())
-						sig.append(RTLIL::State::S1);
-					else
-						sig.append(net_map_at(net));
-				} else
-					sig.append(RTLIL::State::Sz);
-			}
-			return sig;
-		} else {
-			Port *port = inst->View()->GetPort(portname);
-			log_assert(port != NULL);
-			Net *net = inst->GetNet(port);
-			return net_map_at(net);
-		}
+	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(inst_name, tmp, net_map_at(inst->GetOutput()));
+		return true;
 	}
 
-	RTLIL::SigSpec operatorOutput(Instance *inst)
-	{
-		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)));
-				dummy_wire = NULL;
-			} else {
-				if (dummy_wire == NULL)
-					dummy_wire = module->addWire(NEW_ID);
-				else
-					dummy_wire->width++;
-				sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
-			}
-		return sig;
+	if (inst->Type() == PRIM_OR) {
+		module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		return true;
 	}
 
-	bool import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
-	{
-		if (inst->Type() == PRIM_AND) {
-			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(inst_name, tmp, net_map_at(inst->GetOutput()));
-			return true;
-		}
-
-		if (inst->Type() == PRIM_OR) {
-			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(inst_name, tmp, 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(inst_name, tmp, net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_XOR) {
+		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_XOR) {
-			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(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(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(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		return true;
+	}
 
-		if (inst->Type() == PRIM_BUF) {
-			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_INV) {
+		module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		return true;
+	}
 
-		if (inst->Type() == PRIM_INV) {
-			module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_MUX) {
+		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_MUX) {
-			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(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_TRI) {
-			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 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(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);
+		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 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(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);
-			return true;
-		}
+	if (inst->Type() == PRIM_DFFRS)
+	{
+		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+			module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		else if (inst->GetSet()->IsGnd())
+			module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
+		else if (inst->GetReset()->IsGnd())
+			module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
+					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
+		else
+			module->addDffsrGate(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()));
+		return true;
+	}
 
-		if (inst->Type() == PRIM_DFFRS)
-		{
-			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-				module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			else if (inst->GetSet()->IsGnd())
-				module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
-						net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
-			else if (inst->GetReset()->IsGnd())
-				module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
-						net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
-			else
-				module->addDffsrGate(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()));
-			return true;
-		}
+	return false;
+}
 
-		return false;
+bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
+{
+	if (inst->Type() == PRIM_AND) {
+		module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		return true;
 	}
 
-	bool import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
-	{
-		if (inst->Type() == PRIM_AND) {
-			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(inst_name, tmp, 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(inst_name, tmp, net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_OR) {
+		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_OR) {
-			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(inst_name, tmp, 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(inst_name, tmp, net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_XOR) {
+		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_XOR) {
-			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(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(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(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		return true;
+	}
 
-		if (inst->Type() == PRIM_INV) {
-			module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			return true;
-		}
+	if (inst->Type() == PRIM_MUX) {
+		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_MUX) {
-			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(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_TRI) {
-			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);
+		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(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
+		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);
-			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(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
-			return true;
-		}
+	if (inst->Type() == PRIM_DFFRS)
+	{
+		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+			module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		else if (inst->GetSet()->IsGnd())
+			module->addAdff(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);
+		else if (inst->GetReset()->IsGnd())
+			module->addAdff(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);
+		else
+			module->addDffsr(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()));
+		return true;
+	}
 
-		if (inst->Type() == PRIM_DFFRS)
-		{
-			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-				module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			else if (inst->GetSet()->IsGnd())
-				module->addAdff(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);
-			else if (inst->GetReset()->IsGnd())
-				module->addAdff(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);
-			else
-				module->addDffsr(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()));
-			return true;
-		}
+	if (inst->Type() == PRIM_DLATCHRS)
+	{
+		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+			module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		else
+			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;
+	}
 
-		if (inst->Type() == PRIM_DLATCHRS)
-		{
-			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-				module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-			else
-				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)
+	#define IN1 operatorInput1(inst)
+	#define IN2 operatorInput2(inst)
+	#define OUT operatorOutput(inst)
+	#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()));
+		if (inst->GetCin()->IsGnd()) {
+			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(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
 		}
+		return true;
+	}
 
-		#define IN  operatorInput(inst)
-		#define IN1 operatorInput1(inst)
-		#define IN2 operatorInput2(inst)
-		#define OUT operatorOutput(inst)
-		#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()));
-			if (inst->GetCin()->IsGnd()) {
-				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(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
-			}
-			return true;
-		}
+	if (inst->Type() == OPER_MULTIPLIER) {
+		module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_MULTIPLIER) {
-			module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_DIVIDER) {
+		module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_DIVIDER) {
-			module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_MODULO) {
+		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_MODULO) {
-			module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_REMAINDER) {
+		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_REMAINDER) {
-			module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_SHIFT_LEFT) {
+		module->addShl(inst_name, IN1, IN2, OUT, false);
+		return true;
+	}
 
-		if (inst->Type() == OPER_SHIFT_LEFT) {
-			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()));
+		for (unsigned i = 1; i < inst->OutputSize(); i++) {
+			vec.append(RTLIL::State::S0);
 		}
+		module->addShl(inst_name, vec, IN, OUT, false);
+		return true;
+	}
 
-		if (inst->Type() == OPER_ENABLED_DECODER) {
-			RTLIL::SigSpec vec;
-			vec.append(net_map_at(inst->GetControl()));
-			for (unsigned i = 1; i < inst->OutputSize(); i++) {
-				vec.append(RTLIL::State::S0);
-			}
-			module->addShl(inst_name, vec, IN, OUT, false);
-			return true;
+	if (inst->Type() == OPER_DECODER) {
+		RTLIL::SigSpec vec;
+		vec.append(RTLIL::State::S1);
+		for (unsigned i = 1; i < inst->OutputSize(); i++) {
+			vec.append(RTLIL::State::S0);
 		}
+		module->addShl(inst_name, vec, IN, OUT, false);
+		return true;
+	}
 
-		if (inst->Type() == OPER_DECODER) {
-			RTLIL::SigSpec vec;
-			vec.append(RTLIL::State::S1);
-			for (unsigned i = 1; i < inst->OutputSize(); i++) {
-				vec.append(RTLIL::State::S0);
-			}
-			module->addShl(inst_name, vec, IN, OUT, false);
-			return true;
-		}
+	if (inst->Type() == OPER_SHIFT_RIGHT) {
+		Net *net_cin = inst->GetCin();
+		Net *net_a_msb = inst->GetInput1Bit(0);
+		if (net_cin->IsGnd())
+			module->addShr(inst_name, IN1, IN2, OUT, false);
+		else if (net_cin == net_a_msb)
+			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_SHIFT_RIGHT) {
-			Net *net_cin = inst->GetCin();
-			Net *net_a_msb = inst->GetInput1Bit(0);
-			if (net_cin->IsGnd())
-				module->addShr(inst_name, IN1, IN2, OUT, false);
-			else if (net_cin == net_a_msb)
-				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(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_REDUCE_AND) {
-			module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_REDUCE_OR) {
+		module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_REDUCE_OR) {
-			module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_REDUCE_XOR) {
+		module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_REDUCE_XOR) {
-			module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_REDUCE_XNOR) {
+		module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_REDUCE_XNOR) {
-			module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_LESSTHAN) {
+		Net *net_cin = inst->GetCin();
+		if (net_cin->IsGnd())
+			module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		else if (net_cin->IsPwr())
+			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_LESSTHAN) {
-			Net *net_cin = inst->GetCin();
-			if (net_cin->IsGnd())
-				module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
-			else if (net_cin->IsPwr())
-				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(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_AND) {
-			module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_OR) {
+		module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_OR) {
-			module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_XOR) {
+		module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_XOR) {
-			module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_XNOR) {
+		module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_XNOR) {
-			module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_BUF) {
+		module->addPos(inst_name, IN, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_BUF) {
-			module->addPos(inst_name, IN, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_INV) {
+		module->addNot(inst_name, IN, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_INV) {
-			module->addNot(inst_name, IN, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_MINUS) {
+		module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_MINUS) {
-			module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_UMINUS) {
+		module->addNeg(inst_name, IN, OUT, SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_UMINUS) {
-			module->addNeg(inst_name, IN, OUT, SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_EQUAL) {
+		module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_EQUAL) {
-			module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_NEQUAL) {
+		module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		return true;
+	}
 
-		if (inst->Type() == OPER_NEQUAL) {
-			module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_MUX) {
+		module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_MUX) {
-			module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
-			return true;
-		}
+	if (inst->Type() == OPER_WIDE_TRI) {
+		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_TRI) {
-			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");
+		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(inst_name, net_map_at(inst->GetClock()), IN, OUT);
+		else
+			module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
+		return true;
+	}
 
-		if (inst->Type() == OPER_WIDE_DFFRS) {
-			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(inst_name, net_map_at(inst->GetClock()), IN, OUT);
-			else
-				module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
-			return true;
-		}
+	#undef IN
+	#undef IN1
+	#undef IN2
+	#undef OUT
+	#undef SIGNED
 
-		#undef IN
-		#undef IN1
-		#undef IN2
-		#undef OUT
-		#undef SIGNED
+	return false;
+}
 
-		return false;
-	}
+void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
+{
+	bool keep_running = true;
+	SigMap sigmap;
 
-	void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
+	while (keep_running)
 	{
-		bool keep_running = true;
-		SigMap sigmap;
-
-		while (keep_running)
-		{
-			keep_running = false;
+		keep_running = false;
 
-			dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
-			SigSpec dbits;
+		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);
-			}
+		for (auto cell : candidates) {
+			SigBit bit = sigmap(cell->getPort("\\D"));
+			dbits_db[bit].insert(cell);
+			dbits.append(bit);
+		}
 
-			dbits.sort_and_unify();
+		dbits.sort_and_unify();
 
-			for (auto chunk : dbits.chunks())
-			{
-				SigSpec sig_d = chunk;
+		for (auto chunk : dbits.chunks())
+		{
+			SigSpec sig_d = chunk;
 
-				if (chunk.wire == nullptr || GetSize(sig_d) == 1)
-					continue;
+			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);
+			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 (verbose)
-					log("  merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
+			if (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 (verbose)
-							log("    replacing old ff %s on bit %d.\n", log_id(old_ff), i);
+			for (int i = 0; i < GetSize(sig_d); i++)
+				for (auto old_ff : dbits_db[sig_d[i]])
+				{
+					if (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];
+					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;
-					}
-			}
+					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;
 
-	void merge_past_ffs(pool<RTLIL::Cell*> &candidates)
+	for (auto cell : candidates)
 	{
-		dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
+		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 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);
+}
 
-		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());
 
-	void 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;
 
-		netlist = nl;
+	if (design->has(module_name)) {
+		if (!nl->IsOperator())
+			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+		return;
+	}
 
-		if (design->has(module_name)) {
-			if (!nl->IsOperator())
-				log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
-			return;
-		}
+	module = new RTLIL::Module;
+	module->name = module_name;
+	design->add(module);
 
-		module = new RTLIL::Module;
-		module->name = module_name;
-		design->add(module);
+	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));
+	}
 
-		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;
+	Port *port;
+	PortBus *portbus;
+	Net *net;
+	NetBus *netbus;
+	Instance *inst;
+	PortRef *pr;
 
-		SetIter si;
-		MapIter mi, mi2;
-		Port *port;
-		PortBus *portbus;
-		Net *net;
-		NetBus *netbus;
-		Instance *inst;
-		PortRef *pr;
+	if (!mode_nosvapp)
+	{
+		vector<Instance*> asserts, assumes, covers;
 
-		if (!mode_nosvapp)
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
 		{
-			vector<Instance*> asserts, assumes, covers;
+			if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
+				asserts.push_back(inst);
 
-			FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
-			{
-				if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
-					asserts.push_back(inst);
+			if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
+				assumes.push_back(inst);
 
-				if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
-					assumes.push_back(inst);
+			if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
+				covers.push_back(inst);
+		}
 
-				if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
-					covers.push_back(inst);
-			}
+		for (auto inst : asserts)
+			svapp_assert(inst);
 
-			for (auto inst : asserts)
-				svapp_assert(inst);
+		for (auto inst : assumes)
+			svapp_assume(inst);
 
-			for (auto inst : assumes)
-				svapp_assume(inst);
+		for (auto inst : covers)
+			svapp_cover(inst);
+	}
 
-			for (auto inst : covers)
-				svapp_cover(inst);
-		}
+	FOREACH_PORT_OF_NETLIST(nl, mi, port)
+	{
+		if (port->Bus())
+			continue;
 
-		FOREACH_PORT_OF_NETLIST(nl, mi, port)
-		{
-			if (port->Bus())
-				continue;
+		if (verbose)
+			log("  importing port %s.\n", port->Name());
 
-			if (verbose)
-				log("  importing port %s.\n", port->Name());
+		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
+		import_attributes(wire->attributes, port);
 
-			RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
-			import_attributes(wire->attributes, port);
+		wire->port_id = nl->IndexOf(port) + 1;
 
-			wire->port_id = nl->IndexOf(port) + 1;
+		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
+			wire->port_input = true;
+		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
+			wire->port_output = true;
 
-			if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
-				wire->port_input = true;
-			if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
-				wire->port_output = true;
+		if (port->GetNet()) {
+			net = port->GetNet();
+			if (net_map.count(net) == 0)
+				net_map[net] = wire;
+			else if (wire->port_input)
+				module->connect(net_map_at(net), wire);
+			else
+				module->connect(wire, net_map_at(net));
+		}
+	}
 
-			if (port->GetNet()) {
-				net = port->GetNet();
+	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
+	{
+		if (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());
+		import_attributes(wire->attributes, portbus);
+
+		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
+			wire->port_input = true;
+		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
+			wire->port_output = true;
+
+		for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
+			if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
+				net = portbus->ElementAtIndex(i)->GetNet();
+				RTLIL::SigBit bit(wire, i - wire->start_offset);
 				if (net_map.count(net) == 0)
-					net_map[net] = wire;
+					net_map[net] = bit;
 				else if (wire->port_input)
-					module->connect(net_map_at(net), wire);
+					module->connect(net_map_at(net), bit);
 				else
-					module->connect(wire, net_map_at(net));
+					module->connect(bit, net_map_at(net));
 			}
+			if (i == portbus->RightIndex())
+				break;
 		}
+	}
 
-		FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
-		{
-			if (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());
-			import_attributes(wire->attributes, portbus);
+	module->fixup_ports();
 
-			if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
-				wire->port_input = true;
-			if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
-				wire->port_output = true;
+	dict<Net*, char, hash_ptr_ops> init_nets;
+	pool<Net*, hash_ptr_ops> anyconst_nets;
+	pool<Net*, hash_ptr_ops> anyseq_nets;
 
-			for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
-				if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
-					net = portbus->ElementAtIndex(i)->GetNet();
-					RTLIL::SigBit bit(wire, i - wire->start_offset);
-					if (net_map.count(net) == 0)
-						net_map[net] = bit;
-					else if (wire->port_input)
-						module->connect(net_map_at(net), bit);
-					else
-						module->connect(bit, net_map_at(net));
+	FOREACH_NET_OF_NETLIST(nl, mi, net)
+	{
+		if (net->IsRamNet())
+		{
+			RTLIL::Memory *memory = new RTLIL::Memory;
+			memory->name = RTLIL::escape_id(net->Name());
+			log_assert(module->count_id(memory->name) == 0);
+			module->memories[memory->name] = memory;
+
+			int number_of_bits = net->Size();
+			int bits_in_word = number_of_bits;
+			FOREACH_PORTREF_OF_NET(net, si, pr) {
+				if (pr->GetInst()->Type() == OPER_READ_PORT) {
+					bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
+					continue;
 				}
-				if (i == portbus->RightIndex())
-					break;
+				if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
+					bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
+					continue;
+				}
+				log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
+						net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
 			}
-		}
 
-		module->fixup_ports();
-
-		dict<Net*, char, hash_ptr_ops> init_nets;
-		pool<Net*, hash_ptr_ops> anyconst_nets;
-		pool<Net*, hash_ptr_ops> anyseq_nets;
-
-		FOREACH_NET_OF_NETLIST(nl, mi, net)
-		{
-			if (net->IsRamNet())
-			{
-				RTLIL::Memory *memory = new RTLIL::Memory;
-				memory->name = RTLIL::escape_id(net->Name());
-				log_assert(module->count_id(memory->name) == 0);
-				module->memories[memory->name] = memory;
-
-				int number_of_bits = net->Size();
-				int bits_in_word = number_of_bits;
-				FOREACH_PORTREF_OF_NET(net, si, pr) {
-					if (pr->GetInst()->Type() == OPER_READ_PORT) {
-						bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
-						continue;
-					}
-					if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
-						bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
-						continue;
-					}
-					log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
-							net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
+			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++;
 				}
-
-				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');
+				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++;
 					}
-					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);
-						}
+					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;
 			}
+			continue;
+		}
 
-			if (net->GetInitialValue())
-				init_nets[net] = net->GetInitialValue();
+		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 *rand_const_attr = net->GetAttValue(" rand_const");
+		const char *rand_attr = net->GetAttValue(" rand");
 
-			if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
-				anyconst_nets.insert(net);
+		if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
+			anyconst_nets.insert(net);
 
-			else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
-				anyseq_nets.insert(net);
+		else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
+			anyseq_nets.insert(net);
 
-			if (net_map.count(net)) {
-				if (verbose)
-					log("  skipping net %s.\n", net->Name());
-				continue;
-			}
+		if (net_map.count(net)) {
+			if (verbose)
+				log("  skipping net %s.\n", net->Name());
+			continue;
+		}
 
-			if (net->Bus())
-				continue;
+		if (net->Bus())
+			continue;
 
-			RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
+		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
 
-			if (verbose)
-				log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));
+		if (verbose)
+			log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));
 
-			RTLIL::Wire *wire = module->addWire(wire_name);
-			import_attributes(wire->attributes, net);
+		RTLIL::Wire *wire = module->addWire(wire_name);
+		import_attributes(wire->attributes, net);
 
-			net_map[net] = wire;
+		net_map[net] = wire;
+	}
+
+	FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
+	{
+		bool found_new_net = false;
+		for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
+			net = netbus->ElementAtIndex(i);
+			if (net_map.count(net) == 0)
+				found_new_net = true;
+			if (i == netbus->RightIndex())
+				break;
 		}
 
-		FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
+		if (found_new_net)
 		{
-			bool found_new_net = false;
-			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
-				net = netbus->ElementAtIndex(i);
-				if (net_map.count(net) == 0)
-					found_new_net = true;
-				if (i == netbus->RightIndex())
-					break;
-			}
-
-			if (found_new_net)
-			{
-				RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
+			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
 
-				if (verbose)
-					log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
+			if (verbose)
+				log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
 
-				RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
-				wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
-				import_attributes(wire->attributes, netbus);
+			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
+			wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
+			import_attributes(wire->attributes, netbus);
 
-				RTLIL::Const initval = Const(State::Sx, GetSize(wire));
-				bool initval_valid = false;
+			RTLIL::Const initval = Const(State::Sx, GetSize(wire));
+			bool initval_valid = false;
 
-				for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
+			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
+			{
+				if (netbus->ElementAtIndex(i))
 				{
-					if (netbus->ElementAtIndex(i))
-					{
-						int bitidx = i - wire->start_offset;
-						net = netbus->ElementAtIndex(i);
-						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));
+					int bitidx = i - wire->start_offset;
+					net = netbus->ElementAtIndex(i);
+					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 (i == netbus->RightIndex())
-						break;
+					if (net_map.count(net) == 0)
+						net_map[net] = bit;
+					else
+						module->connect(bit, net_map_at(net));
 				}
 
-				if (initval_valid)
-					wire->attributes["\\init"] = initval;
-			}
-			else
-			{
-				if (verbose)
-					log("  skipping netbus %s.\n", netbus->Name());
-			}
-
-			SigSpec anyconst_sig;
-			SigSpec anyseq_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 (i == netbus->LeftIndex())
+				if (i == netbus->RightIndex())
 					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 (initval_valid)
+				wire->attributes["\\init"] = initval;
 		}
-
-		for (auto it : init_nets)
+		else
 		{
-			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<RTLIL::Cell*> past_ffs;
-
-		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
-		{
-			RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
-
 			if (verbose)
-				log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
-
-			if (inst->Type() == PRIM_PWR) {
-				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);
-				continue;
-			}
-
-			if (inst->Type() == PRIM_BUF) {
-				module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
-				continue;
-			}
-
-			if (inst->Type() == PRIM_X) {
-				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);
-				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());
-
-				RTLIL::SigSpec addr = operatorInput1(inst);
-				RTLIL::SigSpec data = operatorOutput(inst);
-
-				RTLIL::Cell *cell = module->addCell(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);
-				continue;
-			}
-
-			if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
-			{
-				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());
-
-				RTLIL::SigSpec addr = operatorInput1(inst);
-				RTLIL::SigSpec data = operatorInput2(inst);
-
-				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("\\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()));
-				}
-				continue;
-			}
-
-			if (!mode_gates) {
-				if (import_netlist_instance_cells(inst, inst_name))
-					continue;
-				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(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() == OPER_SVA_STABLE && !mode_nosva)
-			{
-				VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
-
-				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 (verbose) {
-					log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
-							log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
-					log("    XNOR with A=%s, B=%s, Y=%s.\n",
-							log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
-				}
-
-				module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
-				module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
-
-				if (!mode_keep)
-					continue;
-			}
-
-			if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
-			{
-				VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
-
-				SigSpec sig_d = net_map_at(inst->GetInput1());
-				SigSpec sig_o = net_map_at(inst->GetOutput());
-				SigSpec sig_q = module->addWire(NEW_ID);
-
-				if (verbose) {
-					log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
-							log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
-					log("    XNOR with A=%s, B=%s, Y=%s.\n",
-							log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
-				}
-
-				module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
-				module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
-
-				if (!mode_keep)
-					continue;
-			}
-
-			if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
-			{
-				VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
-
-				SigBit sig_d = net_map_at(inst->GetInput1());
-				SigBit sig_q = net_map_at(inst->GetOutput());
-
-				if (verbose)
-					log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
-							log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
-
-				past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge));
-
-				if (!mode_keep)
-					continue;
-			}
-
-			if (!mode_keep && verific_sva_prims.count(inst->Type())) {
-				if (verbose)
-					log("    skipping SVA cell in non k-mode\n");
-				continue;
-			}
-
-			if (inst->IsPrimitive())
-			{
-				if (inst->Type() == PRIM_HDL_ASSERTION)
-					continue;
+				log("  skipping netbus %s.\n", netbus->Name());
+		}
 
-				if (!mode_keep)
-					log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+		SigSpec anyconst_sig;
+		SigSpec anyseq_sig;
 
-				if (!verific_sva_prims.count(inst->Type()))
-					log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+		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);
 			}
-
-			nl_todo.insert(inst->View());
-
-			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 (verbose)
-				log("    ports in verific db:\n");
-
-			FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
-				if (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()) {
-					port_name = pr->GetPort()->Bus()->Name();
-					port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
-							min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
-				}
-				IdString port_name_id = RTLIL::escape_id(port_name);
-				auto &sigvec = cell_port_conns[port_name_id];
-				if (GetSize(sigvec) <= port_offset) {
-					SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
-					for (auto bit : zwires)
-						sigvec.push_back(bit);
-				}
-				sigvec[port_offset] = net_map_at(pr->GetNet());
-			}
-
-			if (verbose)
-				log("    ports in yosys db:\n");
-
-			for (auto &it : cell_port_conns) {
-				if (verbose)
-					log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
-				cell->setPort(it.first, it.second);
+			if (net != nullptr && anyseq_nets.count(net)) {
+				anyseq_sig.append(net_map_at(net));
+				anyseq_nets.erase(net);
 			}
+			if (i == netbus->LeftIndex())
+				break;
 		}
 
-		if (!mode_nosva)
-		{
-			for (auto inst : sva_asserts)
-				import_sva_assert(this, inst);
-
-			for (auto inst : sva_assumes)
-				import_sva_assume(this, inst);
+		if (GetSize(anyconst_sig))
+			module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
 
-			for (auto inst : sva_covers)
-				import_sva_cover(this, inst);
-
-			merge_past_ffs(past_ffs);
-		}
+		if (GetSize(anyseq_sig))
+			module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
 	}
-};
-
-VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
-{
-	log_assert(importer != nullptr);
-	log_assert(inst != nullptr);
 
-	// SVA posedge/negedge
-	if (inst->Type() == PRIM_SVA_POSEDGE)
+	for (auto it : init_nets)
 	{
-		clock_net = inst->GetInput();
-		posedge = true;
+		Const initval;
+		SigBit bit = net_map_at(it.first);
+		log_assert(bit.wire);
 
-		Instance *driver = clock_net->Driver();
-		if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
-			clock_net = driver->GetInput();
-			posedge = false;
-		}
+		if (bit.wire->attributes.count("\\init"))
+			initval = bit.wire->attributes.at("\\init");
 
-		clock_sig = importer->net_map_at(clock_net);
-		return;
-	}
-}
+		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;
 
-struct VerificSvaImporter
-{
-	VerificImporter *importer;
-	Module *module;
+		bit.wire->attributes["\\init"] = initval;
+	}
 
-	Netlist *netlist;
-	Instance *root;
+	for (auto net : anyconst_nets)
+		module->connect(net_map_at(net), module->Anyconst(NEW_ID));
 
-	SigBit clock = State::Sx;
-	bool clock_posedge = false;
+	for (auto net : anyseq_nets)
+		module->connect(net_map_at(net), module->Anyseq(NEW_ID));
 
-	SigBit disable_iff = State::S0;
+	pool<Instance*, hash_ptr_ops> sva_asserts;
+	pool<Instance*, hash_ptr_ops> sva_assumes;
+	pool<Instance*, hash_ptr_ops> sva_covers;
 
-	bool mode_assert = false;
-	bool mode_assume = false;
-	bool mode_cover = false;
-	bool eventually = false;
-	bool did_something = false;
+	pool<RTLIL::Cell*> past_ffs;
 
-	Instance *net_to_ast_driver(Net *n)
+	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
 	{
-		if (n == nullptr)
-			return nullptr;
-
-		if (n->IsMultipleDriven())
-			return nullptr;
-
-		Instance *inst = n->Driver();
-
-		if (inst == nullptr)
-			return nullptr;
+		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
 
-		if (!verific_sva_prims.count(inst->Type()))
-			return nullptr;
+		if (verbose)
+			log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
 
-		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)
-			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 Preprocessor
+		if (inst->Type() == PRIM_PWR) {
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
+			continue;
+		}
 
-	Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
-	Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
-	Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
-	Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
-	Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
+		if (inst->Type() == PRIM_GND) {
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
+			continue;
+		}
 
-	Net *rewrite(Instance *inst, Net *default_net = nullptr)
-	{
-		if (inst == nullptr)
-			return default_net;
-
-		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
-				inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
-			Net *new_net = rewrite(get_ast_input(inst));
-			if (new_net) {
-				inst->Disconnect(inst->View()->GetInput());
-				inst->Connect(inst->View()->GetInput(), new_net);
-			}
-			return default_net;
+		if (inst->Type() == PRIM_BUF) {
+			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+			continue;
 		}
 
-		if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
-			Net *new_net = rewrite(get_ast_input2(inst));
-			if (new_net) {
-				inst->Disconnect(inst->View()->GetInput2());
-				inst->Connect(inst->View()->GetInput2(), new_net);
-			}
-			return default_net;
+		if (inst->Type() == PRIM_X) {
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
+			continue;
 		}
 
-		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-		{
-			if (mode_cover) {
-				did_something = true;
-				Net *new_in1 = rewrite_input1(inst);
-				Net *new_in2 = rewrite_input2(inst);
-				return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
-			}
-			return default_net;
+		if (inst->Type() == PRIM_Z) {
+			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
+			continue;
 		}
 
-		if (inst->Type() == PRIM_SVA_NOT)
+		if (inst->Type() == OPER_READ_PORT)
 		{
-			if (mode_assert || mode_assume) {
-				did_something = true;
-				Net *new_in = rewrite_input(inst);
-				Net *net_zero = netlist->Gnd(inst->Linefile());
-				return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
+			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());
+
+			RTLIL::SigSpec addr = operatorInput1(inst);
+			RTLIL::SigSpec data = operatorOutput(inst);
+
+			RTLIL::Cell *cell = module->addCell(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);
+			continue;
+		}
+
+		if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
+		{
+			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());
+
+			RTLIL::SigSpec addr = operatorInput1(inst);
+			RTLIL::SigSpec data = operatorInput2(inst);
+
+			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("\\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()));
 			}
-			return default_net;
+			continue;
 		}
 
-		return default_net;
-	}
-
-	void rewrite()
-	{
-		netlist = root->Owner();
-		do {
-			did_something = false;
-			rewrite(root);
-		} while (did_something);
-	}
-
-	// ----------------------------------------------------------
-	// SVA Inporter
-
-	struct sequence_t {
-		int length = 0;
-		SigBit sig_a = State::S1;
-		SigBit sig_en = State::S1;
-	};
-
-	void sequence_cond(sequence_t &seq, SigBit cond)
-	{
-		seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
-	}
-
-	void sequence_ff(sequence_t &seq)
-	{
-		if (disable_iff != State::S0)
-			seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
+		if (!mode_gates) {
+			if (import_netlist_instance_cells(inst, inst_name))
+				continue;
+			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(inst, inst_name))
+				continue;
+		}
 
-		Wire *sig_a_q = module->addWire(NEW_ID);
-		sig_a_q->attributes["\\init"] = Const(0, 1);
+		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
+			sva_asserts.insert(inst);
 
-		Wire *sig_en_q = module->addWire(NEW_ID);
-		sig_en_q->attributes["\\init"] = Const(0, 1);
+		if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
+			sva_assumes.insert(inst);
 
-		module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
-		module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
+		if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
+			sva_covers.insert(inst);
 
-		seq.length++;
-		seq.sig_a = sig_a_q;
-		seq.sig_en = sig_en_q;
-	}
+		if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
+		{
+			VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
 
-	void parse_sequence(sequence_t &seq, Net *n)
-	{
-		Instance *inst = net_to_ast_driver(n);
+			log_assert(inst->Input1Size() == inst->OutputSize());
 
-		// Regular expression
+			SigSpec sig_d, sig_q, sig_o;
+			sig_q = module->addWire(NEW_ID, inst->Input1Size());
 
-		if (inst == nullptr) {
-			sequence_cond(seq, importer->net_map_at(n));
-			return;
-		}
+			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)));
+			}
 
-		// SVA Primitives
+			if (verbose) {
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+				log("    XNOR with A=%s, B=%s, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+			}
 
-		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
-		{
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-			parse_sequence(seq, inst->GetInput2());
-			return;
-		}
+			module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
 
-		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-		{
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-			sequence_ff(seq);
-			parse_sequence(seq, inst->GetInput2());
-			return;
+			if (!mode_keep)
+				continue;
 		}
 
-		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
+		if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
 		{
-			int sva_low = atoi(inst->GetAttValue("sva:low"));
-			int sva_high = atoi(inst->GetAttValue("sva:low"));
+			VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
 
-			if (sva_low != sva_high)
-				log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
+			SigSpec sig_d = net_map_at(inst->GetInput1());
+			SigSpec sig_o = net_map_at(inst->GetOutput());
+			SigSpec sig_q = module->addWire(NEW_ID);
 
-			parse_sequence(seq, inst->GetInput1());
+			if (verbose) {
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+				log("    XNOR with A=%s, B=%s, Y=%s.\n",
+						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+			}
 
-			for (int i = 0; i < sva_low; i++)
-				sequence_ff(seq);
+			module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
 
-			parse_sequence(seq, inst->GetInput2());
-			return;
+			if (!mode_keep)
+				continue;
 		}
 
-		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
+		if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
 		{
-			int sva_low = atoi(inst->GetAttValue("sva:low"));
-			int sva_high = atoi(inst->GetAttValue("sva:low"));
-
-			if (sva_low != sva_high)
-				log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
+			VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
 
-			parse_sequence(seq, inst->GetInput());
+			SigBit sig_d = net_map_at(inst->GetInput1());
+			SigBit sig_q = net_map_at(inst->GetOutput());
 
-			for (int i = 1; i < sva_low; i++) {
-				sequence_ff(seq);
-				parse_sequence(seq, inst->GetInput());
-			}
-			return;
-		}
-
-		// Handle unsupported primitives
-
-		if (!importer->mode_keep)
-			log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
-		log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
-	}
-
-	void import()
-	{
-		module = importer->module;
-		netlist = root->Owner();
+			if (verbose)
+				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
 
-		RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+			past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge));
 
-		// parse SVA property clock event
+			if (!mode_keep)
+				continue;
+		}
 
-		Instance *at_node = get_ast_input(root);
+		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
+			if (verbose)
+				log("    skipping SVA cell in non k-mode\n");
+			continue;
+		}
 
-		// asynchronous immediate assertion/assumption/cover
-		if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
-				root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
+		if (inst->IsPrimitive())
 		{
-			SigSpec sig_a = importer->net_map_at(root->GetInput());
-			RTLIL::Cell *c = nullptr;
-
-			if (eventually) {
-				if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
-				if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
-			} else {
-				if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
-				if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
-				if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
-			}
+			if (inst->Type() == PRIM_HDL_ASSERTION)
+				continue;
 
-			importer->import_attributes(c->attributes, root);
-			return;
+			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());
 		}
 
-		log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
+		nl_todo.insert(inst->View());
 
-		VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
-		clock = clock_edge.clock_sig;
-		clock_posedge = clock_edge.posedge;
+		RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
+				std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
 
-		// parse disable_iff expression
+		if (inst->IsPrimitive() && mode_keep)
+			cell->attributes["\\keep"] = 1;
 
-		Net *sequence_net = at_node->GetInput2();
+		dict<IdString, vector<SigBit>> cell_port_conns;
 
-		while (1)
-		{
-			Instance *sequence_node = net_to_ast_driver(sequence_net);
+		if (verbose)
+			log("    ports in verific db:\n");
 
-			if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
-				eventually = true;
-				sequence_net = sequence_node->GetInput();
-				continue;
+		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
+			if (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()) {
+				port_name = pr->GetPort()->Bus()->Name();
+				port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
+						min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
 			}
-
-			if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
-				disable_iff = importer->net_map_at(sequence_node->GetInput1());
-				sequence_net = sequence_node->GetInput2();
-				continue;
+			IdString port_name_id = RTLIL::escape_id(port_name);
+			auto &sigvec = cell_port_conns[port_name_id];
+			if (GetSize(sigvec) <= port_offset) {
+				SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
+				for (auto bit : zwires)
+					sigvec.push_back(bit);
 			}
-
-			break;
+			sigvec[port_offset] = net_map_at(pr->GetNet());
 		}
 
-		// parse SVA sequence into trigger signal
+		if (verbose)
+			log("    ports in yosys db:\n");
 
-		sequence_t seq;
-		parse_sequence(seq, sequence_net);
-		sequence_ff(seq);
+		for (auto &it : cell_port_conns) {
+			if (verbose)
+				log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
+			cell->setPort(it.first, it.second);
+		}
+	}
 
-		// generate assert/assume/cover cell
+	if (!mode_nosva)
+	{
+		for (auto inst : sva_asserts)
+			import_sva_assert(this, inst);
 
-		RTLIL::Cell *c = nullptr;
+		for (auto inst : sva_assumes)
+			import_sva_assume(this, inst);
 
-		if (eventually) {
-			if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
-			if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
-		} else {
-			if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
-			if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
-			if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
-		}
+		for (auto inst : sva_covers)
+			import_sva_cover(this, inst);
 
-		importer->import_attributes(c->attributes, root);
+		merge_past_ffs(past_ffs);
 	}
-};
-
-void svapp_assert(Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_assert = true;
-	worker.rewrite();
 }
 
-void svapp_assume(Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_assume = true;
-	worker.rewrite();
-}
+// ==================================================================
 
-void svapp_cover(Instance *inst)
+VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
 {
-	VerificSvaImporter worker;
-	worker.root = inst;
-	worker.mode_cover = true;
-	worker.rewrite();
-}
+	log_assert(importer != nullptr);
+	log_assert(inst != nullptr);
 
-void import_sva_assert(VerificImporter *importer, Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.importer = importer;
-	worker.root = inst;
-	worker.mode_assert = true;
-	worker.import();
-}
+	// SVA posedge/negedge
+	if (inst->Type() == PRIM_SVA_POSEDGE)
+	{
+		clock_net = inst->GetInput();
+		posedge = true;
 
-void import_sva_assume(VerificImporter *importer, Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.importer = importer;
-	worker.root = inst;
-	worker.mode_assume = true;
-	worker.import();
-}
+		Instance *driver = clock_net->Driver();
+		if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
+			clock_net = driver->GetInput();
+			posedge = false;
+		}
 
-void import_sva_cover(VerificImporter *importer, Instance *inst)
-{
-	VerificSvaImporter worker;
-	worker.importer = importer;
-	worker.root = inst;
-	worker.mode_cover = true;
-	worker.import();
+		clock_sig = importer->net_map_at(clock_net);
+		return;
+	}
 }
 
 // ==================================================================
@@ -1728,8 +1351,11 @@ struct VerificExtNets
 	}
 };
 
+YOSYS_NAMESPACE_END
 #endif /* YOSYS_ENABLE_VERIFIC */
 
+PRIVATE_NAMESPACE_BEGIN
+
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
 	virtual void help()
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
new file mode 100644
index 000000000..4f1cb5d0f
--- /dev/null
+++ b/frontends/verific/verific.h
@@ -0,0 +1,79 @@
+/*
+ *  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 pool<int> verific_sva_prims;
+
+struct VerificImporter;
+
+struct VerificClockEdge {
+	Verific::Net *clock_net = nullptr;
+	SigBit clock_sig = State::Sx;
+	bool posedge = false;
+	VerificClockEdge(VerificImporter *importer, Verific::Instance *inst);
+};
+
+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;
+
+	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
+
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose);
+
+	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);
+
+	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 import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
+void import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
+void import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
+
+void svapp_assert(Verific::Instance *inst);
+void svapp_assume(Verific::Instance *inst);
+void svapp_cover(Verific::Instance *inst);
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
new file mode 100644
index 000000000..5a56b2fe0
--- /dev/null
+++ b/frontends/verific/verificsva.cc
@@ -0,0 +1,384 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "frontends/verific/verific.h"
+
+USING_YOSYS_NAMESPACE
+
+#ifdef VERIFIC_NAMESPACE
+using namespace Verific;
+#endif
+
+YOSYS_NAMESPACE_BEGIN
+
+struct VerificSvaImporter
+{
+	VerificImporter *importer = nullptr;
+	Module *module = nullptr;
+
+	Netlist *netlist = nullptr;
+	Instance *root = nullptr;
+
+	SigBit clock = State::Sx;
+	bool clock_posedge = false;
+
+	SigBit disable_iff = State::S0;
+
+	bool mode_assert = false;
+	bool mode_assume = false;
+	bool mode_cover = false;
+	bool eventually = false;
+	bool did_something = 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)
+			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 Preprocessor
+
+	Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
+	Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
+	Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
+	Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
+	Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
+
+	Net *rewrite(Instance *inst, Net *default_net = nullptr)
+	{
+		if (inst == nullptr)
+			return default_net;
+
+		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
+				inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
+			Net *new_net = rewrite(get_ast_input(inst));
+			if (new_net) {
+				inst->Disconnect(inst->View()->GetInput());
+				inst->Connect(inst->View()->GetInput(), new_net);
+			}
+			return default_net;
+		}
+
+		if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
+			Net *new_net = rewrite(get_ast_input2(inst));
+			if (new_net) {
+				inst->Disconnect(inst->View()->GetInput2());
+				inst->Connect(inst->View()->GetInput2(), new_net);
+			}
+			return default_net;
+		}
+
+		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			if (mode_cover) {
+				did_something = true;
+				Net *new_in1 = rewrite_input1(inst);
+				Net *new_in2 = rewrite_input2(inst);
+				return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
+			}
+			return default_net;
+		}
+
+		if (inst->Type() == PRIM_SVA_NOT)
+		{
+			if (mode_assert || mode_assume) {
+				did_something = true;
+				Net *new_in = rewrite_input(inst);
+				Net *net_zero = netlist->Gnd(inst->Linefile());
+				return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
+			}
+			return default_net;
+		}
+
+		return default_net;
+	}
+
+	void rewrite()
+	{
+		netlist = root->Owner();
+		do {
+			did_something = false;
+			rewrite(root);
+		} while (did_something);
+	}
+
+	// ----------------------------------------------------------
+	// SVA Importer
+
+	struct sequence_t {
+		int length = 0;
+		SigBit sig_a = State::S1;
+		SigBit sig_en = State::S1;
+	};
+
+	void sequence_cond(sequence_t &seq, SigBit cond)
+	{
+		seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
+	}
+
+	void sequence_ff(sequence_t &seq)
+	{
+		if (disable_iff != State::S0)
+			seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
+
+		Wire *sig_a_q = module->addWire(NEW_ID);
+		sig_a_q->attributes["\\init"] = Const(0, 1);
+
+		Wire *sig_en_q = module->addWire(NEW_ID);
+		sig_en_q->attributes["\\init"] = Const(0, 1);
+
+		module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
+		module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
+
+		seq.length++;
+		seq.sig_a = sig_a_q;
+		seq.sig_en = sig_en_q;
+	}
+
+	void parse_sequence(sequence_t &seq, Net *n)
+	{
+		Instance *inst = net_to_ast_driver(n);
+
+		// Regular expression
+
+		if (inst == nullptr) {
+			sequence_cond(seq, importer->net_map_at(n));
+			return;
+		}
+
+		// SVA Primitives
+
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
+		{
+			parse_sequence(seq, inst->GetInput1());
+			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
+			parse_sequence(seq, inst->GetInput2());
+			return;
+		}
+
+		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			parse_sequence(seq, inst->GetInput1());
+			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
+			sequence_ff(seq);
+			parse_sequence(seq, inst->GetInput2());
+			return;
+		}
+
+		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
+		{
+			int sva_low = atoi(inst->GetAttValue("sva:low"));
+			int sva_high = atoi(inst->GetAttValue("sva:low"));
+
+			if (sva_low != sva_high)
+				log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
+
+			parse_sequence(seq, inst->GetInput1());
+
+			for (int i = 0; i < sva_low; i++)
+				sequence_ff(seq);
+
+			parse_sequence(seq, inst->GetInput2());
+			return;
+		}
+
+		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
+		{
+			int sva_low = atoi(inst->GetAttValue("sva:low"));
+			int sva_high = atoi(inst->GetAttValue("sva:low"));
+
+			if (sva_low != sva_high)
+				log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
+
+			parse_sequence(seq, inst->GetInput());
+
+			for (int i = 1; i < sva_low; i++) {
+				sequence_ff(seq);
+				parse_sequence(seq, inst->GetInput());
+			}
+			return;
+		}
+
+		// Handle unsupported primitives
+
+		if (!importer->mode_keep)
+			log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
+		log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
+	}
+
+	void import()
+	{
+		module = importer->module;
+		netlist = root->Owner();
+
+		RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+
+		// parse SVA property clock event
+
+		Instance *at_node = get_ast_input(root);
+
+		// asynchronous immediate assertion/assumption/cover
+		if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
+				root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
+		{
+			SigSpec sig_a = importer->net_map_at(root->GetInput());
+			RTLIL::Cell *c = nullptr;
+
+			if (eventually) {
+				if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
+				if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
+			} else {
+				if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
+				if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
+				if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
+			}
+
+			importer->import_attributes(c->attributes, root);
+			return;
+		}
+
+		log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
+
+		VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
+		clock = clock_edge.clock_sig;
+		clock_posedge = clock_edge.posedge;
+
+		// parse disable_iff expression
+
+		Net *sequence_net = at_node->GetInput2();
+
+		while (1)
+		{
+			Instance *sequence_node = net_to_ast_driver(sequence_net);
+
+			if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
+				eventually = true;
+				sequence_net = sequence_node->GetInput();
+				continue;
+			}
+
+			if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
+				disable_iff = importer->net_map_at(sequence_node->GetInput1());
+				sequence_net = sequence_node->GetInput2();
+				continue;
+			}
+
+			break;
+		}
+
+		// parse SVA sequence into trigger signal
+
+		sequence_t seq;
+		parse_sequence(seq, sequence_net);
+		sequence_ff(seq);
+
+		// generate assert/assume/cover cell
+
+		RTLIL::Cell *c = nullptr;
+
+		if (eventually) {
+			if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
+			if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
+		} else {
+			if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
+			if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
+			if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
+		}
+
+		importer->import_attributes(c->attributes, root);
+	}
+};
+
+void svapp_assert(Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.root = inst;
+	worker.mode_assert = true;
+	worker.rewrite();
+}
+
+void svapp_assume(Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.root = inst;
+	worker.mode_assume = true;
+	worker.rewrite();
+}
+
+void svapp_cover(Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.root = inst;
+	worker.mode_cover = true;
+	worker.rewrite();
+}
+
+void import_sva_assert(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assert = true;
+	worker.import();
+}
+
+void import_sva_assume(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assume = true;
+	worker.import();
+}
+
+void import_sva_cover(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaImporter worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_cover = true;
+	worker.import();
+}
+
+YOSYS_NAMESPACE_END