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

Fix handling of zero-length SVA consecutive repetition 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-05-05 13:58:01 +02:00
parent e3575a86c5
commit 3e67497ec2
1 changed files with 47 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

74
frontends/verific/verificsva.cc
View File

@ -50,11 +50,11 @@
// sequence ##[+] sequence // sequence ##[+] sequence
// sequence ##[N:M] sequence // sequence ##[N:M] sequence
// sequence ##[N:$] sequence // sequence ##[N:$] sequence
// sequence [*] // expression [*]
// sequence [+] // expression [+]
// sequence [*N] // expression [*N]
// sequence [*N:M] // expression [*N:M]
// sequence [*N:$] // expression [*N:$]
// sequence or sequence // sequence or sequence
// sequence and sequence // sequence and sequence
// expression throughout sequence // expression throughout sequence
@ -1138,7 +1138,7 @@ struct VerificSvaImporter
log_abort(); log_abort();
} }
int parse_sequence(SvaFsm &fsm, int start_node, Net *net) int parse_sequence(SvaFsm &fsm, int start_node, Net *net, int past_start_node = -1)
{ {
if (check_expression(net)) { if (check_expression(net)) {
int node = fsm.createNode(); int node = fsm.createNode();
@ -1183,15 +1183,28 @@ struct VerificSvaImporter
bool sva_inf = !strcmp(sva_high_s, "$"); bool sva_inf = !strcmp(sva_high_s, "$");
int node = parse_sequence(fsm, start_node, inst->GetInput1()); int node = parse_sequence(fsm, start_node, inst->GetInput1());
int past_node = -1;
Net *next_net = inst->GetInput2();
Instance *next_inst = net_to_ast_driver(next_net);
if (next_inst != nullptr && next_inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT && sva_low > 0) {
past_node = fsm.createNode();
log_dump(past_node);
}
for (int i = 0; i < sva_low; i++) { for (int i = 0; i < sva_low; i++) {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node); fsm.createEdge(node, next_node);
if (past_node >= 0 && i == sva_low-1)
fsm.createLink(node, past_node);
node = next_node; node = next_node;
} }
if (sva_inf) if (sva_inf)
{ {
if (past_node >= 0)
fsm.createLink(node, past_node);
fsm.createEdge(node, node); fsm.createEdge(node, node);
} }
else else
@ -1201,11 +1214,13 @@ struct VerificSvaImporter
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node); fsm.createEdge(node, next_node);
fsm.createLink(node, next_node); fsm.createLink(node, next_node);
if (past_node >= 0)
fsm.createLink(node, past_node);
node = next_node; node = next_node;
} }
} }
node = parse_sequence(fsm, node, inst->GetInput2()); node = parse_sequence(fsm, node, inst->GetInput2(), past_node);
return node; return node;
} }
@ -1220,46 +1235,51 @@ struct VerificSvaImporter
bool sva_inf = !strcmp(sva_high_s, "$"); bool sva_inf = !strcmp(sva_high_s, "$");
Net *body_net = inst->GetInput(); Net *body_net = inst->GetInput();
int node = fsm.createNode(start_node);
for (int i = 0; i < sva_low; i++) bool bypass = false;
if (sva_low == 0) {
if (past_start_node == -1)
parser_error("Possibly zero-length consecutive repeat must follow a delay of at least one cycle", inst);
bypass = true;
sva_low++;
}
int node = fsm.createNode(start_node);
int prev_node = node;
node = parse_sequence(fsm, node, body_net);
for (int i = 1; i < sva_low; i++)
{ {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node);
if (i == 0) prev_node = node;
fsm.createLink(node, next_node);
else
fsm.createEdge(node, next_node);
node = parse_sequence(fsm, next_node, body_net); node = parse_sequence(fsm, next_node, body_net);
} }
if (sva_inf) if (sva_inf)
{ {
int next_node = fsm.createNode(); log_assert(prev_node >= 0);
fsm.createEdge(node, next_node); fsm.createEdge(node, prev_node);
next_node = parse_sequence(fsm, next_node, body_net);
fsm.createLink(next_node, node);
} }
else else
{ {
for (int i = sva_low; i < sva_high; i++) for (int i = sva_low; i < sva_high; i++)
{ {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node);
if (i == 0) prev_node = node;
fsm.createLink(node, next_node); node = parse_sequence(fsm, next_node, body_net);
else
fsm.createEdge(node, next_node);
next_node = parse_sequence(fsm, next_node, body_net); fsm.createLink(prev_node, node);
fsm.createLink(node, next_node);
node = next_node;
} }
} }
if (bypass)
fsm.createLink(past_start_node, node);
return node; return node;
} }