aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific/verificsva.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2019-11-22 15:52:21 +0100
committerClifford Wolf <clifford@clifford.at>2019-11-22 15:52:21 +0100
commit6af0d03faede4a8d87292a76ae70dd1362dfcbb3 (patch)
tree32f8e72013cf4e6be4e1fb728f7670ebde320d1e /frontends/verific/verificsva.cc
parent72d2ef6fd071a8b2b9e1a77ddab3a9d632aa0f3d (diff)
downloadyosys-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/verificsva.cc')
-rw-r--r--frontends/verific/verificsva.cc20
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);