From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 12:36:00 +0000 (+0100)
Subject: Add assert/assume support to verific front-end
X-Git-Tag: yosys-0.8~523
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=911c44d164e04026bd3a3a2eb1bf0c5d9cca5c19;p=yosys.git

Add assert/assume support to verific front-end
---

diff --git a/frontends/verific/build_amd64.txt b/frontends/verific/build_amd64.txt
index d6952820e..95d618ecc 100644
--- a/frontends/verific/build_amd64.txt
+++ b/frontends/verific/build_amd64.txt
@@ -6,7 +6,7 @@ only have the i386 eval version of Verific:
 1.) Use a Makefile.conf like the following one:
 
 --snip--
-CONFIG := clang
+CONFIG := gcc
 ENABLE_TCL := 0
 ENABLE_PLUGINS := 0
 ENABLE_VERIFIC := 1
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7dd36a747..9bf5a6c6c 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -49,7 +49,13 @@ USING_YOSYS_NAMESPACE
 using namespace Verific ;
 #endif
 
-static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
+#endif
+
+PRIVATE_NAMESPACE_BEGIN
+
+#ifdef YOSYS_ENABLE_VERIFIC
+
+void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
 {
 	log("VERIFIC-%s [%s] ",
 			msg_type == VERIFIC_NONE ? "NONE" :
@@ -65,763 +71,817 @@ static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type
 	log("\n");
 }
 
-static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+struct VerificImporter
 {
-	MapIter mi;
-	Att *attr;
-
-	if (obj->Linefile())
-		attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
-
-	// FIXME: Parse numeric attributes
-	FOREACH_ATTRIBUTE(obj, mi, attr)
-		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
-}
+	RTLIL::Module *module;
+	std::map<Net*, RTLIL::SigBit> net_map;
+	std::map<Net*, Net*> sva_posedge_map;
 
-static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	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;
-}
+	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+	{
+		MapIter mi;
+		Att *attr;
 
-static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	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;
-}
+		if (obj->Linefile())
+			attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
 
-static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	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;
-}
+		// FIXME: Parse numeric attributes
+		FOREACH_ATTRIBUTE(obj, mi, attr)
+			attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+	}
 
-static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	PortBus *portbus = inst->View()->GetPortBus(portname);
-	if (portbus) {
+	RTLIL::SigSpec operatorInput(Instance *inst)
+	{
 		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
+		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;
-	} else {
-		Port *port = inst->View()->GetPort(portname);
-		log_assert(port != NULL);
-		Net *net = inst->GetNet(port);
-		return net_map.at(net);
 	}
-}
 
-static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map, RTLIL::Module *module)
-{
-	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);
+	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)));
 			else
-				dummy_wire->width++;
-			sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
-		}
-	return sig;
-}
-
-static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
-{
-	if (inst->Type() == PRIM_AND) {
-		module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_NAND) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_OR) {
-		module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
+				sig.append(RTLIL::State::Sz);
+		return sig;
 	}
 
-	if (inst->Type() == PRIM_NOR) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
+	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;
 	}
 
-	if (inst->Type() == PRIM_XOR) {
-		module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		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_XNOR) {
-		module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), 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_BUF) {
-		module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+	bool import_netlist_instance_gates(Instance *inst)
+	{
+		if (inst->Type() == PRIM_AND) {
+			module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_INV) {
-		module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_NAND) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_MUX) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_OR) {
+			module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_TRI) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_NOR) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			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(RTLIL::escape_id(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_XOR) {
+			module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_DFFRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else if (inst->GetSet()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false);
-		else if (inst->GetReset()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true);
-		else
-			module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_XNOR) {
+			module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	return false;
-}
+		if (inst->Type() == PRIM_BUF) {
+			module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
-{
-	if (inst->Type() == PRIM_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_INV) {
+			module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_NAND) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_MUX) {
+			module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_TRI) {
+			module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_NOR) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		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(RTLIL::escape_id(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_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_DFFRS)
+		{
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else if (inst->GetSet()->IsGnd())
+				module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false);
+			else if (inst->GetReset()->IsGnd())
+				module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true);
+			else
+				module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
+		return false;
 	}
 
-	if (inst->Type() == PRIM_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+	bool import_netlist_instance_cells(Instance *inst)
+	{
+		if (inst->Type() == PRIM_AND) {
+			module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_NAND) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_OR) {
+			module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			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(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y);
-		return true;
-	}
+		if (inst->Type() == PRIM_NOR) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_DFFRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else if (inst->GetSet()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0);
-		else if (inst->GetReset()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1);
-		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_XOR) {
+			module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == PRIM_DLATCHRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else
-			module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
+		if (inst->Type() == PRIM_XNOR) {
+			module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	#define IN  operatorInput(inst, net_map)
-	#define IN1 operatorInput1(inst, net_map)
-	#define IN2 operatorInput2(inst, net_map)
-	#define OUT operatorOutput(inst, net_map, module)
-	#define 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(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
-		} else {
-			RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
-			module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
-			module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false);
+		if (inst->Type() == PRIM_INV) {
+			module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
 		}
-		return true;
-	}
 
-	if (inst->Type() == OPER_MULTIPLIER) {
-		module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == PRIM_MUX) {
+			module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == OPER_DIVIDER) {
-		module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == PRIM_TRI) {
+			module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == OPER_MODULO) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		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(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y);
+			return true;
+		}
 
-	if (inst->Type() == OPER_REMAINDER) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == PRIM_DFFRS)
+		{
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else if (inst->GetSet()->IsGnd())
+				module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0);
+			else if (inst->GetReset()->IsGnd())
+				module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1);
+			else
+				module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
 
-	if (inst->Type() == OPER_SHIFT_LEFT) {
-		module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
-		return true;
-	}
+		if (inst->Type() == PRIM_DLATCHRS)
+		{
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else
+				module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			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);
+		#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(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
+			} else {
+				RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
+				module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
+				module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false);
+			}
+			return true;
 		}
-		module->addShl(RTLIL::escape_id(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);
+		if (inst->Type() == OPER_MULTIPLIER) {
+			module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
 		}
-		module->addShl(RTLIL::escape_id(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(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
-		else if (net_cin == net_a_msb)
-			module->addSshr(RTLIL::escape_id(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_DIVIDER) {
+			module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_REDUCE_AND) {
-		module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_MODULO) {
+			module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_REDUCE_OR) {
-		module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_REMAINDER) {
+			module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_REDUCE_XOR) {
-		module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_SHIFT_LEFT) {
+			module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+			return true;
+		}
 
-	if (inst->Type() == OPER_REDUCE_XNOR) {
-		module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		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(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+			return true;
+		}
 
-	if (inst->Type() == OPER_LESSTHAN) {
-		Net *net_cin = inst->GetCin();
-		if (net_cin->IsGnd())
-			module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		else if (net_cin->IsPwr())
-			module->addLe(RTLIL::escape_id(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_DECODER) {
+			RTLIL::SigSpec vec;
+			vec.append(RTLIL::State::S1);
+			for (unsigned i = 1; i < inst->OutputSize(); i++) {
+				vec.append(RTLIL::State::S0);
+			}
+			module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		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(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+			else if (net_cin == net_a_msb)
+				module->addSshr(RTLIL::escape_id(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_WIDE_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_REDUCE_AND) {
+			module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_REDUCE_OR) {
+			module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_REDUCE_XOR) {
+			module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_REDUCE_XNOR) {
+			module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_LESSTHAN) {
+			Net *net_cin = inst->GetCin();
+			if (net_cin->IsGnd())
+				module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			else if (net_cin->IsPwr())
+				module->addLe(RTLIL::escape_id(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_MINUS) {
-		module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_AND) {
+			module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_UMINUS) {
-		module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_OR) {
+			module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_EQUAL) {
-		module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_XOR) {
+			module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_NEQUAL) {
-		module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_XNOR) {
+			module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_BUF) {
+			module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT);
-		return true;
-	}
+		if (inst->Type() == OPER_WIDE_INV) {
+			module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
 
-	if (inst->Type() == OPER_WIDE_DFFRS) {
-		RTLIL::SigSpec sig_set = operatorInport(inst, "set", net_map);
-		RTLIL::SigSpec sig_reset = operatorInport(inst, "reset", net_map);
-		if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT);
-		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
-		return true;
-	}
+		if (inst->Type() == OPER_MINUS) {
+			module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
 
-	#undef IN
-	#undef IN1
-	#undef IN2
-	#undef OUT
-	#undef SIGNED
+		if (inst->Type() == OPER_UMINUS) {
+			module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
 
-	return false;
-}
+		if (inst->Type() == OPER_EQUAL) {
+			module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
-{
-	std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
+		if (inst->Type() == OPER_NEQUAL) {
+			module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
 
-	if (design->has(module_name)) {
-		if (!nl->IsOperator())
-			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
-		return;
-	}
+		if (inst->Type() == OPER_WIDE_MUX) {
+			module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT);
+			return true;
+		}
 
-	RTLIL::Module *module = new RTLIL::Module;
-	module->name = module_name;
-	design->add(module);
+		if (inst->Type() == OPER_WIDE_TRI) {
+			module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT);
+			return true;
+		}
 
-	log("Importing module %s.\n", RTLIL::id2cstr(module->name));
+		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(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT);
+			else
+				module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
+			return true;
+		}
 
-	std::map<Net*, RTLIL::SigBit> net_map;
+		#undef IN
+		#undef IN1
+		#undef IN2
+		#undef OUT
+		#undef SIGNED
 
-	SetIter si;
-	MapIter mi, mi2;
-	Port *port;
-	PortBus *portbus;
-	Net *net;
-	NetBus *netbus;
-	Instance *inst;
-	PortRef *pr;
+		return false;
+	}
 
-	FOREACH_PORT_OF_NETLIST(nl, mi, port)
+	void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
 	{
-		if (port->Bus())
-			continue;
+		std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
 
-		// log("  importing port %s.\n", port->Name());
+		if (design->has(module_name)) {
+			if (!nl->IsOperator())
+				log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+			return;
+		}
 
-		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
-		import_attributes(wire->attributes, port);
+		module = new RTLIL::Module;
+		module->name = module_name;
+		design->add(module);
 
-		wire->port_id = nl->IndexOf(port) + 1;
+		log("Importing module %s.\n", RTLIL::id2cstr(module->name));
 
-		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;
+		SetIter si;
+		MapIter mi, mi2;
+		Port *port;
+		PortBus *portbus;
+		Net *net;
+		NetBus *netbus;
+		Instance *inst;
+		PortRef *pr;
 
-		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));
-		}
-	}
+		FOREACH_PORT_OF_NETLIST(nl, mi, port)
+		{
+			if (port->Bus())
+				continue;
 
-	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
-	{
-		// log("  importing portbus %s.\n", portbus->Name());
+			// 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(portbus->Name()), portbus->Size());
-		wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
-		import_attributes(wire->attributes, portbus);
+			wire->port_id = nl->IndexOf(port) + 1;
 
-		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;
+			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;
 
-		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 (port->GetNet()) {
+				net = port->GetNet();
 				if (net_map.count(net) == 0)
-					net_map[net] = bit;
+					net_map[net] = wire;
 				else if (wire->port_input)
-					module->connect(net_map.at(net), bit);
+					module->connect(net_map.at(net), wire);
 				else
-					module->connect(bit, net_map.at(net));
+					module->connect(wire, net_map.at(net));
 			}
-			if (i == portbus->RightIndex())
-				break;
 		}
-	}
-
-	module->fixup_ports();
 
-	FOREACH_NET_OF_NETLIST(nl, mi, net)
-	{
-		if (net->IsRamNet())
+		FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
 		{
-			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("  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] = bit;
+					else if (wire->port_input)
+						module->connect(net_map.at(net), bit);
+					else
+						module->connect(bit, net_map.at(net));
 				}
-				log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
-						net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
+				if (i == portbus->RightIndex())
+					break;
 			}
-
-			memory->width = bits_in_word;
-			memory->size = number_of_bits / bits_in_word;
-			continue;
 		}
 
-		if (net_map.count(net)) {
-			// log("  skipping net %s.\n", net->Name());
-			continue;
-		}
+		module->fixup_ports();
 
-		if (net->Bus())
-			continue;
+		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());
+				}
 
-		// log("  importing net %s.\n", net->Name());
+				memory->width = bits_in_word;
+				memory->size = number_of_bits / bits_in_word;
+				continue;
+			}
 
-		RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
-		RTLIL::Wire *wire = module->addWire(wire_name);
-		import_attributes(wire->attributes, net);
+			if (net_map.count(net)) {
+				// log("  skipping net %s.\n", net->Name());
+				continue;
+			}
 
-		net_map[net] = wire;
-	}
+			if (net->Bus())
+				continue;
 
-	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;
-		}
+			// log("  importing net %s.\n", net->Name());
 
-		if (found_new_net)
-		{
-			// log("  importing netbus %s.\n", netbus->Name());
+			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
+			RTLIL::Wire *wire = module->addWire(wire_name);
+			import_attributes(wire->attributes, net);
 
-			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
-			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
-			wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
-			import_attributes(wire->attributes, netbus);
+			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) {
-				if (netbus->ElementAtIndex(i)) {
-					net = netbus->ElementAtIndex(i);
-					RTLIL::SigBit bit(wire, i - wire->start_offset);
-					if (net_map.count(net) == 0)
-						net_map[net] = bit;
-					else
-						module->connect(bit, net_map.at(net));
-				}
+				net = netbus->ElementAtIndex(i);
+				if (net_map.count(net) == 0)
+					found_new_net = true;
 				if (i == netbus->RightIndex())
 					break;
 			}
+
+			if (found_new_net)
+			{
+				// log("  importing netbus %s.\n", netbus->Name());
+
+				RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
+				RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
+				wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
+				import_attributes(wire->attributes, netbus);
+
+				for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
+					if (netbus->ElementAtIndex(i)) {
+						net = netbus->ElementAtIndex(i);
+						RTLIL::SigBit bit(wire, i - wire->start_offset);
+						if (net_map.count(net) == 0)
+							net_map[net] = bit;
+						else
+							module->connect(bit, net_map.at(net));
+					}
+					if (i == netbus->RightIndex())
+						break;
+				}
+			}
+			else
+			{
+				// log("  skipping netbus %s.\n", netbus->Name());
+			}
 		}
-		else
+
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
 		{
-			// log("  skipping netbus %s.\n", netbus->Name());
+			if (inst->Type() == PRIM_SVA_POSEDGE) {
+				Net *in_net = inst->GetInput();
+				Net *out_net = inst->GetOutput();
+				sva_posedge_map[out_net] = in_net;
+				continue;
+			}
 		}
-	}
 
-	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
-	{
-		// log("  importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+		{
+			if (inst->Type() == PRIM_SVA_POSEDGE)
+				continue;
 
-		if (inst->Type() == PRIM_PWR) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1);
-			continue;
-		}
+			// log("  importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
 
-		if (inst->Type() == PRIM_GND) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0);
-			continue;
-		}
+			if (inst->Type() == PRIM_SVA_AT)
+			{
+				Net *in1 = inst->GetInput1();
+				Net *in2 = inst->GetInput2();
+				Net *out = inst->GetOutput();
 
-		if (inst->Type() == PRIM_BUF) {
-			module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-			continue;
-		}
+				if (sva_posedge_map.count(in2))
+					std::swap(in1, in2);
 
-		if (inst->Type() == PRIM_X) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx);
-			continue;
-		}
+				log_assert(sva_posedge_map.count(in1));
+				Net *clk = sva_posedge_map.at(in1);
 
-		if (inst->Type() == PRIM_Z) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
-			continue;
-		}
+				SigBit outsig = net_map.at(out);
+				log_assert(outsig.wire && GetSize(outsig.wire) == 1);
+				outsig.wire->attributes["\\init"] == Const(0, 1);
 
-		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, net_map);
-			RTLIL::SigSpec data = operatorOutput(inst, net_map, module);
-
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd");
-			cell->parameters["\\MEMID"] = memory->name.str();
-			cell->parameters["\\CLK_ENABLE"] = false;
-			cell->parameters["\\CLK_POLARITY"] = true;
-			cell->parameters["\\TRANSPARENT"] = false;
-			cell->parameters["\\ABITS"] = GetSize(addr);
-			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\CLK", RTLIL::State::Sx);
-			cell->setPort("\\EN", RTLIL::State::Sx);
-			cell->setPort("\\ADDR", addr);
-			cell->setPort("\\DATA", data);
-			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, net_map);
-			RTLIL::SigSpec data = operatorInput2(inst, net_map);
-
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(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()));
+				module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out));
+				continue;
 			}
-			continue;
-		}
 
-		if (!mode_gates) {
-			if (import_netlist_instance_cells(module, net_map, inst))
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) {
+				Net *in = inst->GetInput();
+				module->addAssert(NEW_ID, net_map.at(in), State::S1);
 				continue;
-			if (inst->IsOperator())
-				log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
-		} else {
-			if (import_netlist_instance_gates(module, net_map, inst))
+			}
+
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) {
+				Net *in = inst->GetInput();
+				module->addAssume(NEW_ID, net_map.at(in), State::S1);
 				continue;
-		}
+			}
 
-		if (inst->IsPrimitive())
-			log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) {
+				// Net *in = inst->GetInput();
+				// module->addCover(NEW_ID, net_map.at(in), State::S1);
+				continue;
+			}
 
-		nl_todo.insert(inst->View());
+			if (inst->Type() == PRIM_PWR) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1);
+				continue;
+			}
 
-		RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ?
-				std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
+			if (inst->Type() == PRIM_GND) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0);
+				continue;
+			}
 
-		dict<IdString, vector<SigBit>> cell_port_conns;
+			if (inst->Type() == PRIM_BUF) {
+				module->addBufGate(RTLIL::escape_id(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;
+			}
 
-		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
-			// 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 (inst->Type() == PRIM_Z) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
+				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);
+
+			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(RTLIL::escape_id(inst->Name()), "$memrd");
+				cell->parameters["\\MEMID"] = memory->name.str();
+				cell->parameters["\\CLK_ENABLE"] = false;
+				cell->parameters["\\CLK_POLARITY"] = true;
+				cell->parameters["\\TRANSPARENT"] = false;
+				cell->parameters["\\ABITS"] = GetSize(addr);
+				cell->parameters["\\WIDTH"] = GetSize(data);
+				cell->setPort("\\CLK", RTLIL::State::Sx);
+				cell->setPort("\\EN", RTLIL::State::Sx);
+				cell->setPort("\\ADDR", addr);
+				cell->setPort("\\DATA", data);
+				continue;
 			}
-			sigvec[port_offset] = net_map.at(pr->GetNet());
-		}
 
-		for (auto &it : cell_port_conns) {
-			// log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
-			cell->setPort(it.first, it.second);
+			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(RTLIL::escape_id(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))
+					continue;
+				if (inst->IsOperator())
+					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))
+					continue;
+			}
+
+			if (inst->IsPrimitive())
+				log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+
+			nl_todo.insert(inst->View());
+
+			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ?
+					std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
+
+			dict<IdString, vector<SigBit>> cell_port_conns;
+
+			FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
+				// 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());
+			}
+
+			for (auto &it : cell_port_conns) {
+				// log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
+				cell->setPort(it.first, it.second);
+			}
 		}
 	}
-}
+};
 
 #endif /* YOSYS_ENABLE_VERIFIC */
 
-YOSYS_NAMESPACE_BEGIN
-
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
 	virtual void help()
@@ -982,8 +1042,10 @@ struct VerificPass : public Pass {
 
 			while (!nl_todo.empty()) {
 				Netlist *nl = *nl_todo.begin();
-				if (nl_done.count(nl) == 0)
-					import_netlist(design, nl, nl_todo, mode_gates);
+				if (nl_done.count(nl) == 0) {
+					VerificImporter importer;
+					importer.import_netlist(design, nl, nl_todo, mode_gates);
+				}
 				nl_todo.erase(nl);
 				nl_done.insert(nl);
 			}
@@ -1001,5 +1063,5 @@ struct VerificPass : public Pass {
 #endif
 } VerificPass;
 
-YOSYS_NAMESPACE_END
+PRIVATE_NAMESPACE_END