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

Fix handling of unclocked immediate assertions in Verific front-end 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-26 13:04:10 +02:00
parent 3f00702475
commit 315d5e32bf
3 changed files with 42 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
frontends/verific/verific.cc
View File

@ -1297,7 +1297,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
// ==================================================================
VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
{
module = importer->module;
@ -1320,6 +1320,11 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
body_net = body_inst->GetInput2();
}
}
else
{
if (sva_at_only)
return;
}
if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
{

2
frontends/verific/verific.h
View File

@ -42,7 +42,7 @@ struct VerificClocking {
bool posedge = true;
VerificClocking() { }
VerificClocking(VerificImporter *importer, Verific::Net *net);
VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);

50
frontends/verific/verificsva.cc
View File

@ -1543,20 +1543,33 @@ struct VerificSvaImporter
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
clocking = VerificClocking(importer, root->GetInput());
if (clocking.body_net == nullptr)
parser_error(stringf("Failed to parse SVA clocking"), root);
// parse SVA sequence into trigger signal
Net *net = clocking.body_net;
SigBit accept_bit = State::S0, reject_bit = State::S0;
clocking = VerificClocking(importer, root->GetInput(), true);
SigBit accept_bit = State::S0, reject_bit = State::S0;
if (mode_assert || mode_assume) {
parse_property(net, nullptr, &reject_bit);
} else {
parse_property(net, &accept_bit, nullptr);
if (clocking.body_net == nullptr)
{
if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr || clocking.cond_net != nullptr)
parser_error(stringf("Failed to parse SVA clocking"), root);
if (mode_assert || mode_assume) {
log_ping();
reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
} else {
log_ping();
accept_bit = parse_expression(root->GetInput());
}
}
else
{
if (mode_assert || mode_assume) {
log_ping();
parse_property(clocking.body_net, nullptr, &reject_bit);
} else {
log_ping();
parse_property(clocking.body_net, &accept_bit, nullptr);
}
}
if (mode_trigger)
@ -1570,10 +1583,17 @@ struct VerificSvaImporter
// add final FF stage
SigBit sig_a_q = module->addWire(NEW_ID);
SigBit sig_en_q = module->addWire(NEW_ID);
clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
SigBit sig_a_q, sig_en_q;
if (clocking.body_net == nullptr) {
sig_a_q = sig_a;
sig_en_q = sig_en;
} else {
sig_a_q = module->addWire(NEW_ID);
sig_en_q = module->addWire(NEW_ID);
clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
}
// generate assert/assume/cover cell