#include "VeriWrite.h"
#include "VhdlUnits.h"
#include "VeriLibrary.h"
+
+#if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS)
#include "VeriExtensions.h"
+#endif
#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 < 20201201
+#if YOSYSHQ_VERIFIC_API_VERSION < 20210103
# error "Please update your version of YosysHQ flavored Verific."
#endif
continue;
}
+#ifdef YOSYSHQ_VERIFIC_INITSTATE
if (inst->Type() == PRIM_YOSYSHQ_INITSTATE)
{
SigBit initstate = module->Initstate(new_verific_id(inst));
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");
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
if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
}
log("\n");
log("Applications:\n");
log("\n");
-#ifdef YOSYS_ENABLE_VERIFIC
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
VerificFormalApplications vfa;
log("%s\n",vfa.GetHelp().c_str());
#else
log("\n");
log("Templates:\n");
log("\n");
-#ifdef YOSYS_ENABLE_VERIFIC
+#if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
VerificTemplateGenerator vfg;
log("%s\n",vfg.GetHelp().c_str());
#else
goto check_error;
}
+#ifdef YOSYSHQ_VERIFIC_FORMALAPPS
if (argidx < GetSize(args) && args[argidx] == "-app")
{
if (!(argidx+1 < GetSize(args)))
}
goto check_error;
}
-
+#endif
if (argidx < GetSize(args) && args[argidx] == "-pp")
{
const char* filename = nullptr;
goto check_error;
}
+#ifdef YOSYSHQ_VERIFIC_TEMPLATES
if (argidx < GetSize(args) && args[argidx] == "-template")
{
if (!(argidx+1 < GetSize(args)))
fclose(of);
goto check_error;
}
-
+#endif
if (GetSize(args) > argidx && args[argidx] == "-import")
{
std::set<Netlist*> nl_todo, nl_done;
std::set<std::string> top_mod_names;
+#ifdef YOSYSHQ_VERIFIC_INITSTATE
InitialAssertionRewriter rw;
rw.RegisterCallBack();
-
+#endif
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");