diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-10-12 11:59:11 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-10-12 12:00:09 +0200 |
| commit | bc5cc4e103bf59711c339719d6aabbc3d4b655a4 (patch) | |
| tree | 6129905e0609d5c645a7992b9482401ab4003379 /frontends/verific | |
| parent | 2b03a73a460a2033f8944c7c85623cef11600024 (diff) | |
| download | yosys-bc5cc4e103bf59711c339719d6aabbc3d4b655a4.tar.gz yosys-bc5cc4e103bf59711c339719d6aabbc3d4b655a4.tar.bz2 yosys-bc5cc4e103bf59711c339719d6aabbc3d4b655a4.zip | |
Add Verific fairness/liveness support
Diffstat (limited to 'frontends/verific')
| -rw-r--r-- | frontends/verific/verific.cc | 43 |
1 files 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); + } } }; |