From 78f2cca2d92e4a88ea8192af86e89bf4fdfa9a49 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Mar 2018 14:41:27 +0100 Subject: [PATCH] Add SVA within support Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 20 ++++++++++++++++++-- 1 file 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; -- 2.30.2