mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 17:44:09 +00:00
Code Activity

Ganulate Verific support

Browse source
This commit is contained in:
Miodrag Milanovic 2021-02-12 10:08:43 +01:00
parent 17c895cbf8
commit 13c2fd7137
1 changed files with 16 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
frontends/verific/verific.cc
View file

@ -49,13 +49,16 @@ USING_YOSYS_NAMESPACE
#include "VeriWrite.h" #include "VeriWrite.h"
#include "VhdlUnits.h" #include "VhdlUnits.h"
#include "VeriLibrary.h" #include "VeriLibrary.h"
#if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS)
#include "VeriExtensions.h" #include "VeriExtensions.h"
#endif
#ifndef YOSYSHQ_VERIFIC_API_VERSION #ifndef YOSYSHQ_VERIFIC_API_VERSION
# error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific." # error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
#endif #endif
#if YOSYSHQ_VERIFIC_API_VERSION < 20210101 #if YOSYSHQ_VERIFIC_API_VERSION < 20210103
# error "Please update your version of YosysHQ flavored Verific." # error "Please update your version of YosysHQ flavored Verific."
#endif #endif
@ -1471,6 +1474,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
#ifdef YOSYSHQ_VERIFIC_INITSTATE
if (inst->Type() == PRIM_YOSYSHQ_INITSTATE) if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
{ {
SigBit initstate = module->Initstate(new_verific_id(inst)); SigBit initstate = module->Initstate(new_verific_id(inst));
@ -1480,7 +1484,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (!mode_keep) if (!mode_keep)
continue; continue;
} }
#endif
if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (!mode_keep && verific_sva_prims.count(inst->Type())) {
if (verific_verbose) if (verific_verbose)
log(" skipping SVA cell in non k-mode\n"); log(" skipping SVA cell in non k-mode\n");
@ -1958,9 +1962,10 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
for (const auto &i : parameters) for (const auto &i : parameters)
verific_params.Insert(i.first.c_str(), i.second.c_str()); verific_params.Insert(i.first.c_str(), i.second.c_str());
#ifdef YOSYSHQ_VERIFIC_INITSTATE
InitialAssertionRewriter rw; InitialAssertionRewriter rw;
rw.RegisterCallBack(); rw.RegisterCallBack();
#endif
if (top.empty()) { if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
} }
@ -2217,7 +2222,7 @@ struct VerificPass : public Pass {
log("\n"); log("\n");
log("Applications:\n"); log("Applications:\n");
log("\n"); log("\n");
#ifdef YOSYS_ENABLE_VERIFIC #if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
VerificFormalApplications vfa; VerificFormalApplications vfa;
log("%s\n",vfa.GetHelp().c_str()); log("%s\n",vfa.GetHelp().c_str());
#else #else
@ -2243,7 +2248,7 @@ struct VerificPass : public Pass {
log("\n"); log("\n");
log("Templates:\n"); log("Templates:\n");
log("\n"); log("\n");
#ifdef YOSYS_ENABLE_VERIFIC #if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
VerificTemplateGenerator vfg; VerificTemplateGenerator vfg;
log("%s\n",vfg.GetHelp().c_str()); log("%s\n",vfg.GetHelp().c_str());
#else #else
@ -2494,6 +2499,7 @@ struct VerificPass : public Pass {
goto check_error; goto check_error;
} }
#ifdef YOSYSHQ_VERIFIC_FORMALAPPS
if (argidx < GetSize(args) && args[argidx] == "-app") if (argidx < GetSize(args) && args[argidx] == "-app")
{ {
if (!(argidx+1 < GetSize(args))) if (!(argidx+1 < GetSize(args)))
@ -2587,7 +2593,7 @@ struct VerificPass : public Pass {
} }
goto check_error; goto check_error;
} }
#endif
if (argidx < GetSize(args) && args[argidx] == "-pp") if (argidx < GetSize(args) && args[argidx] == "-pp")
{ {
const char* filename = nullptr; const char* filename = nullptr;
@ -2630,6 +2636,7 @@ struct VerificPass : public Pass {
goto check_error; goto check_error;
} }
#ifdef YOSYSHQ_VERIFIC_TEMPLATES
if (argidx < GetSize(args) && args[argidx] == "-template") if (argidx < GetSize(args) && args[argidx] == "-template")
{ {
if (!(argidx+1 < GetSize(args))) if (!(argidx+1 < GetSize(args)))
@ -2713,7 +2720,7 @@ struct VerificPass : public Pass {
fclose(of); fclose(of);
goto check_error; goto check_error;
} }
#endif
if (GetSize(args) > argidx && args[argidx] == "-import") if (GetSize(args) > argidx && args[argidx] == "-import")
{ {
std::set<Netlist*> nl_todo, nl_done; std::set<Netlist*> nl_todo, nl_done;
@ -2798,9 +2805,10 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names; std::set<std::string> top_mod_names;
#ifdef YOSYSHQ_VERIFIC_INITSTATE
InitialAssertionRewriter rw; InitialAssertionRewriter rw;
rw.RegisterCallBack(); rw.RegisterCallBack();
#endif
if (mode_all) if (mode_all)
{ {
log("Running hier_tree::ElaborateAll().\n"); log("Running hier_tree::ElaborateAll().\n");