mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
Remove all PSL support code from verific.cc
This commit is contained in:
Clifford Wolf
parent
309f8fe74f
commit
0a31a0b3ae
1 changed files with 17 additions and 179 deletions
|
|
@ -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<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),
|
||||
|
|
@ -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<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)
|
||||
|
|
@ -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 (!mode_keep && verific_sva_prims.count(inst->Type())) {
|
||||
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 (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} <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");
|
||||
|
|
@ -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<Netlist*> nl_todo, nl_done;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue