Merge pull request #3039 from YosysHQ/claire/verific_aldff

Add support for $aldff flip-flops to verific importer
This commit is contained in:
Claire Xen 2021-10-11 10:01:56 +02:00 committed by GitHub
commit 2d3c79458d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 91 additions and 1 deletions

View File

@ -410,6 +410,32 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
return true;
}
if (inst->Type() == PRIM_DLATCHRS)
{
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else
module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true;
}
if (inst->Type() == PRIM_DFF)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetAsyncCond()->IsGnd())
clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else
clocking.addAldff(inst_name, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true;
}
// FIXME: PRIM_DLATCH
return false;
}
@ -520,6 +546,23 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
if (inst->Type() == PRIM_DFF)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetAsyncCond()->IsGnd())
cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else
cell = clocking.addAldff(inst_name, net_map_at(inst->GetAsyncCond()), net_map_at(inst->GetAsyncVal()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
// FIXME: PRIM_DLATCH
#define IN operatorInput(inst)
#define IN1 operatorInput1(inst)
#define IN2 operatorInput2(inst)
@ -792,6 +835,38 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true;
}
// FIXME: OPER_WIDE_DLATCHSR
if (inst->Type() == OPER_WIDE_DFF)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
RTLIL::SigSpec sig_d = IN;
RTLIL::SigSpec sig_q = OUT;
RTLIL::SigSpec sig_adata = IN1;
RTLIL::SigSpec sig_acond = IN2;
if (sig_acond.is_fully_const() && !sig_acond.as_bool()) {
cell = clocking.addDff(inst_name, sig_d, sig_q);
import_attributes(cell->attributes, inst);
} else {
int offset = 0, width = 0;
for (offset = 0; offset < GetSize(sig_acond); offset += width) {
for (width = 1; offset+width < GetSize(sig_acond); width++)
if (sig_acond[offset] != sig_acond[offset+width]) break;
cell = clocking.addAldff(inst_name, sig_acond[offset], sig_adata.extract(offset, width),
sig_d.extract(offset, width), sig_q.extract(offset, width));
import_attributes(cell->attributes, inst);
}
}
return true;
}
// FIXME: OPER_WIDE_DLATCH
#undef IN
#undef IN1
#undef IN2
@ -1790,6 +1865,7 @@ Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec s
log_assert(gclk == false);
log_assert(disable_sig == State::S0);
// FIXME: Adffe
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
@ -1801,12 +1877,25 @@ Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::Si
log_assert(gclk == false);
log_assert(disable_sig == State::S0);
// FIXME: Dffsre
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
}
Cell *VerificClocking::addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q)
{
log_assert(gclk == false);
log_assert(disable_sig == State::S0);
// FIXME: Aldffe
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
return module->addAldff(name, clock_sig, sig_aload, sig_d, sig_q, sig_adata, posedge);
}
// ==================================================================
struct VerificExtNets

View File

@ -50,6 +50,7 @@ struct VerificClocking {
RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
RTLIL::Cell *addAldff(IdString name, RTLIL::SigSpec sig_aload, RTLIL::SigSpec sig_adata, SigSpec sig_d, SigSpec sig_q);
bool property_matches_sequence(const VerificClocking &seq) const {
if (clock_net != seq.clock_net)