riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add Verific support for SVA nexttime properties 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-11-22 16:11:56 +01:00
parent e93e4a7a2c
commit db323685a4
1 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
frontends/verific/verificsva.cc
View File

@ -36,6 +36,8 @@
// basic_property: // basic_property:
// sequence // sequence
// not basic_property // not basic_property
// nexttime basic_property
// nexttime[N] basic_property
// sequence #-# basic_property // sequence #-# basic_property
// sequence #=# basic_property // sequence #=# basic_property
// basic_property or basic_property (cover only) // basic_property or basic_property (cover only)
@ -1264,6 +1266,26 @@ struct VerificSvaImporter
return node; return node;
} }
if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
{
const char *sva_low_s = inst->GetAttValue("sva:low");
const char *sva_high_s = inst->GetAttValue("sva:high");
int sva_low = atoi(sva_low_s);
int sva_high = atoi(sva_high_s);
log_assert(sva_low == sva_high);
int node = start_node;
for (int i = 0; i < sva_low; i++) {
int next_node = fsm.createNode();
fsm.createEdge(node, next_node);
node = next_node;
}
return parse_sequence(fsm, node, inst->GetInput());
}
if (inst->Type() == PRIM_SVA_SEQ_CONCAT) if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{ {
const char *sva_low_s = inst->GetAttValue("sva:low"); const char *sva_low_s = inst->GetAttValue("sva:low");