Imported GIT HEAD: 0.8+20190328git32bd0f2

4 files changed, 354 insertions, 235 deletions

diff --git a/frontends/verific/README b/frontends/verific/README
index b4c436a3..89584f2e 100644
--- a/frontends/verific/README
+++ b/frontends/verific/README
@@ -4,35 +4,6 @@ This directory contains Verific bindings for Yosys.
 See http://www.verific.com/ for details.
 
 
-Building Yosys with the 32 bit Verific eval library on amd64:
-=============================================================
-
-1.) Use a Makefile.conf like the following one:
-
---snip--
-CONFIG := gcc
-ENABLE_TCL := 0
-ENABLE_PLUGINS := 0
-ENABLE_VERIFIC := 1
-CXXFLAGS += -m32
-LDFLAGS += -m32
-VERIFIC_DIR = /usr/local/src/verific_lib_eval
---snap--
-
-
-2.) Install the necessary multilib packages
-
-Hint: On debian/ubuntu the multilib packages have names such as
-libreadline-dev:i386 or lib32readline6-dev, depending on the
-exact version of debian/ubuntu you are working with.
-
-
-3.) Build and test
-
-make -j8
-./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top'
-
-
 Verific Features that should be enabled in your Verific library
 ===============================================================
 
@@ -50,7 +21,7 @@ Then run in the following command in this directory:
 
 	sby -f example.sby
 
-This will generate approximately one page of text outpout. The last lines
+This will generate approximately one page of text output. The last lines
 should be something like this:
 
 	SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c5fa5831..ed9727b8 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -118,6 +118,27 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
 	return net_map.at(net);
 }
 
+bool is_blackbox(Netlist *nl)
+{
+	if (nl->IsBlackBox())
+		return true;
+
+	const char *attr = nl->GetAttValue("blackbox");
+	if (attr != nullptr && strcmp(attr, "0"))
+		return true;
+
+	return false;
+}
+
+RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
+{
+	std::string s = stringf("$verific$%s", obj->Name());
+	if (obj->Linefile())
+		s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile()));
+	s += stringf("$%d", autoidx++);
+	return s;
+}
+
 void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
 {
 	MapIter mi;
@@ -203,7 +224,7 @@ RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*,
 			dummy_wire = NULL;
 		} else {
 			if (dummy_wire == NULL)
-				dummy_wire = module->addWire(NEW_ID);
+				dummy_wire = module->addWire(new_verific_id(inst));
 			else
 				dummy_wire->width++;
 			sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
@@ -219,8 +240,8 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 	}
 
 	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);
+		RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+		module->addAndGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
 		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
@@ -231,8 +252,8 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 	}
 
 	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);
+		RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+		module->addOrGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
 		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
 		return true;
 	}
@@ -272,16 +293,16 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 	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);
+		RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(new_verific_id(inst));
+		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
+		RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst));
+		RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst));
+		RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst));
+		module->addXorGate(new_verific_id(inst), a, b, tmp1);
 		module->addXorGate(inst_name, tmp1, c, y);
-		module->addAndGate(NEW_ID, tmp1, c, tmp2);
-		module->addAndGate(NEW_ID, a, b, tmp3);
-		module->addOrGate(NEW_ID, tmp2, tmp3, x);
+		module->addAndGate(new_verific_id(inst), tmp1, c, tmp2);
+		module->addAndGate(new_verific_id(inst), a, b, tmp3);
+		module->addOrGate(new_verific_id(inst), tmp2, tmp3, x);
 		return true;
 	}
 
@@ -308,63 +329,78 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 
 bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
 {
+	RTLIL::Cell *cell = nullptr;
+
 	if (inst->Type() == PRIM_AND) {
-		module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NAND) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
-		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+		RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+		cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		import_attributes(cell->attributes, inst);
+		cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_OR) {
-		module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_NOR) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
-		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+		RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
+		cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
+		import_attributes(cell->attributes, inst);
+		cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XOR) {
-		module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_XNOR) {
-		module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_INV) {
-		module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_MUX) {
-		module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+		cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_TRI) {
-		module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+		cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_FADD)
 	{
-		RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
-		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
+		RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2);
+		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
 		if (inst->GetCout())
 			y.append(net_map_at(inst->GetCout()));
-		module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
-		module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
+		cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
+		import_attributes(cell->attributes, inst);
+		cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -375,24 +411,26 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		log_assert(clocking.body_net == nullptr);
 
 		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+			cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		else if (inst->GetSet()->IsGnd())
-			clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
+			cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
 		else if (inst->GetReset()->IsGnd())
-			clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
+			cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
 		else
-			clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+			cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
 					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == PRIM_DLATCHRS)
 	{
 		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+			cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
 		else
-			module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
+			cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
 					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -408,37 +446,45 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		if (inst->GetCout() != NULL)
 			out.append(net_map_at(inst->GetCout()));
 		if (inst->GetCin()->IsGnd()) {
-			module->addAdd(inst_name, IN1, IN2, out, SIGNED);
+			cell = module->addAdd(inst_name, IN1, IN2, out, SIGNED);
+			import_attributes(cell->attributes, inst);
 		} else {
-			RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
-			module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
-			module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
+			RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst), GetSize(out));
+			cell = module->addAdd(new_verific_id(inst), IN1, IN2, tmp, SIGNED);
+			import_attributes(cell->attributes, inst);
+			cell = module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
+			import_attributes(cell->attributes, inst);
 		}
 		return true;
 	}
 
 	if (inst->Type() == OPER_MULTIPLIER) {
-		module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_DIVIDER) {
-		module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_MODULO) {
-		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REMAINDER) {
-		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_SHIFT_LEFT) {
-		module->addShl(inst_name, IN1, IN2, OUT, false);
+		cell = module->addShl(inst_name, IN1, IN2, OUT, false);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -448,7 +494,8 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		for (unsigned i = 1; i < inst->OutputSize(); i++) {
 			vec.append(RTLIL::State::S0);
 		}
-		module->addShl(inst_name, vec, IN, OUT, false);
+		cell = module->addShl(inst_name, vec, IN, OUT, false);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -458,7 +505,8 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		for (unsigned i = 1; i < inst->OutputSize(); i++) {
 			vec.append(RTLIL::State::S0);
 		}
-		module->addShl(inst_name, vec, IN, OUT, false);
+		cell = module->addShl(inst_name, vec, IN, OUT, false);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -466,108 +514,127 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		Net *net_cin = inst->GetCin();
 		Net *net_a_msb = inst->GetInput1Bit(0);
 		if (net_cin->IsGnd())
-			module->addShr(inst_name, IN1, IN2, OUT, false);
+			cell = module->addShr(inst_name, IN1, IN2, OUT, false);
 		else if (net_cin == net_a_msb)
-			module->addSshr(inst_name, IN1, IN2, OUT, true);
+			cell = module->addSshr(inst_name, IN1, IN2, OUT, true);
 		else
 			log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_AND) {
-		module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_OR) {
-		module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_XOR) {
-		module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_XNOR) {
-		module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_REDUCE_NOR) {
-		SigSpec t = module->ReduceOr(NEW_ID, IN, SIGNED);
-		module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
+		SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED);
+		cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_LESSTHAN) {
 		Net *net_cin = inst->GetCin();
 		if (net_cin->IsGnd())
-			module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+			cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		else if (net_cin->IsPwr())
-			module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+			cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
 		else
 			log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_AND) {
-		module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_OR) {
-		module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_XOR) {
-		module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_XNOR) {
-		module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
+		cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_INV) {
-		module->addNot(inst_name, IN, OUT, SIGNED);
+		cell = module->addNot(inst_name, IN, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_MINUS) {
-		module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+		cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_UMINUS) {
-		module->addNeg(inst_name, IN, OUT, SIGNED);
+		cell = module->addNeg(inst_name, IN, OUT, SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_EQUAL) {
-		module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_NEQUAL) {
-		module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_MUX) {
-		module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+		cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_NTO1MUX) {
-		module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+		cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -587,25 +654,29 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 			padded_data.append(d);
 		}
 
-		module->addShr(inst_name, padded_data, sel, out);
+		cell = module->addShr(inst_name, padded_data, sel, out);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_SELECTOR)
 	{
-		module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
+		cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_SELECTOR)
 	{
 		SigSpec out = OUT;
-		module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
+		cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
 	if (inst->Type() == OPER_WIDE_TRI) {
-		module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
+		cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
+		import_attributes(cell->attributes, inst);
 		return true;
 	}
 
@@ -619,9 +690,10 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		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())
-			clocking.addDff(inst_name, IN, OUT);
+			cell = clocking.addDff(inst_name, IN, OUT);
 		else
-			clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
+			cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
+		import_attributes(cell->attributes, inst);
 
 		return true;
 	}
@@ -709,7 +781,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	netlist = nl;
 
 	if (design->has(module_name)) {
-		if (!nl->IsOperator())
+		if (!nl->IsOperator() && !is_blackbox(nl))
 			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
 		return;
 	}
@@ -718,7 +790,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	module->name = module_name;
 	design->add(module);
 
-	if (nl->IsBlackBox()) {
+	if (is_blackbox(nl)) {
 		log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
 		module->set_bool_attribute("\\blackbox");
 	} else {
@@ -850,7 +922,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 						ascii_initdata++;
 					}
 					if (initval_valid) {
-						RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
+						RTLIL::Cell *cell = module->addCell(new_verific_id(net), "$meminit");
 						cell->parameters["\\WORDS"] = 1;
 						if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
 							cell->setPort("\\ADDR", word_idx);
@@ -913,7 +985,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		if (net->Bus())
 			continue;
 
-		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);
+		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net));
 
 		if (verific_verbose)
 			log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));
@@ -937,7 +1009,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 		if (found_new_net)
 		{
-			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);
+			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus));
 
 			if (verific_verbose)
 				log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
@@ -1013,16 +1085,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		}
 
 		if (GetSize(anyconst_sig))
-			module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));
+			module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig)));
 
 		if (GetSize(anyseq_sig))
-			module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
+			module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig)));
 
 		if (GetSize(allconst_sig))
-			module->connect(allconst_sig, module->Allconst(NEW_ID, GetSize(allconst_sig)));
+			module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig)));
 
 		if (GetSize(allseq_sig))
-			module->connect(allseq_sig, module->Allseq(NEW_ID, GetSize(allseq_sig)));
+			module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig)));
 	}
 
 	for (auto it : init_nets)
@@ -1046,10 +1118,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	}
 
 	for (auto net : anyconst_nets)
-		module->connect(net_map_at(net), module->Anyconst(NEW_ID));
+		module->connect(net_map_at(net), module->Anyconst(new_verific_id(net)));
 
 	for (auto net : anyseq_nets)
-		module->connect(net_map_at(net), module->Anyseq(NEW_ID));
+		module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
 
 	pool<Instance*, hash_ptr_ops> sva_asserts;
 	pool<Instance*, hash_ptr_ops> sva_assumes;
@@ -1060,7 +1132,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
 	{
-		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);
+		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst));
 
 		if (verific_verbose)
 			log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
@@ -1128,27 +1200,34 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		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 asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+			int numchunks = int(inst->Input2Size()) / memory->width;
+			int chunksbits = ceil_log2(numchunks);
+
+			if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0)
+				log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
+
+			for (int i = 0; i < numchunks; i++)
+			{
+				RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
+				RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
+
+				RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
+						RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$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);
 
-			RTLIL::SigSpec addr = operatorInput1(inst);
-			RTLIL::SigSpec data = operatorInput2(inst);
-
-			RTLIL::Cell *cell = module->addCell(inst_name, "$memwr");
-			cell->parameters["\\MEMID"] = memory->name.str();
-			cell->parameters["\\CLK_ENABLE"] = false;
-			cell->parameters["\\CLK_POLARITY"] = true;
-			cell->parameters["\\PRIORITY"] = 0;
-			cell->parameters["\\ABITS"] = GetSize(addr);
-			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
-			cell->setPort("\\CLK", RTLIL::State::S0);
-			cell->setPort("\\ADDR", addr);
-			cell->setPort("\\DATA", data);
-
-			if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
-				cell->parameters["\\CLK_ENABLE"] = true;
-				cell->setPort("\\CLK", net_map_at(inst->GetClock()));
+				if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
+					cell->parameters["\\CLK_ENABLE"] = true;
+					cell->setPort("\\CLK", net_map_at(inst->GetClock()));
+				}
 			}
 			continue;
 		}
@@ -1184,7 +1263,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			log_assert(inst->Input1Size() == inst->OutputSize());
 
 			SigSpec sig_d, sig_q, sig_o;
-			sig_q = module->addWire(NEW_ID, inst->Input1Size());
+			sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
 
 			for (int i = int(inst->Input1Size())-1; i >= 0; i--){
 				sig_d.append(net_map_at(inst->GetInput1Bit(i)));
@@ -1198,8 +1277,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
 			}
 
-			clocking.addDff(NEW_ID, sig_d, sig_q);
-			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+			clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+			module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
 
 			if (!mode_keep)
 				continue;
@@ -1213,7 +1292,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 			SigSpec sig_d = net_map_at(inst->GetInput1());
 			SigSpec sig_o = net_map_at(inst->GetOutput());
-			SigSpec sig_q = module->addWire(NEW_ID);
+			SigSpec sig_q = module->addWire(new_verific_id(inst));
 
 			if (verific_verbose) {
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
@@ -1222,8 +1301,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
 			}
 
-			clocking.addDff(NEW_ID, sig_d, sig_q);
-			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+			clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+			module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
 
 			if (!mode_keep)
 				continue;
@@ -1242,7 +1321,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
 						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
 
-			past_ffs.insert(clocking.addDff(NEW_ID, sig_d, sig_q));
+			past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
 
 			if (!mode_keep)
 				continue;
@@ -1256,14 +1335,14 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 			SigBit sig_d = net_map_at(inst->GetInput1());
 			SigBit sig_o = net_map_at(inst->GetOutput());
-			SigBit sig_q = module->addWire(NEW_ID);
+			SigBit sig_q = module->addWire(new_verific_id(inst));
 
 			if (verific_verbose)
 				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
 						log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
 
-			clocking.addDff(NEW_ID, sig_d, sig_q);
-			module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
+			clocking.addDff(new_verific_id(inst), sig_d, sig_q);
+			module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
 
 			if (!mode_keep)
 				continue;
@@ -1286,9 +1365,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 			Cell *cell = nullptr;
 			if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
-				cell = module->addAssume(NEW_ID, cond, State::S1);
+				cell = module->addAssume(new_verific_id(inst), cond, State::S1);
 			else
-				cell = module->addAssert(NEW_ID, cond, State::S1);
+				cell = module->addAssert(new_verific_id(inst), cond, State::S1);
 
 			import_attributes(cell->attributes, inst);
 			continue;
@@ -1330,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			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));
+				SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
 				for (auto bit : zwires)
 					sigvec.push_back(bit);
 			}
@@ -1540,30 +1619,35 @@ struct VerificExtNets
 	int portname_cnt = 0;
 
 	// a map from Net to the same Net one level up in the design hierarchy
-	std::map<Net*, Net*> net_level_up;
+	std::map<Net*, Net*> net_level_up_drive_up;
+	std::map<Net*, Net*> net_level_up_drive_down;
 
-	Net *get_net_level_up(Net *net)
+	Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
 	{
+		auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
+
 		if (net_level_up.count(net) == 0)
 		{
 			Netlist *nl = net->Owner();
 
 			// Simply return if Netlist is not unique
-			if (nl->NumOfRefs() != 1)
-				return net;
+			log_assert(nl->NumOfRefs() == 1);
 
 			Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
 			Netlist *up_nl = up_inst->Owner();
 
 			// create new Port
 			string name = stringf("___extnets_%d", portname_cnt++);
-			Port *new_port = new Port(name.c_str(), DIR_OUT);
+			Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
 			nl->Add(new_port);
 			net->Connect(new_port);
 
 			// create new Net in up Netlist
-			Net *new_net = new Net(name.c_str());
-			up_nl->Add(new_net);
+			Net *new_net = final_net;
+			if (new_net == nullptr || new_net->Owner() != up_nl) {
+				new_net = new Net(name.c_str());
+				up_nl->Add(new_net);
+			}
 			up_inst->Connect(new_port, new_net);
 
 			net_level_up[net] = new_net;
@@ -1572,6 +1656,39 @@ struct VerificExtNets
 		return net_level_up.at(net);
 	}
 
+	Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
+	{
+		while (net->Owner() != dest)
+			net = route_up(net, drive_up, final_net);
+		if (final_net != nullptr)
+			log_assert(net == final_net);
+		return net;
+	}
+
+	Netlist *find_common_ancestor(Netlist *A, Netlist *B)
+	{
+		std::set<Netlist*> ancestors_of_A;
+
+		Netlist *cursor = A;
+		while (1) {
+			ancestors_of_A.insert(cursor);
+			if (cursor->NumOfRefs() != 1)
+				break;
+			cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+		}
+
+		cursor = B;
+		while (1) {
+			if (ancestors_of_A.count(cursor))
+				return cursor;
+			if (cursor->NumOfRefs() != 1)
+				break;
+			cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
+		}
+
+		log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str());
+	}
+
 	void run(Netlist *nl)
 	{
 		MapIter mi, mi2;
@@ -1595,19 +1712,37 @@ struct VerificExtNets
 			if (verific_verbose)
 				log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
 
-			while (net->IsExternalTo(nl))
-			{
-				Net *newnet = get_net_level_up(net);
-				if (newnet == net) break;
+			Netlist *ext_nl = net->Owner();
+
+			if (verific_verbose)
+				log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
+
+			Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
+
+			if (verific_verbose)
+				log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
 
+			Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
+			Net *new_net = ca_net;
+
+			if (ca_nl != nl)
+			{
 				if (verific_verbose)
-					log("  external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
-				net = newnet;
+					log(" net in common ancestor: %s\n", ca_net->Name());
+
+				string name = stringf("___extnets_%d", portname_cnt++);
+				new_net = new Net(name.c_str());
+				nl->Add(new_net);
+
+				Net *n = route_up(new_net, port->IsOutput(), ca_nl, ca_net);
+				log_assert(n == ca_net);
 			}
 
 			if (verific_verbose)
-				log("  final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
-			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
+				log(" new local net: %s\n", new_net->Name());
+
+			log_assert(!new_net->IsExternalTo(nl));
+			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
 		}
 
 		for (auto it : todo_connect) {
@@ -1676,6 +1811,7 @@ YOSYS_NAMESPACE_END
 
 PRIVATE_NAMESPACE_BEGIN
 
+#ifdef YOSYS_ENABLE_VERIFIC
 bool check_noverific_env()
 {
 	const char *e = getenv("YOSYS_NOVERIFIC");
@@ -1685,6 +1821,7 @@ bool check_noverific_env()
 		return false;
 	return true;
 }
+#endif
 
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
@@ -1774,6 +1911,13 @@ struct VerificPass : public Pass {
 		log("  -autocover\n");
 		log("    Generate automatic cover statements for all asserts\n");
 		log("\n");
+		log("  -chparam name value \n");
+		log("    Elaborate the specified top modules (all modules when -all given) using\n");
+		log("    this parameter value. Modules on which this parameter does not exist will\n");
+		log("    cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
+		log("    can be specified multiple times to override multiple parameters.\n");
+		log("    String values must be passed in double quotes (\").\n");
+		log("\n");
 		log("  -v, -vv\n");
 		log("    Verbose log messages. (-vv is even more verbose than -v.)\n");
 		log("\n");
@@ -1819,12 +1963,19 @@ struct VerificPass : public Pass {
 		{
 			Message::SetConsoleOutput(0);
 			Message::RegisterCallBackMsg(msg_func);
+
 			RuntimeFlags::SetVar("db_preserve_user_nets", 1);
 			RuntimeFlags::SetVar("db_allow_external_nets", 1);
-			RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+			RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+
 			RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
 			RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
-			RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+
+			RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
+			RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
+
+			RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
+			RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
 
 			// Workaround for VIPER #13851
 			RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
@@ -1832,6 +1983,10 @@ struct VerificPass : public Pass {
 			// WARNING: instantiating unknown module 'XYZ' (VERI-1063)
 			Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
 
+#ifndef DB_PRESERVE_INITIAL_VALUE
+#  warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
+#endif
+
 			set_verific_global_flags = false;
 		}
 
@@ -2017,6 +2172,7 @@ struct VerificPass : public Pass {
 			bool mode_autocover = false;
 			bool flatten = false, extnets = false;
 			string dumpfile;
+			Map parameters(STRING_HASH);
 
 			for (argidx++; argidx < GetSize(args); argidx++) {
 				if (args[argidx] == "-all") {
@@ -2055,6 +2211,15 @@ struct VerificPass : public Pass {
 					mode_autocover = true;
 					continue;
 				}
+				if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
+                                        const std::string &key = args[++argidx];
+                                        const std::string &value = args[++argidx];
+					unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
+									           1 /* force_overwrite */);
+					if (!new_insertion)
+						log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
+					continue;
+				}
 				if (args[argidx] == "-V") {
 					mode_verific = true;
 					continue;
@@ -2079,42 +2244,6 @@ struct VerificPass : public Pass {
 
 			if (mode_all)
 			{
-#if 0
-				log("Running veri_file::ElaborateAll().\n");
-				if (!veri_file::ElaborateAll())
-					log_cmd_error("Elaboration of Verilog modules failed.\n");
-
-				log("Running vhdl_file::ElaborateAll().\n");
-				if (!vhdl_file::ElaborateAll())
-					log_cmd_error("Elaboration of VHDL modules failed.\n");
-
-				Library *lib = Netlist::PresentDesign()->Owner()->Owner();
-
-				if (argidx == GetSize(args))
-				{
-					MapIter iter;
-					char *iter_name;
-					Verific::Cell *iter_cell;
-
-					FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) {
-						if (*iter_name != '$')
-							nl_todo.insert(iter_cell->GetFirstNetlist());
-					}
-				}
-				else
-				{
-					for (; argidx < GetSize(args); argidx++)
-					{
-						Verific::Cell *cell = lib->GetCell(args[argidx].c_str());
-
-						if (cell == nullptr)
-							log_cmd_error("Module not found: %s\n", args[argidx].c_str());
-
-						nl_todo.insert(cell->GetFirstNetlist());
-						cell->GetFirstNetlist()->SetPresentDesign();
-					}
-				}
-#else
 				log("Running hier_tree::ElaborateAll().\n");
 
 				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
@@ -2124,35 +2253,19 @@ struct VerificPass : public Pass {
 				if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
 				if (veri_lib) veri_libs.InsertLast(veri_lib);
 
-				Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+				Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
 				Netlist *nl;
 				int i;
 
 				FOREACH_ARRAY_ITEM(netlists, i, nl)
 					nl_todo.insert(nl);
 				delete netlists;
-#endif
 			}
 			else
 			{
 				if (argidx == GetSize(args))
 					log_cmd_error("No top module specified.\n");
 
-#if 0
-				for (; argidx < GetSize(args); argidx++) {
-					if (veri_file::GetModule(args[argidx].c_str())) {
-						log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
-						if (!veri_file::Elaborate(args[argidx].c_str()))
-							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
-						nl_todo.insert(Netlist::PresentDesign());
-					} else {
-						log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
-						if (!vhdl_file::Elaborate(args[argidx].c_str()))
-							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
-						nl_todo.insert(Netlist::PresentDesign());
-					}
-				}
-#else
 				Array veri_modules, vhdl_units;
 				for (; argidx < GetSize(args); argidx++)
 				{
@@ -2177,14 +2290,13 @@ struct VerificPass : public Pass {
 				}
 
 				log("Running hier_tree::Elaborate().\n");
-				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units);
+				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
 				Netlist *nl;
 				int i;
 
 				FOREACH_ARRAY_ITEM(netlists, i, nl)
 					nl_todo.insert(nl);
 				delete netlists;
-#endif
 			}
 
 			if (!verific_error_msg.empty())
@@ -2274,21 +2386,43 @@ struct ReadPass : public Pass {
 		log("\n");
 		log("Add directory to global Verilog/SystemVerilog include directories.\n");
 		log("\n");
+		log("\n");
+		log("    read -verific\n");
+		log("    read -noverific\n");
+		log("\n");
+		log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
+		log("with -verific will result in an error on Yosys binaries that are built without\n");
+		log("Verific support. The default is to use Verific if it is available.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		if (args.size() < 2)
+#ifdef YOSYS_ENABLE_VERIFIC
+		static bool verific_available = !check_noverific_env();
+#else
+		static bool verific_available = false;
+#endif
+		static bool use_verific = verific_available;
+
+		if (args.size() < 2 || args[1][0] != '-')
 			log_cmd_error("Missing mode parameter.\n");
 
+		if (args[1] == "-verific" || args[1] == "-noverific") {
+			if (args.size() != 2)
+				log_cmd_error("Additional arguments to -verific/-noverific.\n");
+			if (args[1] == "-verific") {
+				if (!verific_available)
+					log_cmd_error("This version of Yosys is built without Verific support.\n");
+				use_verific = true;
+			} else {
+				use_verific = false;
+			}
+			return;
+		}
+
 		if (args.size() < 3)
 			log_cmd_error("Missing file name parameter.\n");
 
-#ifdef YOSYS_ENABLE_VERIFIC
-		bool use_verific = !check_noverific_env();
-#else
-		bool use_verific = false;
-#endif
-
 		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
 			if (use_verific) {
 				args[0] = "verific";
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 334a436a..b331dd4b 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -78,6 +78,7 @@ struct VerificImporter
 
 	RTLIL::SigBit net_map_at(Verific::Net *net);
 
+	RTLIL::IdString new_verific_id(Verific::DesignObj *obj);
 	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj);
 
 	RTLIL::SigSpec operatorInput(Verific::Instance *inst);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index cdc9ece8..8ea8372d 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -827,9 +827,9 @@ struct SvaFsm
 
 			for (auto &it : nodes[i].edges) {
 				if (it.second != State::S1)
-					log("          egde %s -> %d\n", log_signal(it.second), it.first);
+					log("          edge %s -> %d\n", log_signal(it.second), it.first);
 				else
-					log("          egde -> %d\n", it.first);
+					log("          edge -> %d\n", it.first);
 			}
 
 			for (auto &it : nodes[i].links) {
@@ -856,9 +856,9 @@ struct SvaFsm
 
 			for (auto &it : unodes[i].edges) {
 				if (!it.second.empty())
-					log("          egde %s -> %d\n", log_signal(it.second), it.first);
+					log("          edge %s -> %d\n", log_signal(it.second), it.first);
 				else
-					log("          egde -> %d\n", it.first);
+					log("          edge -> %d\n", it.first);
 			}
 
 			for (auto &ctrl : unodes[i].accept) {
@@ -1666,7 +1666,20 @@ struct VerificSvaImporter
 				log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
 						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
 
-			RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+			bool is_user_declared = root->IsUserDeclared();
+
+			// FIXME
+			if (!is_user_declared) {
+				const char *name = root->Name();
+				for (int i = 0; name[i]; i++) {
+					if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
+						is_user_declared = true;
+						break;
+					}
+				}
+			}
+
+			RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
 			// parse SVA sequence into trigger signal