Fix "verific -extnets" for more complex situations

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

2 files changed, 93 insertions, 15 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c412cd3a3..95b7d3586 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1619,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;
@@ -1651,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;
@@ -1674,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) {
diff --git a/tests/sva/extnets.sv b/tests/sva/extnets.sv
new file mode 100644
index 000000000..47312de7a
--- /dev/null
+++ b/tests/sva/extnets.sv
@@ -0,0 +1,22 @@
+module top(input i, output o);
+	A A();
+	B B();
+	assign A.i = i;
+	assign o = B.o;
+	always @* assert(o == i);
+endmodule
+
+module A;
+	wire i, y;
+`ifdef FAIL
+	assign B.x = i;
+`else
+	assign B.x = !i;
+`endif
+	assign y = !B.y;
+endmodule
+
+module B;
+	wire x, y, o;
+	assign y = x, o = A.y;
+endmodule