From fc462c8243d60ebd769d5ce01142fb7ed49fa8f8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 29 Jul 2019 10:29:36 +0200 Subject: Call "read_verilog" with -defer from "read" Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 2bf99e58e..06d58a44a 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2484,7 +2484,7 @@ struct ReadPass : public Pass { args[0] = "verific"; } else { args[0] = "read_verilog"; - args.erase(args.begin()+1, args.begin()+2); + args[1] = "-defer"; } Pass::call(design, args); return; @@ -2498,6 +2498,7 @@ struct ReadPass : public Pass { if (args[1] == "-formal") args.insert(args.begin()+1, std::string()); args[1] = "-sv"; + args.insert(args.begin()+1, "-defer"); } Pass::call(design, args); return; -- cgit v1.2.3 From c11ad24fd7d961432cfdbca7497ba229d3b4f38d Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Tue, 6 Aug 2019 16:45:48 -0700 Subject: Use std::stoi instead of atoi(.c_str()) --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 06d58a44a..12c2f7ab8 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2244,7 +2244,7 @@ struct VerificPass : public Pass { continue; } if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { - verific_sva_fsm_limit = atoi(args[++argidx].c_str()); + verific_sva_fsm_limit = std::stoi(args[++argidx]); continue; } if (args[argidx] == "-n") { -- cgit v1.2.3 From 9260e97aa28b245ee88d81d162bb6b83cbc5eab0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Aug 2019 15:31:49 +0200 Subject: Automatically prune init attributes in verific front-end, fixes #1237 Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 63 ++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 58 insertions(+), 5 deletions(-) (limited to 'frontends/verific/verific.cc') 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); -- cgit v1.2.3 From 48d0f994064557dc0832748e17133ee2eac88cbf Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 7 Aug 2019 11:09:17 -0700 Subject: stoi -> atoi --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 12c2f7ab8..06d58a44a 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2244,7 +2244,7 @@ struct VerificPass : public Pass { continue; } if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { - verific_sva_fsm_limit = std::stoi(args[++argidx]); + verific_sva_fsm_limit = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-n") { -- cgit v1.2.3 From 6d77236f3845cd8785e7bdd4da3c5ef966be6043 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 7 Aug 2019 12:20:08 -0700 Subject: substr() -> compare() --- frontends/verific/verific.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 06d58a44a..594da45eb 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2140,7 +2140,7 @@ struct VerificPass : public Pass { veri_file::DefineMacro("VERIFIC"); veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS"); - for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) { + for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) { std::string name = args[argidx].substr(2); if (args[argidx] == "-D") { if (++argidx >= GetSize(args)) @@ -2283,7 +2283,7 @@ struct VerificPass : public Pass { break; } - if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-") + if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0) cmd_error(args, argidx, "unknown option"); if (mode_all) -- cgit v1.2.3 From 0c5db07cd6cc3c19b926da21a46599f97592b20f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 11 Aug 2019 23:25:46 +0200 Subject: Fix various NDEBUG compiler warnings, closes #1255 Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 2 ++ 1 file changed, 2 insertions(+) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 17c4a1e5b..64152c9cb 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1789,8 +1789,10 @@ struct VerificExtNets new_net = new Net(name.c_str()); nl->Add(new_net); + #ifndef NDEBUG Net *n = route_up(new_net, port->IsOutput(), ca_nl, ca_net); log_assert(n == ca_net); + #endif } if (verific_verbose) -- cgit v1.2.3 From 27d59dc0550432458d4bd636081a7b9f4b4411fe Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 17 Aug 2019 14:47:02 +0200 Subject: Fix erroneous ifndef-NDEBUG in verific.cc Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'frontends/verific/verific.cc') diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 64152c9cb..c5eef4b55 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1789,10 +1789,8 @@ struct VerificExtNets new_net = new Net(name.c_str()); nl->Add(new_net); - #ifndef NDEBUG - Net *n = route_up(new_net, port->IsOutput(), ca_nl, ca_net); + Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net); log_assert(n == ca_net); - #endif } if (verific_verbose) -- cgit v1.2.3