verific: rewrite initial assume/asserts prior to elaboration

1 files changed, 36 insertions, 17 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 5f8a78e48..ae0970aac 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -48,6 +48,7 @@ USING_YOSYS_NAMESPACE
 #include "VeriWrite.h"
 #include "VhdlUnits.h"
 #include "VeriLibrary.h"
+#include "VeriExtensions.h"
 
 #ifndef SYMBIOTIC_VERIFIC_API_VERSION
 #  error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
@@ -1450,6 +1451,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 				continue;
 		}
 
+		if (inst->Type() == PRIM_SEDA_INITSTATE)
+		{
+			SigBit initstate = module->Initstate(new_verific_id(inst));
+			SigBit sig_o = net_map_at(inst->GetOutput());
+			module->connect(sig_o, initstate);
+
+			if (!mode_keep)
+				continue;
+		}
+
 		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
 			if (verific_verbose)
 				log("    skipping SVA cell in non k-mode\n");
@@ -1927,6 +1938,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
 	for (const auto &i : parameters)
 		verific_params.Insert(i.first.c_str(), i.second.c_str());
 
+	InitialAssertionRewriter rw;
+	rw.RegisterCallBack();
+
 	if (top.empty()) {
 		netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
 	}
@@ -2469,6 +2483,9 @@ struct VerificPass : public Pass {
 
 			std::set<std::string> top_mod_names;
 
+			InitialAssertionRewriter rw;
+			rw.RegisterCallBack();
+
 			if (mode_all)
 			{
 				log("Running hier_tree::ElaborateAll().\n");
@@ -2493,31 +2510,23 @@ struct VerificPass : public Pass {
 				if (argidx == GetSize(args))
 					cmd_error(args, argidx, "No top module specified.\n");
 
+				VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
+				VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
+
 				Array veri_modules, vhdl_units;
 				for (; argidx < GetSize(args); argidx++)
 				{
 					const char *name = args[argidx].c_str();
 					top_mod_names.insert(name);
-					VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
-
-					if (veri_lib) {
-						VeriModule *veri_module = veri_lib->GetModule(name, 1);
-						if (veri_module) {
-							log("Adding Verilog module '%s' to elaboration queue.\n", name);
-							veri_modules.InsertLast(veri_module);
-							continue;
-						}
 
-						// Also elaborate all root modules since they may contain bind statements
-						MapIter mi;
-						FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
-							if (!veri_module->IsRootModule()) continue;
-							veri_modules.InsertLast(veri_module);
-						}
+					VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr;
+					if (veri_module) {
+						log("Adding Verilog module '%s' to elaboration queue.\n", name);
+						veri_modules.InsertLast(veri_module);
+						continue;
 					}
 
-					VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
-					VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
+					VhdlDesignUnit *vhdl_unit = vhdl_lib ? vhdl_lib->GetPrimUnit(name) : nullptr;
 					if (vhdl_unit) {
 						log("Adding VHDL unit '%s' to elaboration queue.\n", name);
 						vhdl_units.InsertLast(vhdl_unit);
@@ -2527,6 +2536,16 @@ struct VerificPass : public Pass {
 					log_error("Can't find module/unit '%s'.\n", name);
 				}
 
+				if (veri_lib) {
+					// Also elaborate all root modules since they may contain bind statements
+					MapIter mi;
+					VeriModule *veri_module;
+					FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
+						if (!veri_module->IsRootModule()) continue;
+						veri_modules.InsertLast(veri_module);
+					}
+				}
+
 				log("Running hier_tree::Elaborate().\n");
 				Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
 				Netlist *nl;