From 03b49654b1573dfea94f589d24415bf256150165 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Mar 2018 15:39:46 +0100 Subject: [PATCH] Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 61 ++++++++++++++++++++++----------- 1 file changed, 41 insertions(+), 20 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 41ce45048..f89595714 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -211,6 +211,13 @@ struct SvaFsm return idx; } + int createStartNode() + { + int node = createNode(); + createLink(startNode, node); + return node; + } + void createEdge(int from_node, int to_node, SigBit ctrl = State::S1) { log_assert(!materialized); @@ -1061,7 +1068,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_FIRST_MATCH) { SvaFsm match_fsm(clocking); - match_fsm.createLink(parse_sequence(match_fsm, match_fsm.startNode, inst->GetInput()), match_fsm.acceptNode); + match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode); int node = fsm.createNode(); match_fsm.getDFsm(fsm, start_node, node); @@ -1111,7 +1118,7 @@ struct VerificSvaImporter return node; } - if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) + if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT) { const char *sva_low_s = inst->GetAttValue("sva:low"); const char *sva_high_s = inst->GetAttValue("sva:high"); @@ -1121,17 +1128,20 @@ struct VerificSvaImporter bool sva_inf = !strcmp(sva_high_s, "$"); Net *body_net = inst->GetInput(); - Instance *body_inst = net_to_ast_driver(body_net); - - if (body_inst != nullptr) - parser_error(body_inst); - - int node = parse_sequence(fsm, start_node, body_net); + int node = start_node; - for (int i = 1; i < sva_low; i++) + for (int i = 0; i < sva_low; i++) { int next_node = fsm.createNode(); - fsm.createEdge(node, next_node); + + if (i == 0) + fsm.createLink(node, next_node); + else + fsm.createEdge(node, next_node); + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT) + fsm.createEdge(next_node, next_node); + node = parse_sequence(fsm, next_node, body_net); } @@ -1139,6 +1149,10 @@ struct VerificSvaImporter { int next_node = fsm.createNode(); fsm.createEdge(node, next_node); + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT) + fsm.createEdge(next_node, next_node); + next_node = parse_sequence(fsm, next_node, body_net); fsm.createLink(next_node, node); } @@ -1148,12 +1162,19 @@ struct VerificSvaImporter { int next_node = fsm.createNode(); fsm.createEdge(node, next_node); + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT) + fsm.createEdge(next_node, next_node); + next_node = parse_sequence(fsm, next_node, body_net); fsm.createLink(node, next_node); node = next_node; } } + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT) + fsm.createEdge(node, node); + return node; } @@ -1168,14 +1189,14 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_SEQ_AND) { SvaFsm fsm1(clocking); - fsm1.createLink(parse_sequence(fsm1, fsm1.startNode, inst->GetInput1()), fsm1.acceptNode); + fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode); SvaFsm fsm2(clocking); - fsm2.createLink(parse_sequence(fsm2, fsm2.startNode, inst->GetInput2()), fsm2.acceptNode); + fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode); SvaFsm combined_fsm(clocking); - fsm1.getDFsm(combined_fsm, combined_fsm.startNode, -1, combined_fsm.acceptNode); - fsm2.getDFsm(combined_fsm, combined_fsm.startNode, -1, combined_fsm.acceptNode); + fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); + fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); int node = fsm.createNode(); combined_fsm.getDFsm(fsm, start_node, -1, node); @@ -1201,12 +1222,12 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_INTERSECT) { - intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.startNode, inst->GetInput1()), intersect_fsm.acceptNode); + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode); } else { int n = intersect_fsm.createNode(); - intersect_fsm.createLink(intersect_fsm.startNode, n); + intersect_fsm.createLink(intersect_fsm.createStartNode(), n); intersect_fsm.createEdge(n, n); n = parse_sequence(intersect_fsm, n, inst->GetInput1()); @@ -1216,7 +1237,7 @@ struct VerificSvaImporter } intersect_fsm.in_cond_mode = true; - intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.startNode, inst->GetInput2()), intersect_fsm.condNode); + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode); intersect_fsm.in_cond_mode = false; int node = fsm.createNode(); @@ -1279,7 +1300,7 @@ struct VerificSvaImporter int node; SvaFsm antecedent_fsm(clocking); - node = parse_sequence(antecedent_fsm, antecedent_fsm.startNode, antecedent_net); + node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); antecedent_fsm.createEdge(node, next_node); @@ -1328,7 +1349,7 @@ struct VerificSvaImporter } SvaFsm consequent_fsm(clocking, antecedent_match); - node = parse_sequence(consequent_fsm, consequent_fsm.startNode, consequent_net); + node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not); @@ -1347,7 +1368,7 @@ struct VerificSvaImporter } SvaFsm fsm(clocking); - int node = parse_sequence(fsm, fsm.startNode, net); + int node = parse_sequence(fsm, fsm.createStartNode(), net); fsm.createLink(node, fsm.acceptNode); get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not); -- 2.30.2