From 0a31a0b3ae570007196c4b4dd6c16ba7de7f3ba9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 20 Oct 2017 13:14:04 +0200 Subject: [PATCH] Remove all PSL support code from verific.cc --- frontends/verific/verific.cc | 196 +++-------------------------------- 1 file changed, 17 insertions(+), 179 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 77594b8cf..54210f98a 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -104,9 +104,9 @@ void svapp_assume(VerificImporter *importer, Instance *inst); void svapp_cover(VerificImporter *importer, Instance *inst); struct VerificClockEdge { - Net *clock_net; - SigBit clock_sig; - bool posedge; + Net *clock_net = nullptr; + SigBit clock_sig = State::Sx; + bool posedge = false; VerificClockEdge(VerificImporter *importer, Instance *inst); }; @@ -121,7 +121,6 @@ struct VerificImporter bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; pool verific_sva_prims; - pool verific_psl_prims; VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) : mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), @@ -152,29 +151,6 @@ struct VerificImporter for (int p : sva_prims) verific_sva_prims.insert(p); - - // Copy&paste from Verific 3.16_484_32_170630 Netlist.h - vector psl_prims { - OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME, - PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE, - PRIM_PSL_COVER, PRIM_ENDPOINT, PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG, - PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV, - PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W, - PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY, - PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE, - PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A, - PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT, - PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG, - PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL, - PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN, - PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT, - PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT, - PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP, - PRIM_NONCONS_REP, PRIM_GOTO_REP - }; - - for (int p : psl_prims) - verific_psl_prims.insert(p); } RTLIL::SigBit net_map_at(Net *net) @@ -1126,20 +1102,20 @@ struct VerificImporter if (!mode_gates) { if (import_netlist_instance_cells(inst, inst_name)) continue; - if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) + if (inst->IsOperator() && !verific_sva_prims.count(inst->Type())) log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); } else { if (import_netlist_instance_gates(inst, inst_name)) continue; } - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_PSL_ASSERT) + if (inst->Type() == PRIM_SVA_ASSERT) sva_asserts.insert(inst); - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_PSL_ASSUME) + if (inst->Type() == PRIM_SVA_ASSUME) sva_assumes.insert(inst); - if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_PSL_COVER) + if (inst->Type() == PRIM_SVA_COVER) sva_covers.insert(inst); if (inst->Type() == PRIM_SVA_PAST && !mode_nosva) @@ -1159,38 +1135,9 @@ struct VerificImporter continue; } - if (inst->Type() == OPER_PSLPREV && !mode_nosva) - { - Net *clock = inst->GetClock(); - - if (!clock->IsConstant()) - { - VerificClockEdge clock_edge(this, clock->Driver()); - - SigSpec sig_d, sig_q; - - for (int i = 0; i < int(inst->InputSize()); i++) { - sig_d.append(net_map_at(inst->GetInputBit(i))); - sig_q.append(net_map_at(inst->GetOutputBit(i))); - } - - if (verbose) - log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); - - RTLIL::Cell *ff = module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); - - if (inst->InputSize() == 1) - past_ffs.insert(ff); - - if (!mode_keep) - continue; - } - } - - if (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) { + if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (verbose) - log(" skipping SVA/PSL cell in non k-mode\n"); + log(" skipping SVA cell in non k-mode\n"); continue; } @@ -1202,7 +1149,7 @@ struct VerificImporter if (!mode_keep) log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); - if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) + if (!verific_sva_prims.count(inst->Type())) log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); } @@ -1277,36 +1224,6 @@ struct VerificImporter } }; -Net *verific_follow_inv(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; - - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != PRIM_INV) - return nullptr; - - return i->GetInput(); -} - -Net *verific_follow_pslprev(Net *w) -{ - if (w == nullptr || w->IsMultipleDriven()) - return nullptr; - - Instance *i = w->Driver(); - if (i == nullptr || i->Type() != OPER_PSLPREV || i->InputSize() != 1) - return nullptr; - - return i->GetInputBit(0); -} - -Net *verific_follow_inv_pslprev(Net *w) -{ - w = verific_follow_inv(w); - return verific_follow_pslprev(w); -} - VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) { log_assert(importer != nullptr); @@ -1327,43 +1244,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) clock_sig = importer->net_map_at(clock_net); return; } - - // VHDL-flavored PSL clock - if (inst->Type() == PRIM_AND) - { - Net *w1 = inst->GetInput1(); - Net *w2 = inst->GetInput2(); - - clock_net = verific_follow_inv_pslprev(w1); - if (clock_net == w2) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; - } - - clock_net = verific_follow_inv_pslprev(w2); - if (clock_net == w1) { - clock_sig = importer->net_map_at(clock_net); - posedge = true; - return; - } - - clock_net = verific_follow_pslprev(w1); - if (clock_net == verific_follow_inv(w2)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } - - clock_net = verific_follow_pslprev(w2); - if (clock_net == verific_follow_inv(w1)) { - clock_sig = importer->net_map_at(clock_net); - posedge = false; - return; - } - - log_abort(); - } } // ================================================================== @@ -1393,8 +1273,7 @@ struct VerificSvaPP if (inst == nullptr) return nullptr; - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) + if (!importer->verific_sva_prims.count(inst->Type())) return nullptr; if (inst->Type() == PRIM_SVA_PAST) @@ -1515,8 +1394,7 @@ struct VerificSvaImporter if (inst == nullptr) return nullptr; - if (!importer->verific_sva_prims.count(inst->Type()) && - !importer->verific_psl_prims.count(inst->Type())) + if (!importer->verific_sva_prims.count(inst->Type())) return nullptr; if (inst->Type() == PRIM_SVA_PAST) @@ -1625,31 +1503,6 @@ struct VerificSvaImporter return; } - // PSL Primitives - - if (inst->Type() == PRIM_ALWAYS) - { - parse_sequence(seq, inst->GetInput()); - return; - } - - if (inst->Type() == PRIM_IMPL) - { - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - parse_sequence(seq, inst->GetInput2()); - return; - } - - if (inst->Type() == PRIM_SUFFIX_IMPL) - { - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - sequence_ff(seq); - parse_sequence(seq, inst->GetInput2()); - return; - } - // Handle unsupported primitives if (!importer->mode_keep) @@ -1665,15 +1518,15 @@ struct VerificSvaImporter // parse SVA property clock event Instance *at_node = get_ast_input(root); - log_assert(at_node && (at_node->Type() == PRIM_SVA_AT || at_node->Type() == PRIM_AT)); + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); - VerificClockEdge clock_edge(importer, at_node->Type() == PRIM_SVA_AT ? get_ast_input1(at_node) : at_node->GetInput2()->Driver()); + VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); clock = clock_edge.clock_sig; clock_posedge = clock_edge.posedge; // parse disable_iff expression - Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1(); + Net *sequence_net = at_node->GetInput2(); while (1) { @@ -1691,12 +1544,6 @@ struct VerificSvaImporter continue; } - if (sequence_node && sequence_node->Type() == PRIM_ABORT) { - disable_iff = importer->net_map_at(sequence_node->GetInput2()); - sequence_net = sequence_node->GetInput1(); - continue; - } - break; } @@ -1846,7 +1693,7 @@ struct VerificPass : public Pass { log("Load the specified Verilog/SystemVerilog files into Verific.\n"); log("\n"); log("\n"); - log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} ..\n"); + log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} ..\n"); log("\n"); log("Load the specified VHDL files into Verific.\n"); log("\n"); @@ -1900,8 +1747,7 @@ struct VerificPass : public Pass { log(" the checker logic inferred by it.\n"); log("\n"); log(" -nosva\n"); - log(" Ignore SVA properties, do not infer checker logic. (This also disables\n"); - log(" PSL properties in -vhdpsl mode.)\n"); + log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); log(" -nosvapp\n"); log(" Disable SVA properties pre-processing pass. This implies -nosva.\n"); @@ -2036,14 +1882,6 @@ struct VerificPass : public Pass { goto check_error; } - if (GetSize(args) > argidx && args[argidx] == "-vhdpsl") { - vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) - if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL)) - log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str()); - goto check_error; - } - if (GetSize(args) > argidx && args[argidx] == "-import") { std::set nl_todo, nl_done; -- 2.30.2