From a4bbfd2d15db25ba9b2599afa0badd8abe1273ba Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 7 Mar 2018 20:06:02 +0100 Subject: [PATCH] Fix Verific handling of "assert property (..);" in always block Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 37 +++++++++++++++++++++++++++++---- frontends/verific/verific.h | 10 +++++---- frontends/verific/verificsva.cc | 27 ++++++++++++++++++------ 3 files changed, 60 insertions(+), 14 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 4aeedf767..0db57d598 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1116,6 +1116,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == OPER_SVA_STABLE) { VerificClocking clocking(this, inst->GetInput2Bit(0)); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); log_assert(inst->Input1Size() == inst->OutputSize()); @@ -1144,6 +1146,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == PRIM_SVA_STABLE) { VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); SigSpec sig_d = net_map_at(inst->GetInput1()); SigSpec sig_o = net_map_at(inst->GetOutput()); @@ -1166,6 +1170,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == PRIM_SVA_PAST) { VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_q = net_map_at(inst->GetOutput()); @@ -1183,6 +1189,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL)) { VerificClocking clocking(this, inst->GetInput2()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_o = net_map_at(inst->GetOutput()); @@ -1264,16 +1272,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (!mode_nosva) { for (auto inst : sva_asserts) - import_sva_assert(this, inst); + verific_import_sva_assert(this, inst); for (auto inst : sva_assumes) - import_sva_assume(this, inst); + verific_import_sva_assume(this, inst); for (auto inst : sva_covers) - import_sva_cover(this, inst); + verific_import_sva_cover(this, inst); for (auto inst : sva_triggers) - import_sva_trigger(this, inst); + verific_import_sva_trigger(this, inst); merge_past_ffs(past_ffs); } @@ -1356,6 +1364,27 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net) inst = net->Driver();; } while (0); + // Detect condition expression + do { + if (body_net == nullptr) + break; + + Instance *inst_mux = body_net->Driver(); + + if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX) + break; + + if (!inst_mux->GetInput1()->IsPwr()) + break; + + Net *sva_net = inst_mux->GetInput2(); + if (!verific_is_sva_net(importer, sva_net)) + break; + + body_net = sva_net; + cond_net = inst_mux->GetControl(); + } while (0); + clock_net = net; clock_sig = importer->net_map_at(clock_net); } diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 1f33d4ccb..877d79057 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -35,6 +35,7 @@ struct VerificClocking { Verific::Net *enable_net = nullptr; Verific::Net *disable_net = nullptr; Verific::Net *body_net = nullptr; + Verific::Net *cond_net = nullptr; SigBit clock_sig = State::Sx; SigBit enable_sig = State::S1; SigBit disable_sig = State::S0; @@ -88,10 +89,11 @@ struct VerificImporter void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set &nl_todo); }; -void import_sva_assert(VerificImporter *importer, Verific::Instance *inst); -void import_sva_assume(VerificImporter *importer, Verific::Instance *inst); -void import_sva_cover(VerificImporter *importer, Verific::Instance *inst); -void import_sva_trigger(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_assume(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst); +void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst); +bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net); YOSYS_NAMESPACE_END diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index da320019b..1472bb7b4 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1017,6 +1017,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_AT) { VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); if (!clocking.property_matches_sequence(new_clocking)) parser_error("Mixed clocking is currently not supported", inst); return parse_sequence(fsm, start_node, new_clocking.body_net); @@ -1241,8 +1242,15 @@ struct VerificSvaImporter { Instance *inst = net_to_ast_driver(net); + SigBit trig = State::S1; + + if (clocking.cond_net != nullptr) + trig = importer->net_map_at(clocking.cond_net); + if (inst == nullptr) { + log_assert(trig == State::S1); + if (accept_p != nullptr) *accept_p = importer->net_map_at(net); if (reject_p != nullptr) @@ -1256,7 +1264,7 @@ struct VerificSvaImporter Net *consequent_net = inst->GetInput2(); int node; - SvaFsm antecedent_fsm(clocking); + SvaFsm antecedent_fsm(clocking, trig); node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -1324,7 +1332,7 @@ struct VerificSvaImporter inst = net_to_ast_driver(net); } - SvaFsm fsm(clocking); + SvaFsm fsm(clocking, trig); int node = parse_sequence(fsm, fsm.createStartNode(), net); fsm.createLink(node, fsm.acceptNode); @@ -1399,7 +1407,7 @@ struct VerificSvaImporter } }; -void import_sva_assert(VerificImporter *importer, Instance *inst) +void verific_import_sva_assert(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; worker.importer = importer; @@ -1408,7 +1416,7 @@ void import_sva_assert(VerificImporter *importer, Instance *inst) worker.import(); } -void import_sva_assume(VerificImporter *importer, Instance *inst) +void verific_import_sva_assume(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; worker.importer = importer; @@ -1417,7 +1425,7 @@ void import_sva_assume(VerificImporter *importer, Instance *inst) worker.import(); } -void import_sva_cover(VerificImporter *importer, Instance *inst) +void verific_import_sva_cover(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; worker.importer = importer; @@ -1426,7 +1434,7 @@ void import_sva_cover(VerificImporter *importer, Instance *inst) worker.import(); } -void import_sva_trigger(VerificImporter *importer, Instance *inst) +void verific_import_sva_trigger(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; worker.importer = importer; @@ -1435,4 +1443,11 @@ void import_sva_trigger(VerificImporter *importer, Instance *inst) worker.import(); } +bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net) +{ + VerificSvaImporter worker; + worker.importer = importer; + return worker.net_to_ast_driver(net) != nullptr; +} + YOSYS_NAMESPACE_END