aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
diff options
context:
space:
mode:
Diffstat (limited to 'frontends/verific')
-rw-r--r--frontends/verific/verific.cc490
-rw-r--r--frontends/verific/verific.h12
-rw-r--r--frontends/verific/verificsva.cc360
3 files changed, 718 insertions, 144 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7b5dac309..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] ",
@@ -99,9 +102,9 @@ string get_full_netlist_name(Netlist *nl)
// ==================================================================
-VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific) :
+VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
- mode_names(mode_names), mode_verific(mode_verific)
+ mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover)
{
}
@@ -123,8 +126,11 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
// FIXME: Parse numeric attributes
- FOREACH_ATTRIBUTE(obj, mi, attr)
+ FOREACH_ATTRIBUTE(obj, mi, attr) {
+ if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
+ continue;
attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+ }
}
RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
@@ -186,12 +192,12 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
}
}
-RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
+RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
{
RTLIL::SigSpec sig;
RTLIL::Wire *dummy_wire = NULL;
for (int i = int(inst->OutputSize())-1; i >= 0; i--)
- if (inst->GetOutputBit(i)) {
+ if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
sig.append(net_map_at(inst->GetOutputBit(i)));
dummy_wire = NULL;
} else {
@@ -241,7 +247,9 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
}
if (inst->Type() == PRIM_BUF) {
- module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ auto outnet = inst->GetOutput();
+ if (!any_all_nets.count(outnet))
+ module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
return true;
}
@@ -391,6 +399,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
#define IN1 operatorInput1(inst)
#define IN2 operatorInput2(inst)
#define OUT operatorOutput(inst)
+ #define FILTERED_OUT operatorOutput(inst, &any_all_nets)
#define SIGNED inst->View()->IsSigned()
if (inst->Type() == OPER_ADDER) {
@@ -522,7 +531,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
}
if (inst->Type() == OPER_WIDE_BUF) {
- module->addPos(inst_name, IN, OUT, SIGNED);
+ module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
return true;
}
@@ -786,8 +795,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
module->fixup_ports();
dict<Net*, char, hash_ptr_ops> init_nets;
- pool<Net*, hash_ptr_ops> anyconst_nets;
- pool<Net*, hash_ptr_ops> anyseq_nets;
+ pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
+ pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
+ any_all_nets.clear();
FOREACH_NET_OF_NETLIST(nl, mi, net)
{
@@ -862,11 +872,36 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
const char *rand_const_attr = net->GetAttValue(" rand_const");
const char *rand_attr = net->GetAttValue(" rand");
- if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
- anyconst_nets.insert(net);
+ const char *anyconst_attr = net->GetAttValue("anyconst");
+ const char *anyseq_attr = net->GetAttValue("anyseq");
+
+ const char *allconst_attr = net->GetAttValue("allconst");
+ const char *allseq_attr = net->GetAttValue("allseq");
- else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
+ if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
+ anyconst_nets.insert(net);
+ any_all_nets.insert(net);
+ }
+ else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
+ anyseq_nets.insert(net);
+ any_all_nets.insert(net);
+ }
+ else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
+ anyconst_nets.insert(net);
+ any_all_nets.insert(net);
+ }
+ else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
anyseq_nets.insert(net);
+ any_all_nets.insert(net);
+ }
+ else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
+ allconst_nets.insert(net);
+ any_all_nets.insert(net);
+ }
+ else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
+ allseq_nets.insert(net);
+ any_all_nets.insert(net);
+ }
if (net_map.count(net)) {
if (verific_verbose)
@@ -951,6 +986,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
SigSpec anyconst_sig;
SigSpec anyseq_sig;
+ SigSpec allconst_sig;
+ SigSpec allseq_sig;
for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
net = netbus->ElementAtIndex(i);
@@ -962,6 +999,14 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
anyseq_sig.append(net_map_at(net));
anyseq_nets.erase(net);
}
+ if (net != nullptr && allconst_nets.count(net)) {
+ allconst_sig.append(net_map_at(net));
+ allconst_nets.erase(net);
+ }
+ if (net != nullptr && allseq_nets.count(net)) {
+ allseq_sig.append(net_map_at(net));
+ allseq_nets.erase(net);
+ }
if (i == netbus->LeftIndex())
break;
}
@@ -971,6 +1016,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (GetSize(anyseq_sig))
module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
+
+ if (GetSize(allconst_sig))
+ module->connect(allconst_sig, module->Allconst(NEW_ID, GetSize(allconst_sig)));
+
+ if (GetSize(allseq_sig))
+ module->connect(allseq_sig, module->Allseq(NEW_ID, GetSize(allseq_sig)));
}
for (auto it : init_nets)
@@ -1027,7 +1078,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
}
if (inst->Type() == PRIM_BUF) {
- module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+ auto outnet = inst->GetOutput();
+ if (!any_all_nets.count(outnet))
+ module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
continue;
}
@@ -1044,23 +1097,30 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == OPER_READ_PORT)
{
RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
- if (memory->width != int(inst->OutputSize()))
- log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+ int numchunks = int(inst->OutputSize()) / memory->width;
+ int chunksbits = ceil_log2(numchunks);
- RTLIL::SigSpec addr = operatorInput1(inst);
- RTLIL::SigSpec data = operatorOutput(inst);
+ if ((numchunks * memory->width) != int(inst->OutputSize()) || (numchunks & (numchunks - 1)) != 0)
+ log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
- RTLIL::Cell *cell = module->addCell(inst_name, "$memrd");
- cell->parameters["\\MEMID"] = memory->name.str();
- cell->parameters["\\CLK_ENABLE"] = false;
- cell->parameters["\\CLK_POLARITY"] = true;
- cell->parameters["\\TRANSPARENT"] = false;
- cell->parameters["\\ABITS"] = GetSize(addr);
- cell->parameters["\\WIDTH"] = GetSize(data);
- cell->setPort("\\CLK", RTLIL::State::Sx);
- cell->setPort("\\EN", RTLIL::State::Sx);
- cell->setPort("\\ADDR", addr);
- cell->setPort("\\DATA", data);
+ for (int i = 0; i < numchunks; i++)
+ {
+ RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
+ RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
+
+ RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
+ RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memrd");
+ cell->parameters["\\MEMID"] = memory->name.str();
+ cell->parameters["\\CLK_ENABLE"] = false;
+ cell->parameters["\\CLK_POLARITY"] = true;
+ cell->parameters["\\TRANSPARENT"] = false;
+ cell->parameters["\\ABITS"] = GetSize(addr);
+ cell->parameters["\\WIDTH"] = GetSize(data);
+ cell->setPort("\\CLK", RTLIL::State::Sx);
+ cell->setPort("\\EN", RTLIL::State::Sx);
+ cell->setPort("\\ADDR", addr);
+ cell->setPort("\\DATA", data);
+ }
continue;
}
@@ -1068,7 +1128,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
{
RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
if (memory->width != int(inst->Input2Size()))
- log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+ log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
RTLIL::SigSpec addr = operatorInput1(inst);
RTLIL::SigSpec data = operatorInput2(inst);
@@ -1214,11 +1274,27 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue;
}
- if (inst->IsPrimitive())
+ if (inst->Type() == PRIM_HDL_ASSERTION)
{
- if (inst->Type() == PRIM_HDL_ASSERTION)
- continue;
+ SigBit cond = net_map_at(inst->GetInput());
+ if (verific_verbose)
+ log(" assert condition %s.\n", log_signal(cond));
+
+ const char *assume_attr = nullptr; // inst->GetAttValue("assume");
+
+ Cell *cell = nullptr;
+ if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
+ cell = module->addAssume(NEW_ID, cond, State::S1);
+ else
+ cell = module->addAssert(NEW_ID, cond, State::S1);
+
+ import_attributes(cell->attributes, inst);
+ continue;
+ }
+
+ if (inst->IsPrimitive())
+ {
if (!mode_keep)
log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
@@ -1272,8 +1348,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (!mode_nosva)
{
- for (auto inst : sva_asserts)
+ for (auto inst : sva_asserts) {
+ if (mode_autocover)
+ verific_import_sva_cover(this, inst);
verific_import_sva_assert(this, inst);
+ }
for (auto inst : sva_assumes)
verific_import_sva_assume(this, inst);
@@ -1290,7 +1369,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
// ==================================================================
-VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
+VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
{
module = importer->module;
@@ -1313,8 +1392,14 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
body_net = body_inst->GetInput2();
}
}
+ else
+ {
+ if (sva_at_only)
+ return;
+ }
- if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
+ // Use while() instead of if() to work around VIPER #13453
+ while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
{
net = inst->GetInput();
inst = net->Driver();;
@@ -1388,6 +1473,10 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
clock_net = net;
clock_sig = importer->net_map_at(clock_net);
+
+ const char *gclk_attr = clock_net->GetAttValue("gclk");
+ if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
+ gclk = true;
}
Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
@@ -1410,15 +1499,20 @@ Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
if (disable_sig != State::S0) {
+ log_assert(gclk == false);
log_assert(GetSize(sig_q) == GetSize(init_value));
return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
}
+ if (gclk)
+ return module->addFf(name, sig_d, sig_q);
+
return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
}
Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
{
+ log_assert(gclk == false);
log_assert(disable_sig == State::S0);
if (enable_sig != State::S1)
@@ -1429,6 +1523,7 @@ Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec s
Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
{
+ log_assert(gclk == false);
log_assert(disable_sig == State::S0);
if (enable_sig != State::S1)
@@ -1521,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()
@@ -1536,6 +1693,18 @@ struct VerificPass : public Pass {
log("\n");
log("Load the specified Verilog/SystemVerilog files into Verific.\n");
log("\n");
+ log("All files specified in one call to this command are one compilation unit.\n");
+ 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");
@@ -1555,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");
@@ -1578,6 +1752,9 @@ struct VerificPass : public Pass {
log(" -extnets\n");
log(" Resolve references to external nets by adding module ports as needed.\n");
log("\n");
+ log(" -autocover\n");
+ log(" Generate automatic cover statements for all asserts\n");
+ log("\n");
log(" -v, -vv\n");
log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
log("\n");
@@ -1609,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);
@@ -1616,8 +1796,12 @@ struct VerificPass : public Pass {
RuntimeFlags::SetVar("db_preserve_user_nets", 1);
RuntimeFlags::SetVar("db_allow_external_nets", 1);
RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
- veri_file::DefineCmdLineMacro("VERIFIC");
- veri_file::DefineCmdLineMacro("SYNTHESIS");
+ RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
+ RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
+ RuntimeFlags::SetVar("db_infer_wide_operators", 1);
+
+ // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
+ Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
verific_verbose = 0;
@@ -1637,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;
}
@@ -1662,38 +1846,65 @@ struct VerificPass : public Pass {
goto check_error;
}
- if (GetSize(args) > argidx && args[argidx] == "-vlog95") {
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95))
- log_cmd_error("Reading `%s' in VERILOG_95 mode failed.\n", args[argidx].c_str());
+ 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] == "-vlog2k") {
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_2K))
- log_cmd_error("Reading `%s' in VERILOG_2K mode failed.\n", args[argidx].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] == "-formal"))
+ {
+ Array file_names;
+ unsigned verilog_mode;
+
+ if (args[argidx] == "-vlog95")
+ verilog_mode = veri_file::VERILOG_95;
+ else if (args[argidx] == "-vlog2k")
+ verilog_mode = veri_file::VERILOG_2K;
+ else if (args[argidx] == "-sv2005")
+ 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" || args[argidx] == "-formal")
+ verilog_mode = veri_file::SYSTEM_VERILOG;
+ else
+ log_abort();
- if (GetSize(args) > argidx && args[argidx] == "-sv2005") {
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2005))
- log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2005 mode failed.\n", args[argidx].c_str());
- goto check_error;
- }
+ veri_file::DefineMacro("VERIFIC");
+ veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
- if (GetSize(args) > argidx && args[argidx] == "-sv2009") {
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2009))
- log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2009 mode failed.\n", args[argidx].c_str());
- goto check_error;
- }
+ 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());
+ }
+ }
- if (GetSize(args) > argidx && (args[argidx] == "-sv2012" || args[argidx] == "-sv")) {
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG))
- log_cmd_error("Reading `%s' in SYSTEM_VERILOG mode failed.\n", args[argidx].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;
}
@@ -1702,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;
}
@@ -1710,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;
}
@@ -1718,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;
}
@@ -1726,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;
}
@@ -1734,6 +1949,7 @@ struct VerificPass : public Pass {
std::set<Netlist*> nl_todo, nl_done;
bool mode_all = false, mode_gates = false, mode_keep = false;
bool mode_nosva = false, mode_names = false, mode_verific = false;
+ bool mode_autocover = false;
bool flatten = false, extnets = false;
string dumpfile;
@@ -1766,6 +1982,10 @@ struct VerificPass : public Pass {
mode_names = true;
continue;
}
+ if (args[argidx] == "-autocover") {
+ mode_autocover = true;
+ continue;
+ }
if (args[argidx] == "-V") {
mode_verific = true;
continue;
@@ -1898,6 +2118,9 @@ struct VerificPass : public Pass {
#endif
}
+ if (!verific_error_msg.empty())
+ goto check_error;
+
if (flatten) {
for (auto nl : nl_todo)
nl->Flatten();
@@ -1918,7 +2141,7 @@ struct VerificPass : public Pass {
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
- mode_names, mode_verific);
+ mode_names, mode_verific, mode_autocover);
importer.import_netlist(design, nl, nl_todo);
}
nl_todo.erase(nl);
@@ -1928,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;
}
@@ -1945,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 877d79057..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;
@@ -40,9 +43,10 @@ struct VerificClocking {
SigBit enable_sig = State::S1;
SigBit disable_sig = State::S0;
bool posedge = true;
+ bool gclk = false;
VerificClocking() { }
- VerificClocking(VerificImporter *importer, Verific::Net *net);
+ VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
@@ -65,10 +69,12 @@ struct VerificImporter
std::map<Verific::Net*, RTLIL::SigBit> net_map;
std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
+ pool<Verific::Net*, hash_ptr_ops> any_all_nets;
bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
+ bool mode_autocover;
- VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific);
+ VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover);
RTLIL::SigBit net_map_at(Verific::Net *net);
@@ -78,7 +84,7 @@ struct VerificImporter
RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
- RTLIL::SigSpec operatorOutput(Verific::Instance *inst);
+ RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr);
bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 5abe0eb35..85b842186 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -21,14 +21,52 @@
// Currently supported SVA sequence and property syntax:
// http://symbiyosys.readthedocs.io/en/latest/verific.html
//
-// Todos:
-// property and property
-// sequence |-> always sequence
-// sequence |-> eventually sequence
-// sequence implies sequence
-// sequence iff sequence
-// accept_on (expr) prop
-// reject_on (expr) prop
+// Next gen property syntax:
+// basic_property
+// [antecedent_condition] property
+// [antecedent_condition] always.. property
+// [antecedent_condition] eventually.. basic_property
+// [antecedent_condition] property until.. expression
+// [antecedent_condition] basic_property until.. basic_property (assert/assume only)
+//
+// antecedent_condition:
+// sequence |->
+// sequence |=>
+//
+// basic_property:
+// sequence
+// not basic_property
+// sequence #-# basic_property
+// sequence #=# basic_property
+// basic_property or basic_property (cover only)
+// basic_property and basic_property (assert/assume only)
+// basic_property implies basic_property
+// basic_property iff basic_property
+//
+// sequence:
+// expression
+// sequence ##N sequence
+// sequence ##[*] sequence
+// sequence ##[+] sequence
+// sequence ##[N:M] sequence
+// sequence ##[N:$] sequence
+// expression [*]
+// expression [+]
+// expression [*N]
+// expression [*N:M]
+// expression [*N:$]
+// sequence or sequence
+// sequence and sequence
+// expression throughout sequence
+// sequence intersect sequence
+// sequence within sequence
+// first_match( sequence )
+// expression [=N]
+// expression [=N:M]
+// expression [=N:$]
+// expression [->N]
+// expression [->N:M]
+// expression [->N:$]
#include "kernel/yosys.h"
@@ -942,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)
{
@@ -1100,6 +1137,97 @@ struct VerificSvaImporter
log_abort();
}
+ bool check_zero_consecutive_repeat(Net *net)
+ {
+ Instance *inst = net_to_ast_driver(net);
+
+ if (inst == nullptr)
+ return false;
+
+ if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT)
+ return false;
+
+ const char *sva_low_s = inst->GetAttValue("sva:low");
+ int sva_low = atoi(sva_low_s);
+
+ return sva_low == 0;
+ }
+
+ int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay)
+ {
+ Instance *inst = net_to_ast_driver(net);
+
+ log_assert(inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT);
+
+ const char *sva_low_s = inst->GetAttValue("sva:low");
+ const char *sva_high_s = inst->GetAttValue("sva:high");
+
+ int sva_low = atoi(sva_low_s);
+ int sva_high = atoi(sva_high_s);
+ bool sva_inf = !strcmp(sva_high_s, "$");
+
+ Net *body_net = inst->GetInput();
+
+ if (add_pre_delay || add_post_delay)
+ log_assert(sva_low == 0);
+
+ if (sva_low == 0) {
+ if (!add_pre_delay && !add_post_delay)
+ parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst);
+ sva_low++;
+ }
+
+ int node = fsm.createNode(start_node);
+ start_node = node;
+
+ if (add_pre_delay) {
+ node = fsm.createNode(start_node);
+ fsm.createEdge(start_node, node);
+ }
+
+ int prev_node = node;
+ node = parse_sequence(fsm, node, body_net);
+
+ for (int i = 1; i < sva_low; i++)
+ {
+ int next_node = fsm.createNode();
+ fsm.createEdge(node, next_node);
+
+ prev_node = node;
+ node = parse_sequence(fsm, next_node, body_net);
+ }
+
+ if (sva_inf)
+ {
+ log_assert(prev_node >= 0);
+ fsm.createEdge(node, prev_node);
+ }
+ else
+ {
+ for (int i = sva_low; i < sva_high; i++)
+ {
+ int next_node = fsm.createNode();
+ fsm.createEdge(node, next_node);
+
+ prev_node = node;
+ node = parse_sequence(fsm, next_node, body_net);
+
+ fsm.createLink(prev_node, node);
+ }
+ }
+
+ if (add_post_delay) {
+ int next_node = fsm.createNode();
+ fsm.createEdge(node, next_node);
+ node = next_node;
+ }
+
+ if (add_pre_delay || add_post_delay)
+ fsm.createLink(start_node, node);
+
+ return node;
+ }
+
int parse_sequence(SvaFsm &fsm, int start_node, Net *net)
{
if (check_expression(net)) {
@@ -1144,7 +1272,20 @@ struct VerificSvaImporter
int sva_high = atoi(sva_high_s);
bool sva_inf = !strcmp(sva_high_s, "$");
- int node = parse_sequence(fsm, start_node, inst->GetInput1());
+ int node = -1;
+ bool past_add_delay = false;
+
+ if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) {
+ node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true);
+ sva_low--, sva_high--;
+ } else {
+ node = parse_sequence(fsm, start_node, inst->GetInput1());
+ }
+
+ if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) {
+ past_add_delay = true;
+ sva_low--, sva_high--;
+ }
for (int i = 0; i < sva_low; i++) {
int next_node = fsm.createNode();
@@ -1167,62 +1308,17 @@ struct VerificSvaImporter
}
}
- node = parse_sequence(fsm, node, inst->GetInput2());
+ if (past_add_delay)
+ node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false);
+ else
+ node = parse_sequence(fsm, node, inst->GetInput2());
return node;
}
if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
{
- const char *sva_low_s = inst->GetAttValue("sva:low");
- const char *sva_high_s = inst->GetAttValue("sva:high");
-
- int sva_low = atoi(sva_low_s);
- int sva_high = atoi(sva_high_s);
- bool sva_inf = !strcmp(sva_high_s, "$");
-
- Net *body_net = inst->GetInput();
- int node = fsm.createNode(start_node);
-
- for (int i = 0; i < sva_low; i++)
- {
- int next_node = fsm.createNode();
-
- if (i == 0)
- fsm.createLink(node, next_node);
- else
- fsm.createEdge(node, next_node);
-
- node = parse_sequence(fsm, next_node, body_net);
- }
-
- if (sva_inf)
- {
- int next_node = fsm.createNode();
- fsm.createEdge(node, next_node);
-
- next_node = parse_sequence(fsm, next_node, body_net);
- fsm.createLink(next_node, node);
- }
- else
- {
- for (int i = sva_low; i < sva_high; i++)
- {
- int next_node = fsm.createNode();
-
- if (i == 0)
- fsm.createLink(node, next_node);
- else
- fsm.createEdge(node, next_node);
-
- next_node = parse_sequence(fsm, next_node, body_net);
-
- fsm.createLink(node, next_node);
- node = next_node;
- }
- }
-
- return node;
+ return parse_consecutive_repeat(fsm, start_node, net, false, false);
}
if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT)
@@ -1390,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);
@@ -1505,20 +1667,65 @@ struct VerificSvaImporter
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
- clocking = VerificClocking(importer, root->GetInput());
+ // parse SVA sequence into trigger signal
+
+ clocking = VerificClocking(importer, root->GetInput(), true);
+ SigBit accept_bit = State::S0, reject_bit = State::S0;
if (clocking.body_net == nullptr)
- parser_error(stringf("Failed to parse SVA clocking"), root);
+ {
+ if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr || clocking.cond_net != nullptr)
+ parser_error(stringf("Failed to parse SVA clocking"), root);
- // parse SVA sequence into trigger signal
+ if (mode_assert || mode_assume) {
+ reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
+ } else {
+ accept_bit = parse_expression(root->GetInput());
+ }
+ }
+ else
+ {
+ Net *net = clocking.body_net;
+ SigBit trig;
- Net *net = clocking.body_net;
- SigBit accept_bit = State::S0, reject_bit = State::S0;
+ if (eventually_property(net, trig))
+ {
+ SigBit sig_a, sig_en = trig;
+ parse_property(net, &sig_a, nullptr);
- if (mode_assert || mode_assume) {
- parse_property(net, nullptr, &reject_bit);
- } else {
- parse_property(net, &accept_bit, 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);
+ }
+ }
}
if (mode_trigger)
@@ -1532,10 +1739,17 @@ struct VerificSvaImporter
// add final FF stage
- SigBit sig_a_q = module->addWire(NEW_ID);
- SigBit 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);
+ 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 assert/assume/cover cell
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-27 05:58:24 +0000