From 9af40faa0b60e2c0717f36888c1e19183e40a88c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 31 Jan 2018 19:06:51 +0100 Subject: [PATCH] Add Verific attribute handling for assert/assume/cover/live/fair cells Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 26 ++++++++++++++++---------- 1 file 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); } }; -- 2.30.2