Fix "verific -extnets" for more complex situations

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

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c412cd3a3af951e60bfa8d1f92d3fff08419d8d2..95b7d3586d7b2e6da9918f835bc418ed862d9b18 100644 (file)
--- 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 (file)
index 0000000..47312de
--- /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