From 3efce9dea99d8b18e6e4694160b5348373afc175 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 12 Oct 2017 11:59:11 +0200 Subject: Add Verific fairness/liveness support --- frontends/verific/verific.cc | 43 ++++++++++++++++++++++++++++++++----------- 1 file changed, 32 insertions(+), 11 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 1efba338b..e77931528 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1500,6 +1500,7 @@ struct VerificSvaImporter bool mode_assert = false; bool mode_assume = false; bool mode_cover = false; + bool eventually = false; Instance *net_to_ast_driver(Net *n) { @@ -1673,15 +1674,30 @@ struct VerificSvaImporter // parse disable_iff expression Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1(); - Instance *sequence_node = net_to_ast_driver(sequence_net); - if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { - disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); - } else - if (sequence_node && sequence_node->Type() == PRIM_ABORT) { - disable_iff = importer->net_map_at(sequence_node->GetInput2()); - sequence_net = sequence_node->GetInput1(); + while (1) + { + Instance *sequence_node = net_to_ast_driver(sequence_net); + + if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { + eventually = true; + sequence_net = sequence_node->GetInput(); + continue; + } + + if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { + disable_iff = importer->net_map_at(sequence_node->GetInput1()); + sequence_net = sequence_node->GetInput2(); + continue; + } + + if (sequence_node && sequence_node->Type() == PRIM_ABORT) { + disable_iff = importer->net_map_at(sequence_node->GetInput2()); + sequence_net = sequence_node->GetInput1(); + continue; + } + + break; } // parse SVA sequence into trigger signal @@ -1694,9 +1710,14 @@ struct VerificSvaImporter RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); - 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 (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); + } 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); + } } }; -- cgit v1.2.3 From e558b3284b346b76ac2c06a0f6d61c9d53cba70c Mon Sep 17 00:00:00 2001 From: Kaj Tuomi Date: Tue, 17 Oct 2017 09:58:01 +0300 Subject: Fix input vector for reduce cells. Infinite loop fixed. --- passes/opt/opt_reduce.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc index eb9d02ad5..8126f3c0d 100644 --- a/passes/opt/opt_reduce.cc +++ b/passes/opt/opt_reduce.cc @@ -44,6 +44,7 @@ struct OptReduceWorker cells.erase(cell); RTLIL::SigSpec sig_a = assign_map(cell->getPort("\\A")); + sig_a.sort_and_unify(); pool new_sig_a_bits; for (auto &bit : sig_a.to_sigbit_set()) @@ -86,6 +87,7 @@ struct OptReduceWorker } RTLIL::SigSpec new_sig_a(new_sig_a_bits); + new_sig_a.sort_and_unify(); if (new_sig_a != sig_a || sig_a.size() != cell->getPort("\\A").size()) { log(" New input vector for %s cell %s: %s\n", cell->type.c_str(), cell->name.c_str(), log_signal(new_sig_a)); -- cgit v1.2.3