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

Fix handling of SVA "until seq.triggered" properties 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-02 18:17:10 +01:00
parent ab791e61b3
commit cabc3c59e0
1 changed files with 25 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
frontends/verific/verificsva.cc
View File

@ -56,7 +56,10 @@
// not seq
// seq |=> seq
// seq |=> not seq
// seq |=> seq until expr
// seq |=> seq until seq.triggered
// seq |=> not seq until expr
// seq |=> not seq until seq.triggered
//
// Currently supported sequence operators:
// ##[N:M]
@ -959,20 +962,28 @@ struct VerificSvaImporter
antecedent_fsm.dump();
}
bool consequent_not = false;
Instance *consequent_inst = net_to_ast_driver(consequent_net);
if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
consequent_not = true;
consequent_net = consequent_inst->GetInput();
}
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))
{
bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
consequent_net = consequent_inst->GetInput1();
Net *until_net = consequent_inst->GetInput2();
Instance *until_inst = net_to_ast_driver(until_net);
consequent_net = consequent_inst->GetInput1();
consequent_inst = net_to_ast_driver(consequent_net);
if (until_inst != nullptr) {
if (until_inst->Type() != PRIM_SVA_TRIGGERED) {
if (!importer->mode_keep)
log_error("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
log_warning("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
return;
}
until_net = until_inst->GetInput();
}
SvaFsm until_fsm(module, clock, clockpol, disable_iff);
node = parse_sequence(&until_fsm, until_fsm.startNode, until_net);
@ -998,6 +1009,13 @@ struct VerificSvaImporter
antecedent_match = antecedent_match_filtered;
}
bool consequent_not = false;
if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
consequent_not = true;
consequent_net = consequent_inst->GetInput();
consequent_inst = net_to_ast_driver(consequent_net);
}
SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match);
node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net);
consequent_fsm.createLink(node, consequent_fsm.acceptNode);