aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
authorMiodrag Milanovic <mmicko@gmail.com>2021-07-09 09:02:27 +0200
committerMiodrag Milanovic <mmicko@gmail.com>2021-07-09 09:02:27 +0200
commit7a5ac909858c22f2daf2f7ca63869c554dc3b9b5 (patch)
tree4c5e9c90348c05c9a508eb2922fdfdb4b367654a /frontends
parent4446cfa524cf06e84add450214f64b2de6e199c3 (diff)
downloadyosys-7a5ac909858c22f2daf2f7ca63869c554dc3b9b5.tar.gz
yosys-7a5ac909858c22f2daf2f7ca63869c554dc3b9b5.tar.bz2
yosys-7a5ac909858c22f2daf2f7ca63869c554dc3b9b5.zip
Update to latest Verific with extensions for initial assertions
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verific/verific.cc23
1 files changed, 9 insertions, 14 deletions
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");