diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-03-26 13:04:10 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-03-26 13:04:10 +0200 |
| commit | 315d5e32bfb63a2b4be2dc5e729125c420b164a4 (patch) | |
| tree | 5c9d7e1dc45022a300a6796f6aea2f0273351722 /frontends/verific/verificsva.cc | |
| parent | 3f0070247590458c5ed28c5a7abfc3b9d1ec138b (diff) | |
| download | yosys-315d5e32bfb63a2b4be2dc5e729125c420b164a4.tar.gz yosys-315d5e32bfb63a2b4be2dc5e729125c420b164a4.tar.bz2 yosys-315d5e32bfb63a2b4be2dc5e729125c420b164a4.zip | |
Fix handling of unclocked immediate assertions in Verific front-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 50 |
1 files changed, 35 insertions, 15 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index c9c341516..1a1000b19 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -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 |