verific: Handle non-seq properties with VerificClocking conditions

This commit is contained in:
Jannis Harder 2023-04-21 17:19:42 +02:00
parent ec47bf1745
commit 3cbca5064c
1 changed files with 11 additions and 6 deletions

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 ||