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

Merge pull request #3736 from jix/conc_assertion_in_unclocked_proc_ctx

This commit is contained in:
N. Engelhardt 2023-05-08 16:15:13 +02:00 committed by GitHub
parent ec56e625f4 3cbca5064c
commit 0aeb6105eb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 33 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
frontends/verific/verific.cc
View File

@ -2011,6 +2011,28 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
Instance *inst = net->Driver();
// Detect condition expression in sva_at_only mode
if (sva_at_only)
do {
Instance *inst_mux = net->Driver();
if (inst_mux->Type() != PRIM_MUX)
break;
bool pwr1 = inst_mux->GetInput1()->IsPwr();
bool pwr2 = inst_mux->GetInput2()->IsPwr();
if (!pwr1 && !pwr2)
break;
Net *sva_net = pwr1 ? inst_mux->GetInput2() : inst_mux->GetInput1();
if (!verific_is_sva_net(importer, sva_net))
break;
inst = sva_net->Driver();
cond_net = inst_mux->GetControl();
cond_pol = pwr1;
} while (0);
if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
{
net = inst->GetInput1();

17
frontends/verific/verificsva.cc
View File

@ -1598,12 +1598,17 @@ struct VerificSvaImporter
if (inst == nullptr)
{
log_assert(trig == State::S1);
if (accept_p != nullptr)
*accept_p = importer->net_map_at(net);
if (reject_p != nullptr)
*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
if (trig != State::S1) {
if (accept_p != nullptr)
*accept_p = module->And(NEW_ID, trig, importer->net_map_at(net));
if (reject_p != nullptr)
*reject_p = module->And(NEW_ID, trig, module->Not(NEW_ID, importer->net_map_at(net)));
} else {
if (accept_p != nullptr)
*accept_p = importer->net_map_at(net);
if (reject_p != nullptr)
*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
}
}
else
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||