From 9260e97aa28b245ee88d81d162bb6b83cbc5eab0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Aug 2019 15:31:49 +0200 Subject: [PATCH] Automatically prune init attributes in verific front-end, fixes #1237 Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 63 +++++++++++++++++++++++++++++++++--- frontends/verific/verific.h | 4 +-- kernel/celltypes.h | 19 ++++++++--- 3 files changed, 74 insertions(+), 12 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 06d58a44a..39a5a6b50 100644 --- 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 #include @@ -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 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 &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 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 88a6cc0ba..5cbd78f7b 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -72,9 +72,9 @@ struct VerificImporter pool 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 d2594bc46..d1d9bf943 100644 --- 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()); setup_type("$meminit", {ADDR, DATA}, pool());