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);
};
bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
pool<int> verific_sva_prims;
- pool<int> 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),
for (int p : sva_prims)
verific_sva_prims.insert(p);
-
- // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
- vector<int> 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)
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)
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;
}
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());
}
}
};
-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);
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();
- }
}
// ==================================================================
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)
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)
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)
// 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)
{
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;
}
log("Load the specified Verilog/SystemVerilog files into Verific.\n");
log("\n");
log("\n");
- log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} <vhdl-file>..\n");
+ log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
log("\n");
log("Load the specified VHDL files into Verific.\n");
log("\n");
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");
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<Netlist*> nl_todo, nl_done;
projects / yosys.git / commitdiff