mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Add Verific attribute handling for assert/assume/cover/live/fair cells

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-01-31 19:06:51 +01:00
parent e97f10b142
commit 9af40faa0b
1 changed files with 16 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

26
frontends/verific/verific.cc
View file

@ -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);
}
};