diff options
Diffstat (limited to 'frontends/verific/verificsva.cc')
-rw-r--r-- | frontends/verific/verificsva.cc | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index db81d0066..8eee02661 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1179,10 +1179,26 @@ struct VerificSvaImporter return node; } - if (inst->Type() == PRIM_SVA_INTERSECT) + if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN) { SvaFsm intersect_fsm(clocking); - intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.startNode, inst->GetInput1()), intersect_fsm.acceptNode); + + if (inst->Type() == PRIM_SVA_INTERSECT) + { + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.startNode, inst->GetInput1()), intersect_fsm.acceptNode); + } + else + { + int n = intersect_fsm.createNode(); + intersect_fsm.createLink(intersect_fsm.startNode, n); + intersect_fsm.createEdge(n, n); + + n = parse_sequence(intersect_fsm, n, inst->GetInput1()); + + intersect_fsm.createLink(n, intersect_fsm.acceptNode); + intersect_fsm.createEdge(n, n); + } + intersect_fsm.in_cond_mode = true; intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.startNode, inst->GetInput2()), intersect_fsm.condNode); intersect_fsm.in_cond_mode = false; |