diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-01 19:37:36 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-01 19:37:36 +0100 |
| commit | 4e5f1f59d66b96c5e0592e4f9810cca5d55c6894 (patch) | |
| tree | bd6fd3555097d89d0bb3c3760e3c330187d9ab91 /frontends/verific/verificsva.cc | |
| parent | 90ae42607850a51da55fd5c6fba20ebb02ef6226 (diff) | |
| download | yosys-4e5f1f59d66b96c5e0592e4f9810cca5d55c6894.tar.gz yosys-4e5f1f59d66b96c5e0592e4f9810cca5d55c6894.tar.bz2 yosys-4e5f1f59d66b96c5e0592e4f9810cca5d55c6894.zip | |
Fix in Verific SVA importer handling of until_with
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index e6430e9c5..70c28e387 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -974,11 +974,6 @@ struct VerificSvaImporter SvaFsm until_fsm(module, clock, clockpol, disable_iff); node = parse_sequence(&until_fsm, until_fsm.startNode, until_net); - if (until_with) { - int next_node = until_fsm.createNode(); - until_fsm.createEdge(node, next_node); - node = next_node; - } until_fsm.createLink(node, until_fsm.acceptNode); SigBit until_match = until_fsm.getAccept(); @@ -993,9 +988,12 @@ struct VerificSvaImporter antecedent_match_q->attributes["\\init"] = Const(0, 1); antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q); - antecedent_match = module->And(NEW_ID, antecedent_match, not_until_match); + SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match); + + module->addDff(NEW_ID, clock, antecedent_match_filtered, antecedent_match_q, clockpol); - module->addDff(NEW_ID, clock, antecedent_match, antecedent_match_q, clockpol); + if (!until_with) + antecedent_match = antecedent_match_filtered; } SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); |