Automatically prune init attributes in verific front-end, fixes #1237

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

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 06d58a44ab46ad8057d0f9fc478296f9355d04b9..39a5a6b5076ba17649fbade294a556aa60e7498e 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -19,6 +19,7 @@
 
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
 #include "kernel/log.h"
 #include <stdlib.h>
 #include <stdio.h>
@@ -111,9 +112,10 @@ string get_full_netlist_name(Netlist *nl)
 
 // ==================================================================
 
-VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover) :
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
                mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
-               mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover)
+               mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
+               mode_fullinit(mode_fullinit)
 {
 }
 
@@ -1454,6 +1456,50 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
                merge_past_ffs(past_ffs);
        }
+
+       if (!mode_fullinit)
+       {
+               pool<SigBit> non_ff_bits;
+               CellTypes ff_types;
+
+               ff_types.setup_internals_ff();
+               ff_types.setup_stdcells_mem();
+
+               for (auto cell : module->cells())
+               {
+                       if (ff_types.cell_known(cell->type))
+                               continue;
+
+                       for (auto conn : cell->connections())
+                       {
+                               if (!cell->output(conn.first))
+                                       continue;
+
+                               for (auto bit : conn.second)
+                                       if (bit.wire != nullptr)
+                                               non_ff_bits.insert(bit);
+                       }
+               }
+
+               for (auto wire : module->wires())
+               {
+                       if (!wire->attributes.count("\\init"))
+                               continue;
+
+                       Const &initval = wire->attributes.at("\\init");
+                       for (int i = 0; i < GetSize(initval); i++)
+                       {
+                               if (initval[i] != State::S0 && initval[i] != State::S1)
+                                       continue;
+
+                               if (non_ff_bits.count(SigBit(wire, i)))
+                                       initval[i] = State::Sx;
+                       }
+
+                       if (initval.is_fully_undef())
+                               wire->attributes.erase("\\init");
+               }
+       }
 }
 
 // ==================================================================
@@ -1829,7 +1875,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
        while (!nl_todo.empty()) {
                Netlist *nl = *nl_todo.begin();
                if (nl_done.count(nl) == 0) {
-                       VerificImporter importer(false, false, false, false, false, false);
+                       VerificImporter importer(false, false, false, false, false, false, false);
                        importer.import_netlist(design, nl, nl_todo);
                }
                nl_todo.erase(nl);
@@ -1952,6 +1998,9 @@ struct VerificPass : public Pass {
                log("  -autocover\n");
                log("    Generate automatic cover statements for all asserts\n");
                log("\n");
+               log("  -fullinit\n");
+               log("    Keep all register initializations, even those for non-FF registers.\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");
@@ -2213,7 +2262,7 @@ struct VerificPass : public Pass {
                        std::set<Netlist*> nl_todo, nl_done;
                        bool mode_all = false, mode_gates = false, mode_keep = false;
                        bool mode_nosva = false, mode_names = false, mode_verific = false;
-                       bool mode_autocover = false;
+                       bool mode_autocover = false, mode_fullinit = false;
                        bool flatten = false, extnets = false;
                        string dumpfile;
                        Map parameters(STRING_HASH);
@@ -2255,6 +2304,10 @@ struct VerificPass : public Pass {
                                        mode_autocover = true;
                                        continue;
                                }
+                               if (args[argidx] == "-fullinit") {
+                                       mode_fullinit = true;
+                                       continue;
+                               }
                                if (args[argidx] == "-chparam"  && argidx+2 < GetSize(args)) {
                                        const std::string &key = args[++argidx];
                                        const std::string &value = args[++argidx];
@@ -2378,7 +2431,7 @@ struct VerificPass : public Pass {
                                Netlist *nl = *nl_todo.begin();
                                if (nl_done.count(nl) == 0) {
                                        VerificImporter importer(mode_gates, mode_keep, mode_nosva,
-                                                       mode_names, mode_verific, mode_autocover);
+                                                       mode_names, mode_verific, mode_autocover, mode_fullinit);
                                        importer.import_netlist(design, nl, nl_todo);
                                }
                                nl_todo.erase(nl);

diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 88a6cc0ba1752fd1fa661fc18eccd2298c9766f2..5cbd78f7b576cc9e548887cef97b7b1bf53b396a 100644 (file)
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -72,9 +72,9 @@ struct VerificImporter
        pool<Verific::Net*, hash_ptr_ops> any_all_nets;
 
        bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
-       bool mode_autocover;
+       bool mode_autocover, mode_fullinit;
 
-       VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover);
+       VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
 
        RTLIL::SigBit net_map_at(Verific::Net *net);
 

diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index d2594bc46c1f79021be564f92d696c1a660ea3ab..d1d9bf9438ac12d3696577c99d6a54b6bd438b39 100644 (file)
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -139,13 +139,10 @@ struct CellTypes
                setup_type("$fa", {A, B, C}, {X, Y}, true);
        }
 
-       void setup_internals_mem()
+       void setup_internals_ff()
        {
                IdString SET = "\\SET", CLR = "\\CLR", CLK = "\\CLK", ARST = "\\ARST", EN = "\\EN";
-               IdString Q = "\\Q", D = "\\D", ADDR = "\\ADDR", DATA = "\\DATA", RD_EN = "\\RD_EN";
-               IdString RD_CLK = "\\RD_CLK", RD_ADDR = "\\RD_ADDR", WR_CLK = "\\WR_CLK", WR_EN = "\\WR_EN";
-               IdString WR_ADDR = "\\WR_ADDR", WR_DATA = "\\WR_DATA", RD_DATA = "\\RD_DATA";
-               IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT";
+               IdString Q = "\\Q", D = "\\D";
 
                setup_type("$sr", {SET, CLR}, {Q});
                setup_type("$ff", {D}, {Q});
@@ -156,6 +153,18 @@ struct CellTypes
                setup_type("$dlatch", {EN, D}, {Q});
                setup_type("$dlatchsr", {EN, SET, CLR, D}, {Q});
 
+       }
+
+       void setup_internals_mem()
+       {
+               setup_internals_ff();
+
+               IdString CLK = "\\CLK", ARST = "\\ARST", EN = "\\EN";
+               IdString ADDR = "\\ADDR", DATA = "\\DATA", RD_EN = "\\RD_EN";
+               IdString RD_CLK = "\\RD_CLK", RD_ADDR = "\\RD_ADDR", WR_CLK = "\\WR_CLK", WR_EN = "\\WR_EN";
+               IdString WR_ADDR = "\\WR_ADDR", WR_DATA = "\\WR_DATA", RD_DATA = "\\RD_DATA";
+               IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT";
+
                setup_type("$memrd", {CLK, EN, ADDR}, {DATA});
                setup_type("$memwr", {CLK, EN, ADDR, DATA}, pool<RTLIL::IdString>());
                setup_type("$meminit", {ADDR, DATA}, pool<RTLIL::IdString>());