3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 01:54:10 +00:00

Add support for SVA throughout via Verific

This commit is contained in:
Clifford Wolf 2018-02-21 13:09:47 +01:00
parent 17583b6a21
commit 6d12c83d36
2 changed files with 7 additions and 3 deletions

View file

@ -433,10 +433,14 @@ struct VerificSvaImporter
return; return;
} }
if (inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL || if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH) inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
{ {
bool flag_with = inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH; bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
if (get_ast_input1(inst) != nullptr)
log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n");
SigBit expr = importer->net_map_at(inst->GetInput1()); SigBit expr = importer->net_map_at(inst->GetInput1());
if (flag_with) if (flag_with)

View file

@ -5,7 +5,7 @@ module top (
default clocking @(posedge clk); endclocking default clocking @(posedge clk); endclocking
assert property ( assert property (
a |=> b until_with (c ##1 d) a |=> b throughout (c ##1 d)
); );
`ifndef FAIL `ifndef FAIL