aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-01-31 19:06:51 +0100
committerClifford Wolf <clifford@clifford.at>2018-01-31 19:06:51 +0100
commit9af40faa0b60e2c0717f36888c1e19183e40a88c (patch)
tree5ce2d35b978b0817d271ef6e80eb9ffb0f4c05f4 /frontends/verific
parente97f10b14249a412d3a97d899f6e2a8685fbcdcf (diff)
downloadyosys-9af40faa0b60e2c0717f36888c1e19183e40a88c.tar.gz
yosys-9af40faa0b60e2c0717f36888c1e19183e40a88c.tar.bz2
yosys-9af40faa0b60e2c0717f36888c1e19183e40a88c.zip
Add Verific attribute handling for assert/assume/cover/live/fair cells
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific')
-rw-r--r--frontends/verific/verific.cc26
1 files changed, 16 insertions, 10 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 374411a28..fa1640050 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1562,16 +1562,18 @@ struct VerificSvaImporter
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) module->addLive(root_name, sig_a, State::S1);
- if (mode_assume) module->addFair(root_name, sig_a, State::S1);
+ 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) module->addAssert(root_name, sig_a, State::S1);
- if (mode_assume) module->addAssume(root_name, sig_a, State::S1);
- if (mode_cover) module->addCover(root_name, sig_a, State::S1);
+ 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;
}
@@ -1612,14 +1614,18 @@ struct VerificSvaImporter
// generate assert/assume/cover cell
+ 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);
}
};