Merge https://github.com/cliffordwolf/yosys

10 files changed, 832 insertions, 643 deletions

diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 2d58c682f..38a19a36f 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -84,6 +84,7 @@ std::string AST::type2str(AstNodeType type)
 	X(AST_PREFIX)
 	X(AST_ASSERT)
 	X(AST_ASSUME)
+	X(AST_COVER)
 	X(AST_FCALL)
 	X(AST_TO_BITS)
 	X(AST_TO_SIGNED)
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index cd6e264e6..0b9116d39 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -65,6 +65,7 @@ namespace AST
 		AST_PREFIX,
 		AST_ASSERT,
 		AST_ASSUME,
+		AST_COVER,
 
 		AST_FCALL,
 		AST_TO_BITS,
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index db8d7409f..bdac4de00 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1336,9 +1336,11 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 	// generate $assert cells
 	case AST_ASSERT:
 	case AST_ASSUME:
+	case AST_COVER:
 		{
 			const char *celltype = "$assert";
 			if (type == AST_ASSUME) celltype = "$assume";
+			if (type == AST_COVER) celltype = "$cover";
 
 			log_assert(children.size() == 2);
 
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index c1e77c6ec..eecc04132 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1400,7 +1400,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	}
 skip_dynamic_range_lvalue_expansion:;
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && current_block != NULL)
 	{
 		std::stringstream sstr;
 		sstr << "$formal$" << filename << ":" << linenum << "$" << (autoidx++);
@@ -1462,7 +1462,7 @@ skip_dynamic_range_lvalue_expansion:;
 		goto apply_newNode;
 	}
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && children.size() == 1)
 	{
 		children.push_back(mkconst_int(1, false, 1));
 		did_something = true;
diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 6d4d60870..f610a25c3 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -55,7 +55,30 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count,
 	}
 }
 
-void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode)
+static std::pair<RTLIL::IdString, int> wideports_split(std::string name)
+{
+	int pos = -1;
+
+	if (name.empty() || name.back() != ']')
+		goto failed;
+
+	for (int i = 0; i+1 < GetSize(name); i++) {
+		if (name[i] == '[')
+			pos = i;
+		else if (name[i] < '0' || name[i] > '9')
+			pos = -1;
+		else if (i == pos+1 && name[i] == '0')
+			pos = -1;
+	}
+
+	if (pos >= 0)
+		return std::pair<RTLIL::IdString, int>("\\" + name.substr(0, pos), atoi(name.c_str() + pos+1)+1);
+
+failed:
+	return std::pair<RTLIL::IdString, int>("\\" + name, 0);
+}
+
+void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode, bool wideports)
 {
 	RTLIL::Module *module = nullptr;
 	RTLIL::Const *lutptr = NULL;
@@ -96,6 +119,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 	dict<RTLIL::IdString, RTLIL::Const> *obj_attributes = nullptr;
 	dict<RTLIL::IdString, RTLIL::Const> *obj_parameters = nullptr;
 
+	dict<RTLIL::IdString, std::pair<int, bool>> wideports_cache;
+
 	size_t buffer_size = 4096;
 	char *buffer = (char*)malloc(buffer_size);
 	int line_count = 0;
@@ -148,7 +173,32 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 
 			if (!strcmp(cmd, ".end"))
 			{
+				for (auto &wp : wideports_cache)
+				{
+					auto name = wp.first;
+					int width = wp.second.first;
+					bool isinput = wp.second.second;
+
+					RTLIL::Wire *wire = module->addWire(name, width);
+					wire->port_input = isinput;
+					wire->port_output = !isinput;
+
+					for (int i = 0; i < width; i++) {
+						RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
+						RTLIL::Wire *other_wire = module->wire(other_name);
+						if (other_wire) {
+							other_wire->port_input = false;
+							other_wire->port_output = false;
+							if (isinput)
+								module->connect(other_wire, SigSpec(wire, i));
+							else
+								module->connect(SigSpec(wire, i), other_wire);
+						}
+					}
+				}
+
 				module->fixup_ports();
+				wideports_cache.clear();
 
 				if (run_clean)
 				{
@@ -187,9 +237,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 				continue;
 			}
 
-			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
+			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs"))
+			{
 				char *p;
-				while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+				while ((p = strtok(NULL, " \t\r\n")) != NULL)
+				{
 					RTLIL::IdString wire_name(stringf("\\%s", p));
 					RTLIL::Wire *wire = module->wire(wire_name);
 					if (wire == nullptr)
@@ -198,6 +250,14 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 						wire->port_input = true;
 					else
 						wire->port_output = true;
+
+					if (wideports) {
+						std::pair<RTLIL::IdString, int> wp = wideports_split(p);
+						if (wp.second > 0) {
+							wideports_cache[wp.first].first = std::max(wideports_cache[wp.first].first, wp.second);
+							wideports_cache[wp.first].second = !strcmp(cmd, ".inputs");
+						}
+					}
 				}
 				obj_attributes = nullptr;
 				obj_parameters = nullptr;
@@ -452,6 +512,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 		}
 	}
 
+	return;
+
 error:
 	log_error("Syntax error in line %d!\n", line_count);
 }
@@ -469,10 +531,15 @@ struct BlifFrontend : public Frontend {
 		log("    -sop\n");
 		log("        Create $sop cells instead of $lut cells\n");
 		log("\n");
+		log("    -wideports\n");
+		log("        Merge ports that match the pattern 'name[int]' into a single\n");
+		log("        multi-bit port 'name'.\n");
+		log("\n");
 	}
 	virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool sop_mode = false;
+		bool wideports = false;
 
 		log_header(design, "Executing BLIF frontend.\n");
 
@@ -483,11 +550,15 @@ struct BlifFrontend : public Frontend {
 				sop_mode = true;
 				continue;
 			}
+			if (arg == "-wideports") {
+				wideports = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
 
-		parse_blif(design, *f, "", true, sop_mode);
+		parse_blif(design, *f, "", true, sop_mode, wideports);
 	}
 } BlifFrontend;
 
diff --git a/frontends/blif/blifparse.h b/frontends/blif/blifparse.h
index 058087d81..955b6aacf 100644
--- a/frontends/blif/blifparse.h
+++ b/frontends/blif/blifparse.h
@@ -24,7 +24,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
-extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean = false, bool sop_mode = false);
+extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name,
+		bool run_clean = false, bool sop_mode = false, bool wideports = false);
 
 YOSYS_NAMESPACE_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..f3b997dc5 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,775 +71,829 @@ 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();
+
+		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;
+				continue;
+			}
 
-		if (net->Bus())
-			continue;
+			if (net_map.count(net)) {
+				// log("  skipping net %s.\n", net->Name());
+				continue;
+			}
 
-		// log("  importing net %s.\n", net->Name());
+			if (net->Bus())
+				continue;
 
-		RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
-		RTLIL::Wire *wire = module->addWire(wire_name);
-		import_attributes(wire->attributes, net);
+			// log("  importing net %s.\n", net->Name());
 
-		net_map[net] = wire;
-	}
+			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
+			RTLIL::Wire *wire = module->addWire(wire_name);
+			import_attributes(wire->attributes, net);
 
-	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;
+			net_map[net] = wire;
 		}
 
-		if (found_new_net)
+		FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
 		{
-			// 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);
-
+			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;
+			}
 
-		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_X) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx);
+				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() == PRIM_Z) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
+				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_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;
+			}
+
+			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()
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..\n");
+		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv|-vlpsl} <verilog-file>..\n");
 		log("\n");
 		log("Load the specified Verilog/SystemVerilog files into Verific.\n");
 		log("\n");
 		log("\n");
-		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>..\n");
+		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdpsl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
@@ -890,6 +950,13 @@ struct VerificPass : public Pass {
 			return;
 		}
 
+		if (args.size() > 1 && args[1] == "-vlpsl") {
+			for (size_t argidx = 2; argidx < args.size(); argidx++)
+				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_PSL))
+					log_cmd_error("Reading `%s' in VERILOG_PSL mode failed.\n", args[argidx].c_str());
+			return;
+		}
+
 		if (args.size() > 1 && args[1] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
 			for (size_t argidx = 2; argidx < args.size(); argidx++)
@@ -922,6 +989,14 @@ struct VerificPass : public Pass {
 			return;
 		}
 
+		if (args.size() > 1 && args[1] == "-vhdpsl") {
+			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
+			for (size_t argidx = 2; argidx < args.size(); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL))
+					log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str());
+			return;
+		}
+
 		if (args.size() > 1 && args[1] == "-import")
 		{
 			std::set<Netlist*> nl_todo, nl_done;
@@ -982,8 +1057,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 +1078,5 @@ struct VerificPass : public Pass {
 #endif
 } VerificPass;
 
-YOSYS_NAMESPACE_END
+PRIVATE_NAMESPACE_END
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 405aeb975..97af0ae2d 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -177,8 +177,11 @@ YOSYS_NAMESPACE_END
 
 "assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
 "assume"   { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
+"cover"    { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
 "restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
 "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
+"rand"     { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
+"const"    { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
 "logic"    { SV_KEYWORD(TOK_REG); }
 "bit"      { SV_KEYWORD(TOK_REG); }
 
@@ -192,14 +195,17 @@ YOSYS_NAMESPACE_END
 "genvar"  { return TOK_GENVAR; }
 "real"    { return TOK_REAL; }
 
+"enum"    { SV_KEYWORD(TOK_ENUM); }
+"typedef" { SV_KEYWORD(TOK_TYPEDEF); }
+
 [0-9][0-9_]* {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9]*[ \t]*\'s?[bodhBODH][ \t\r\n]*[0-9a-fA-FzxZX?_]+ {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? {
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 607c48a81..3eb03dfd8 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -59,6 +59,7 @@ namespace VERILOG_FRONTEND {
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
 	bool norestrict_mode, assume_asserts_mode;
+	bool current_wire_rand, current_wire_const;
 	std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -100,7 +101,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 	bool boolean;
 }
 
-%token <string> TOK_STRING TOK_ID TOK_CONST TOK_REALVAL TOK_PRIMITIVE
+%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
 %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
 %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
 %token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP
@@ -114,7 +115,8 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
+%token TOK_RAND TOK_CONST
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
@@ -355,6 +357,8 @@ delay:
 wire_type:
 	{
 		astbuf3 = new AstNode(AST_WIRE);
+		current_wire_rand = false;
+		current_wire_const = false;
 	} wire_type_token_list delay {
 		$$ = astbuf3;
 	};
@@ -392,6 +396,12 @@ wire_type_token:
 	} |
 	TOK_SIGNED {
 		astbuf3->is_signed = true;
+	} |
+	TOK_RAND {
+		current_wire_rand = true;
+	} |
+	TOK_CONST {
+		current_wire_const = true;
 	};
 
 non_opt_range:
@@ -730,7 +740,15 @@ wire_name_list:
 	wire_name_and_opt_assign | wire_name_list ',' wire_name_and_opt_assign;
 
 wire_name_and_opt_assign:
-	wire_name |
+	wire_name {
+		if (current_wire_rand) {
+			AstNode *wire = new AstNode(AST_IDENTIFIER);
+			AstNode *fcall = new AstNode(AST_FCALL);
+			wire->str = ast_stack.back()->children.back()->str;
+			fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq";
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall));
+		}
+	} |
 	wire_name '=' expr {
 		AstNode *wire = new AstNode(AST_IDENTIFIER);
 		wire->str = ast_stack.back()->children.back()->str;
@@ -1000,6 +1018,15 @@ assert:
 	TOK_ASSUME '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
 	} |
+	TOK_COVER '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3));
+	} |
+	TOK_COVER '(' ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
+	TOK_COVER ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
 	TOK_RESTRICT '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $3;
@@ -1014,6 +1041,9 @@ assert_property:
 	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
 	} |
+	TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
+	} |
 	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $4;
@@ -1350,7 +1380,7 @@ basic_expr:
 	rvalue {
 		$$ = $1;
 	} |
-	'(' expr ')' TOK_CONST {
+	'(' expr ')' TOK_CONSTVAL {
 		if ($4->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = $2;
@@ -1360,7 +1390,7 @@ basic_expr:
 		$$ = new AstNode(AST_TO_BITS, bits, val);
 		delete $4;
 	} |
-	hierarchical_id TOK_CONST {
+	hierarchical_id TOK_CONSTVAL {
 		if ($2->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = new AstNode(AST_IDENTIFIER);
@@ -1372,14 +1402,14 @@ basic_expr:
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST TOK_CONST {
+	TOK_CONSTVAL TOK_CONSTVAL {
 		$$ = const2ast(*$1 + *$2, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL || (*$2)[0] != '\'')
 			log_error("Value conversion failed: `%s%s'\n", $1->c_str(), $2->c_str());
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST {
+	TOK_CONSTVAL {
 		$$ = const2ast(*$1, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL)
 			log_error("Value conversion failed: `%s'\n", $1->c_str());