From: Miodrag Milanovic <mmicko@gmail.com>
Date: Fri, 9 Jul 2021 07:02:27 +0000 (+0200)
Subject: Update to latest Verific with extensions for initial assertions
X-Git-Tag: yosys-0.10~119
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a5ac909858c22f2daf2f7ca63869c554dc3b9b5;p=yosys.git

Update to latest Verific with extensions for initial assertions
---

diff --git a/Makefile b/Makefile
index d585512a5..42569ecd8 100644
--- a/Makefile
+++ b/Makefile
@@ -498,7 +498,7 @@ endif
 
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= /usr/local/src/verific_lib
-VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree
+VERIFIC_COMPONENTS ?= verilog vhdl database util containers hier_tree extensions
 CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
 ifeq ($(OS), Darwin)
 LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9e99af680..997a8e826 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -50,15 +50,13 @@ USING_YOSYS_NAMESPACE
 #include "VhdlUnits.h"
 #include "VeriLibrary.h"
 
-#if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS)
-#include "VeriExtensions.h"
-#endif
+#include "InitialAssertions.h"
 
 #ifndef YOSYSHQ_VERIFIC_API_VERSION
 #  error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
 #endif
 
-#if YOSYSHQ_VERIFIC_API_VERSION < 20210103
+#if YOSYSHQ_VERIFIC_API_VERSION < 20210602
 #  error "Please update your version of YosysHQ flavored Verific."
 #endif
 
@@ -1474,9 +1472,10 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 				continue;
 		}
 
-#ifdef YOSYSHQ_VERIFIC_INITSTATE
 		if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
 		{
+			if (verific_verbose)
+				log("   adding YosysHQ init state\n");
 			SigBit initstate = module->Initstate(new_verific_id(inst));
 			SigBit sig_o = net_map_at(inst->GetOutput());
 			module->connect(sig_o, initstate);
@@ -1484,7 +1483,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 			if (!mode_keep)
 				continue;
 		}
-#endif
+
 		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
 			if (verific_verbose)
 				log("    skipping SVA cell in non k-mode\n");
@@ -1962,10 +1961,8 @@ 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());
 
-#ifdef YOSYSHQ_VERIFIC_INITSTATE
-	InitialAssertionRewriter rw;
-	rw.RegisterCallBack();
-#endif
+	InitialAssertions::Rewrite("work");
+
 	if (top.empty()) {
 		netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
 	}
@@ -2850,10 +2847,8 @@ struct VerificPass : public Pass {
 
 			std::set<std::string> top_mod_names;
 
-#ifdef YOSYSHQ_VERIFIC_INITSTATE
-			InitialAssertionRewriter rw;
-			rw.RegisterCallBack();
-#endif
+			InitialAssertions::Rewrite(work);
+
 			if (mode_all)
 			{
 				log("Running hier_tree::ElaborateAll().\n");