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

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

2 files changed, 60 insertions, 7 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 <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 88a6cc0ba..5cbd78f7b 100644
--- 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);