aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
diff options
context:
space:
mode:
Diffstat (limited to 'frontends/verific')
-rw-r--r--frontends/verific/verific.cc271
-rw-r--r--frontends/verific/verific.h3
-rw-r--r--frontends/verific/verificsva.cc111
3 files changed, 370 insertions, 15 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index f67337754..b8dd72b98 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -62,8 +62,11 @@ using namespace Verific;
YOSYS_NAMESPACE_BEGIN
int verific_verbose;
+bool verific_import_pending;
string verific_error_msg;
+vector<string> verific_incdirs, verific_libdirs;
+
void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{
string message_prefix = stringf("VERIFIC-%s [%s] ",
@@ -1613,11 +1616,73 @@ struct VerificExtNets
}
};
+void verific_import(Design *design, std::string top)
+{
+ std::set<Netlist*> nl_todo, nl_done;
+
+ {
+ VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+ VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+
+ Array veri_libs, vhdl_libs;
+ if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+ if (veri_lib) veri_libs.InsertLast(veri_lib);
+
+ Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+ Netlist *nl;
+ int i;
+
+ FOREACH_ARRAY_ITEM(netlists, i, nl) {
+ if (top.empty() || nl->Owner()->Name() == top)
+ nl_todo.insert(nl);
+ }
+
+ delete netlists;
+ }
+
+ if (!verific_error_msg.empty())
+ log_error("%s\n", verific_error_msg.c_str());
+
+ VerificExtNets worker;
+ for (auto nl : nl_todo)
+ worker.run(nl);
+
+ while (!nl_todo.empty()) {
+ Netlist *nl = *nl_todo.begin();
+ if (nl_done.count(nl) == 0) {
+ VerificImporter importer(false, false, false, false, false, false);
+ importer.import_netlist(design, nl, nl_todo);
+ }
+ nl_todo.erase(nl);
+ nl_done.insert(nl);
+ }
+
+ veri_file::Reset();
+ vhdl_file::Reset();
+ Libset::Reset();
+ verific_incdirs.clear();
+ verific_libdirs.clear();
+ verific_import_pending = false;
+
+ if (!verific_error_msg.empty())
+ log_error("%s\n", verific_error_msg.c_str());
+}
+
YOSYS_NAMESPACE_END
#endif /* YOSYS_ENABLE_VERIFIC */
PRIVATE_NAMESPACE_BEGIN
+bool check_noverific_env()
+{
+ const char *e = getenv("YOSYS_NOVERIFIC");
+ if (e == nullptr)
+ return false;
+ if (atoi(e) == 0)
+ return false;
+ return true;
+}
+
struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
virtual void help()
@@ -1632,6 +1697,14 @@ struct VerificPass : public Pass {
log("Files passed to different calls to this command are treated as belonging to\n");
log("different compilation units.\n");
log("\n");
+ log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+ log("the language version (and before file names) to set additional verilog defines.\n");
+ log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
+ log("\n");
+ log("\n");
+ log(" verific -formal <verilog-file>..\n");
+ log("\n");
+ log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
log("\n");
log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
log("\n");
@@ -1651,7 +1724,12 @@ struct VerificPass : public Pass {
log("\n");
log(" verific -vlog-define <macro>[=<value>]..\n");
log("\n");
- log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
+ log("Add Verilog defines.\n");
+ log("\n");
+ log("\n");
+ log(" verific -vlog-undef <macro>..\n");
+ log("\n");
+ log("Remove Verilog defines previously set with -vlog-define.\n");
log("\n");
log("\n");
log(" verific -import [options] <top-module>..\n");
@@ -1708,6 +1786,9 @@ struct VerificPass : public Pass {
#ifdef YOSYS_ENABLE_VERIFIC
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
+ if (check_noverific_env())
+ log_cmd_error("This version of Yosys is built without Verific support.\n");
+
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
Message::SetConsoleOutput(0);
@@ -1718,8 +1799,9 @@ struct VerificPass : public Pass {
RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
RuntimeFlags::SetVar("db_infer_wide_operators", 1);
- veri_file::DefineCmdLineMacro("VERIFIC");
- veri_file::DefineCmdLineMacro("SYNTHESIS");
+
+ // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
+ Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
verific_verbose = 0;
@@ -1739,13 +1821,13 @@ struct VerificPass : public Pass {
if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
for (argidx++; argidx < GetSize(args); argidx++)
- veri_file::AddIncludeDir(args[argidx].c_str());
+ verific_incdirs.push_back(args[argidx]);
goto check_error;
}
if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
for (argidx++; argidx < GetSize(args); argidx++)
- veri_file::AddYDir(args[argidx].c_str());
+ verific_libdirs.push_back(args[argidx]);
goto check_error;
}
@@ -1764,8 +1846,16 @@ struct VerificPass : public Pass {
goto check_error;
}
+ if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
+ for (argidx++; argidx < GetSize(args); argidx++) {
+ string name = args[argidx];
+ veri_file::UndefineMacro(name.c_str());
+ }
+ goto check_error;
+ }
+
if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
- args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv"))
+ args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
{
Array file_names;
unsigned verilog_mode;
@@ -1778,17 +1868,43 @@ struct VerificPass : public Pass {
verilog_mode = veri_file::SYSTEM_VERILOG_2005;
else if (args[argidx] == "-sv2009")
verilog_mode = veri_file::SYSTEM_VERILOG_2009;
- else if (args[argidx] == "-sv2012" || args[argidx] == "-sv")
+ else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
verilog_mode = veri_file::SYSTEM_VERILOG;
else
log_abort();
- for (argidx++; argidx < GetSize(args); argidx++)
- file_names.Insert(args[argidx].c_str());
+ veri_file::DefineMacro("VERIFIC");
+ veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
+
+ for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
+ std::string name = args[argidx].substr(2);
+ if (args[argidx] == "-D") {
+ if (++argidx >= GetSize(args))
+ break;
+ name = args[argidx];
+ }
+ size_t equal = name.find('=');
+ if (equal != std::string::npos) {
+ string value = name.substr(equal+1);
+ name = name.substr(0, equal);
+ veri_file::DefineMacro(name.c_str(), value.c_str());
+ } else {
+ veri_file::DefineMacro(name.c_str());
+ }
+ }
+
+ for (auto &dir : verific_incdirs)
+ veri_file::AddIncludeDir(dir.c_str());
+ for (auto &dir : verific_libdirs)
+ veri_file::AddYDir(dir.c_str());
+
+ while (argidx < GetSize(args))
+ file_names.Insert(args[argidx++].c_str());
if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
+ verific_import_pending = true;
goto check_error;
}
@@ -1797,6 +1913,7 @@ struct VerificPass : public Pass {
for (argidx++; argidx < GetSize(args); argidx++)
if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
+ verific_import_pending = true;
goto check_error;
}
@@ -1805,6 +1922,7 @@ struct VerificPass : public Pass {
for (argidx++; argidx < GetSize(args); argidx++)
if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
+ verific_import_pending = true;
goto check_error;
}
@@ -1813,6 +1931,7 @@ struct VerificPass : public Pass {
for (argidx++; argidx < GetSize(args); argidx++)
if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
+ verific_import_pending = true;
goto check_error;
}
@@ -1821,6 +1940,7 @@ struct VerificPass : public Pass {
for (argidx++; argidx < GetSize(args); argidx++)
if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
+ verific_import_pending = true;
goto check_error;
}
@@ -2031,6 +2151,9 @@ struct VerificPass : public Pass {
veri_file::Reset();
vhdl_file::Reset();
Libset::Reset();
+ verific_incdirs.clear();
+ verific_libdirs.clear();
+ verific_import_pending = false;
goto check_error;
}
@@ -2048,5 +2171,133 @@ struct VerificPass : public Pass {
#endif
} VerificPass;
-PRIVATE_NAMESPACE_END
+struct ReadPass : public Pass {
+ ReadPass() : Pass("read", "load HDL designs") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
+ log("\n");
+ log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
+ log("is only available via Verific.)\n");
+ log("\n");
+ log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+ log("the language version (and before file names) to set additional verilog defines.\n");
+ log("\n");
+ log("\n");
+ log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
+ log("\n");
+ log("Load the specified VHDL files. (Requires Verific.)\n");
+ log("\n");
+ log("\n");
+ log(" read -define <macro>[=<value>]..\n");
+ log("\n");
+ log("Set global Verilog/SystemVerilog defines.\n");
+ log("\n");
+ log("\n");
+ log(" read -undef <macro>..\n");
+ log("\n");
+ log("Unset global Verilog/SystemVerilog defines.\n");
+ log("\n");
+ log("\n");
+ log(" read -incdir <directory>\n");
+ log("\n");
+ log("Add directory to global Verilog/SystemVerilog include directories.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ if (args.size() < 2)
+ log_cmd_error("Missing mode parameter.\n");
+
+ if (args.size() < 3)
+ log_cmd_error("Missing file name parameter.\n");
+
+#ifdef YOSYS_ENABLE_VERIFIC
+ bool use_verific = !check_noverific_env();
+#else
+ bool use_verific = false;
+#endif
+
+ if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
+ if (use_verific) {
+ args[0] = "verific";
+ } else {
+ args[0] = "read_verilog";
+ args.erase(args.begin()+1, args.begin()+2);
+ }
+ Pass::call(design, args);
+ return;
+ }
+
+ if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
+ if (use_verific) {
+ args[0] = "verific";
+ } else {
+ args[0] = "read_verilog";
+ if (args[1] == "-formal")
+ args.insert(args.begin()+1, std::string());
+ args[1] = "-sv";
+ }
+ Pass::call(design, args);
+ return;
+ }
+
+ if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
+ if (use_verific) {
+ args[0] = "verific";
+ Pass::call(design, args);
+ } else {
+ log_cmd_error("This version of Yosys is built without Verific support.\n");
+ }
+ return;
+ }
+
+ if (args[1] == "-define") {
+ if (use_verific) {
+ args[0] = "verific";
+ args[1] = "-vlog-define";
+ Pass::call(design, args);
+ }
+ args[0] = "verilog_defines";
+ args.erase(args.begin()+1, args.begin()+2);
+ for (int i = 1; i < GetSize(args); i++)
+ args[i] = "-D" + args[i];
+ Pass::call(design, args);
+ return;
+ }
+ if (args[1] == "-undef") {
+ if (use_verific) {
+ args[0] = "verific";
+ args[1] = "-vlog-undef";
+ Pass::call(design, args);
+ }
+ args[0] = "verilog_defines";
+ args.erase(args.begin()+1, args.begin()+2);
+ for (int i = 1; i < GetSize(args); i++)
+ args[i] = "-U" + args[i];
+ Pass::call(design, args);
+ return;
+ }
+
+ if (args[1] == "-incdir") {
+ if (use_verific) {
+ args[0] = "verific";
+ args[1] = "-vlog-incdir";
+ Pass::call(design, args);
+ }
+ args[0] = "verilog_defaults";
+ args[1] = "-add";
+ for (int i = 2; i < GetSize(args); i++)
+ args[i] = "-I" + args[i];
+ Pass::call(design, args);
+ return;
+ }
+
+ log_cmd_error("Missing or unsupported mode parameter.\n");
+ }
+} ReadPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 86a743ea1..cbd9314db 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -25,6 +25,9 @@ YOSYS_NAMESPACE_BEGIN
extern int verific_verbose;
+extern bool verific_import_pending;
+extern void verific_import(Design *design, std::string top = std::string());
+
extern pool<int> verific_sva_prims;
struct VerificImporter;
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4ca..85b842186 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -980,7 +980,6 @@ struct VerificSvaImporter
bool mode_assume = false;
bool mode_cover = false;
bool mode_trigger = false;
- bool eventually = false;
Instance *net_to_ast_driver(Net *n)
{
@@ -1487,6 +1486,72 @@ struct VerificSvaImporter
fsm.getFirstAcceptReject(accept_p, reject_p);
}
+ bool eventually_property(Net *&net, SigBit &trig)
+ {
+ Instance *inst = net_to_ast_driver(net);
+
+ if (inst == nullptr)
+ return false;
+
+ if (clocking.cond_net != nullptr)
+ trig = importer->net_map_at(clocking.cond_net);
+ else
+ trig = State::S1;
+
+ if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
+ {
+ if (mode_cover || mode_trigger)
+ parser_error(inst);
+
+ net = inst->GetInput();
+ clocking.cond_net = nullptr;
+
+ return true;
+ }
+
+ if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+ inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+ {
+ Net *antecedent_net = inst->GetInput1();
+ Net *consequent_net = inst->GetInput2();
+
+ Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+ if (consequent_inst == nullptr)
+ return false;
+
+ if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY)
+ return false;
+
+ if (mode_cover || mode_trigger)
+ parser_error(consequent_inst);
+
+ int node;
+
+ SvaFsm antecedent_fsm(clocking, trig);
+ node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
+ if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
+ int next_node = antecedent_fsm.createNode();
+ antecedent_fsm.createEdge(node, next_node);
+ node = next_node;
+ }
+ antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+ trig = antecedent_fsm.getAccept();
+ net = consequent_inst->GetInput();
+ clocking.cond_net = nullptr;
+
+ if (verific_verbose) {
+ log(" Eventually Antecedent FSM:\n");
+ antecedent_fsm.dump();
+ }
+
+ return true;
+ }
+
+ return false;
+ }
+
void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
{
Instance *inst = net_to_ast_driver(net);
@@ -1620,10 +1685,46 @@ struct VerificSvaImporter
}
else
{
- if (mode_assert || mode_assume) {
- parse_property(clocking.body_net, nullptr, &reject_bit);
- } else {
- parse_property(clocking.body_net, &accept_bit, nullptr);
+ Net *net = clocking.body_net;
+ SigBit trig;
+
+ if (eventually_property(net, trig))
+ {
+ SigBit sig_a, sig_en = trig;
+ parse_property(net, &sig_a, nullptr);
+
+ // add final FF stage
+
+ SigBit sig_a_q, sig_en_q;
+
+ if (clocking.body_net == nullptr) {
+ sig_a_q = sig_a;
+ sig_en_q = sig_en;
+ } else {
+ sig_a_q = module->addWire(NEW_ID);
+ sig_en_q = module->addWire(NEW_ID);
+ clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+ clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+ }
+
+ // generate fair/live cell
+
+ RTLIL::Cell *c = nullptr;
+
+ if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
+ if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
+
+ importer->import_attributes(c->attributes, root);
+
+ return;
+ }
+ else
+ {
+ if (mode_assert || mode_assume) {
+ parse_property(net, nullptr, &reject_bit);
+ } else {
+ parse_property(net, &accept_bit, nullptr);
+ }
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-06 07:36:05 +0000