diff options
author | Clifford Wolf <clifford@clifford.at> | 2019-11-22 15:52:21 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2019-11-22 15:52:21 +0100 |
commit | 6af0d03faede4a8d87292a76ae70dd1362dfcbb3 (patch) | |
tree | 32f8e72013cf4e6be4e1fb728f7670ebde320d1e /frontends/verific | |
parent | 72d2ef6fd071a8b2b9e1a77ddab3a9d632aa0f3d (diff) | |
download | yosys-6af0d03faede4a8d87292a76ae70dd1362dfcbb3.tar.gz yosys-6af0d03faede4a8d87292a76ae70dd1362dfcbb3.tar.bz2 yosys-6af0d03faede4a8d87292a76ae70dd1362dfcbb3.zip |
Add Verific SVA support for "always" properties
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific')
-rw-r--r-- | frontends/verific/verificsva.cc | 20 |
1 files 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); |