aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific/verific.cc
diff options
context:
space:
mode:
Diffstat (limited to 'frontends/verific/verific.cc')
-rw-r--r--frontends/verific/verific.cc92
1 files changed, 61 insertions, 31 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 92c7c9e2d..09c379f19 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -719,13 +719,13 @@ struct VerificImporter
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{
- if (inst->Type() == PRIM_SVA_ASSERT)
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
asserts.push_back(inst);
- if (inst->Type() == PRIM_SVA_ASSUME)
+ if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
assumes.push_back(inst);
- if (inst->Type() == PRIM_SVA_COVER)
+ if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
covers.push_back(inst);
}
@@ -1027,24 +1027,6 @@ struct VerificImporter
if (verbose)
log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
- if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) {
- Net *in = inst->GetInput();
- module->addAssert(NEW_ID, net_map_at(in), State::S1);
- continue;
- }
-
- if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
- Net *in = inst->GetInput();
- module->addAssume(NEW_ID, net_map_at(in), State::S1);
- continue;
- }
-
- if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER) {
- Net *in = inst->GetInput();
- module->addCover(NEW_ID, net_map_at(in), State::S1);
- continue;
- }
-
if (inst->Type() == PRIM_PWR) {
module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
continue;
@@ -1131,13 +1113,13 @@ struct VerificImporter
continue;
}
- if (inst->Type() == PRIM_SVA_ASSERT)
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
sva_asserts.insert(inst);
- if (inst->Type() == PRIM_SVA_ASSUME)
+ if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
sva_assumes.insert(inst);
- if (inst->Type() == PRIM_SVA_COVER)
+ if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
sva_covers.insert(inst);
if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
@@ -1168,6 +1150,28 @@ struct VerificImporter
continue;
}
+ if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
+ {
+ VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
+
+ SigSpec sig_d = net_map_at(inst->GetInput1());
+ SigSpec sig_o = net_map_at(inst->GetOutput());
+ SigSpec sig_q = module->addWire(NEW_ID);
+
+ if (verbose) {
+ log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+ log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+ log(" XNOR with A=%s, B=%s, Y=%s.\n",
+ log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+ }
+
+ module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+ module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+
+ if (!mode_keep)
+ continue;
+ }
+
if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
{
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@@ -1336,7 +1340,8 @@ struct VerificSvaPP
if (inst == nullptr)
return default_net;
- if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) {
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
+ inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
Net *new_net = rewrite(get_ast_input(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput());
@@ -1568,9 +1573,32 @@ struct VerificSvaImporter
module = importer->module;
netlist = root->Owner();
+ RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+
// parse SVA property clock event
Instance *at_node = get_ast_input(root);
+
+ // asynchronous immediate assertion/assumption/cover
+ if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
+ root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
+ {
+ SigSpec sig_a = importer->net_map_at(root->GetInput());
+ RTLIL::Cell *c = nullptr;
+
+ if (eventually) {
+ if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
+ if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
+ } else {
+ if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
+ if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
+ if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
+ }
+
+ importer->import_attributes(c->attributes, root);
+ return;
+ }
+
log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
@@ -1608,16 +1636,18 @@ struct VerificSvaImporter
// generate assert/assume/cover cell
- RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
+ RTLIL::Cell *c = nullptr;
if (eventually) {
- if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en);
- if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
} else {
- if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en);
- if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en);
- if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
+ if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
}
+
+ importer->import_attributes(c->attributes, root);
}
};
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-02 11:54:09 +0000