From 6af0d03faede4a8d87292a76ae70dd1362dfcbb3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 22 Nov 2019 15:52:21 +0100 Subject: [PATCH] Add Verific SVA support for "always" properties Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 909e9b4f1..225fd3e4a 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1590,15 +1590,25 @@ struct VerificSvaImporter Instance *consequent_inst = net_to_ast_driver(consequent_net); if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL || - consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH)) + consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH || + consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)) { bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH; - Net *until_net = consequent_inst->GetInput2(); - consequent_net = consequent_inst->GetInput1(); - consequent_inst = net_to_ast_driver(consequent_net); + Net *until_net = nullptr; + if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS) + { + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + else + { + until_net = consequent_inst->GetInput2(); + consequent_net = consequent_inst->GetInput1(); + consequent_inst = net_to_ast_driver(consequent_net); + } - SigBit until_sig = parse_expression(until_net); + SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0; SigBit not_until_sig = module->Not(NEW_ID, until_sig); antecedent_fsm.createEdge(node, node, not_until_sig);