mirror of
https://github.com/YosysHQ/yosys
synced 2026-06-19 07:16:27 +00:00
Merge pull request #5960 from YosysHQ/nella/latch-infer
proc_dlatch - infer $adlatch (Fix #5910).
This commit is contained in:
commit
2195277b5a
6 changed files with 366 additions and 18 deletions
|
|
@ -201,6 +201,77 @@ struct proc_dlatch_db_t
|
|||
sig[index] = State::Sx;
|
||||
cell->setPort(ID::A, sig);
|
||||
}
|
||||
bool sibling_undef = true;
|
||||
for (int i = 0; i < (is_bwmux ? 1 : GetSize(sig_s)); i++)
|
||||
if (sig_b[i*width + index] != State::Sx)
|
||||
sibling_undef = false;
|
||||
if (!sibling_undef) {
|
||||
if (!is_bwmux) {
|
||||
for (int i = 0; i < GetSize(sig_s); i++)
|
||||
n = make_inner(sig_s[i], State::S0, n);
|
||||
} else {
|
||||
n = make_inner(sig_s[index], State::S0, n);
|
||||
}
|
||||
}
|
||||
children.insert(n);
|
||||
}
|
||||
|
||||
for (int i = 0; i < (is_bwmux ? 1 : GetSize(sig_s)); i++) {
|
||||
n = find_mux_feedback(sig_b[i*width + index], needle, set_undef);
|
||||
if (n != false_node) {
|
||||
if (set_undef && sig_b[i*width + index] == needle) {
|
||||
SigSpec sig = cell->getPort(ID::B);
|
||||
sig[i*width + index] = State::Sx;
|
||||
cell->setPort(ID::B, sig);
|
||||
}
|
||||
bool sibling_undef = (sig_a[index] == State::Sx);
|
||||
if (!is_bwmux)
|
||||
for (int j = 0; j < GetSize(sig_s); j++)
|
||||
if (j != i && sig_b[j*width + index] != State::Sx)
|
||||
sibling_undef = false;
|
||||
if (!sibling_undef)
|
||||
n = make_inner(sig_s[is_bwmux ? index : i], State::S1, n);
|
||||
children.insert(n);
|
||||
}
|
||||
}
|
||||
|
||||
if (children.empty())
|
||||
return false_node;
|
||||
|
||||
return make_inner(children);
|
||||
}
|
||||
|
||||
int find_mux_constant(SigBit haystack, State needle, bool set_undef)
|
||||
{
|
||||
if (sigusers[haystack] > 1)
|
||||
set_undef = false;
|
||||
|
||||
if (haystack == SigBit(needle))
|
||||
return true_node;
|
||||
|
||||
auto it = mux_drivers.find(haystack);
|
||||
if (it == mux_drivers.end())
|
||||
return false_node;
|
||||
|
||||
Cell *cell = it->second.first;
|
||||
int index = it->second.second;
|
||||
|
||||
log_assert(cell->type.in(ID($mux), ID($pmux), ID($bwmux)));
|
||||
bool is_bwmux = (cell->type == ID($bwmux));
|
||||
SigSpec sig_a = sigmap(cell->getPort(ID::A));
|
||||
SigSpec sig_b = sigmap(cell->getPort(ID::B));
|
||||
SigSpec sig_s = sigmap(cell->getPort(ID::S));
|
||||
int width = GetSize(sig_a);
|
||||
|
||||
pool<int> children;
|
||||
|
||||
int n = find_mux_constant(sig_a[index], needle, set_undef);
|
||||
if (n != false_node) {
|
||||
if (set_undef && sig_a[index] == SigBit(needle)) {
|
||||
SigSpec sig = cell->getPort(ID::A);
|
||||
sig[index] = State::Sx;
|
||||
cell->setPort(ID::A, sig);
|
||||
}
|
||||
if (!is_bwmux) {
|
||||
for (int i = 0; i < GetSize(sig_s); i++)
|
||||
n = make_inner(sig_s[i], State::S0, n);
|
||||
|
|
@ -211,9 +282,9 @@ struct proc_dlatch_db_t
|
|||
}
|
||||
|
||||
for (int i = 0; i < (is_bwmux ? 1 : GetSize(sig_s)); i++) {
|
||||
n = find_mux_feedback(sig_b[i*width + index], needle, set_undef);
|
||||
n = find_mux_constant(sig_b[i*width + index], needle, set_undef);
|
||||
if (n != false_node) {
|
||||
if (set_undef && sig_b[i*width + index] == needle) {
|
||||
if (set_undef && sig_b[i*width + index] == SigBit(needle)) {
|
||||
SigSpec sig = cell->getPort(ID::B);
|
||||
sig[i*width + index] = State::Sx;
|
||||
cell->setPort(ID::B, sig);
|
||||
|
|
@ -349,7 +420,7 @@ void proc_dlatch(proc_dlatch_db_t &db, RTLIL::Process *proc)
|
|||
{
|
||||
RTLIL::SigSig latches_bits, nolatches_bits;
|
||||
dict<SigBit, SigBit> latches_out_in;
|
||||
dict<SigBit, int> latches_hold;
|
||||
dict<SigBit, int> latches_hold, latches_rst, latches_set;
|
||||
std::string src = proc->get_src_attribute();
|
||||
|
||||
for (auto sr : proc->syncs)
|
||||
|
|
@ -381,15 +452,31 @@ void proc_dlatch(proc_dlatch_db_t &db, RTLIL::Process *proc)
|
|||
|
||||
latches_out_in.sort();
|
||||
for (auto &it : latches_out_in) {
|
||||
int n = db.find_mux_feedback(it.second, it.first, true);
|
||||
if (n == db.false_node) {
|
||||
if (db.find_mux_feedback(it.second, it.first, false) == db.false_node) {
|
||||
nolatches_bits.first.append(it.first);
|
||||
nolatches_bits.second.append(it.second);
|
||||
} else {
|
||||
latches_bits.first.append(it.first);
|
||||
latches_bits.second.append(it.second);
|
||||
latches_hold[it.first] = n;
|
||||
continue;
|
||||
}
|
||||
|
||||
latches_bits.first.append(it.first);
|
||||
latches_bits.second.append(it.second);
|
||||
int nrst = db.find_mux_constant(it.second, State::S0, false);
|
||||
int nset = db.find_mux_constant(it.second, State::S1, false);
|
||||
bool has_rst = (nrst != db.false_node);
|
||||
bool has_set = (nset != db.false_node);
|
||||
|
||||
if (has_rst && !has_set)
|
||||
nrst = db.find_mux_constant(it.second, State::S0, true);
|
||||
else if (has_set && !has_rst)
|
||||
nset = db.find_mux_constant(it.second, State::S1, true);
|
||||
else
|
||||
nrst = nset = db.false_node;
|
||||
|
||||
int n = db.find_mux_feedback(it.second, it.first, true);
|
||||
log_assert(n != db.false_node);
|
||||
latches_hold[it.first] = n;
|
||||
latches_rst[it.first] = nrst;
|
||||
latches_set[it.first] = nset;
|
||||
}
|
||||
|
||||
int offset = 0;
|
||||
|
|
@ -423,20 +510,35 @@ void proc_dlatch(proc_dlatch_db_t &db, RTLIL::Process *proc)
|
|||
while (offset < GetSize(latches_bits.first))
|
||||
{
|
||||
int width = 1;
|
||||
int n = latches_hold[latches_bits.first[offset]];
|
||||
Wire *w = latches_bits.first[offset].wire;
|
||||
SigBit obit = latches_bits.first[offset];
|
||||
int n = latches_hold[obit];
|
||||
int nrst = latches_rst[obit];
|
||||
int nset = latches_set[obit];
|
||||
Wire *w = obit.wire;
|
||||
|
||||
if (w != nullptr)
|
||||
{
|
||||
while (offset+width < GetSize(latches_bits.first) &&
|
||||
n == latches_hold[latches_bits.first[offset+width]] &&
|
||||
nrst == latches_rst[latches_bits.first[offset+width]] &&
|
||||
nset == latches_set[latches_bits.first[offset+width]] &&
|
||||
w == latches_bits.first[offset+width].wire)
|
||||
width++;
|
||||
|
||||
SigSpec lhs = latches_bits.first.extract(offset, width);
|
||||
SigSpec rhs = latches_bits.second.extract(offset, width);
|
||||
|
||||
Cell *cell = db.module->addDlatch(NEW_ID, db.module->Not(NEW_ID, db.make_hold(n, src)), rhs, lhs);
|
||||
SigBit en = db.module->Not(NEW_ID, db.make_hold(n, src));
|
||||
bool has_rst = (nrst != db.false_node);
|
||||
bool has_set = (nset != db.false_node);
|
||||
|
||||
Cell *cell;
|
||||
if (has_rst)
|
||||
cell = db.module->addAdlatch(NEW_ID, en, db.make_hold(nrst, src), rhs, lhs, RTLIL::Const(State::S0, width));
|
||||
else if (has_set)
|
||||
cell = db.module->addAdlatch(NEW_ID, en, db.make_hold(nset, src), rhs, lhs, RTLIL::Const(State::S1, width));
|
||||
else
|
||||
cell = db.module->addDlatch(NEW_ID, en, rhs, lhs);
|
||||
cell->set_src_attribute(src);
|
||||
db.generated_dlatches.insert(cell);
|
||||
|
||||
|
|
|
|||
|
|
@ -370,10 +370,16 @@ struct DffLegalizePass : public Pass {
|
|||
else
|
||||
fail_ff(ff, "initialized dffs with async set and reset are not supported");
|
||||
} else {
|
||||
if (!supported_cells[FF_DLATCHSR])
|
||||
fail_ff(ff, "dlatch with async set and reset are not supported");
|
||||
else
|
||||
fail_ff(ff, "initialized dlatch with async set and reset are not supported");
|
||||
if (!supported_dlatch) {
|
||||
if (!supported_cells[FF_DLATCHSR])
|
||||
fail_ff(ff, "dlatch with async set and reset are not supported");
|
||||
else
|
||||
fail_ff(ff, "initialized dlatch with async set and reset are not supported");
|
||||
}
|
||||
if (ff.cell)
|
||||
log_warning("Emulating async set + reset latch with a plain D latch and logic for %s.%s\n", ff.module->name.unescape(), ff.cell->name.unescape());
|
||||
emulate_dlatch(ff);
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -449,6 +455,51 @@ struct DffLegalizePass : public Pass {
|
|||
legalize_ff(ff_sel);
|
||||
}
|
||||
|
||||
void emulate_dlatch(FfData &ff) {
|
||||
// emulate adlatch or dlatchsr
|
||||
log_assert(!ff.has_clk);
|
||||
log_assert(ff.has_aload);
|
||||
log_assert(ff.width == 1);
|
||||
|
||||
auto active_high = [&](SigBit sig, bool pol) -> SigBit {
|
||||
if (pol)
|
||||
return sig;
|
||||
return ff.is_fine ? ff.module->NotGate(NEW_ID, sig) : ff.module->Not(NEW_ID, sig)[0];
|
||||
};
|
||||
|
||||
auto do_mux = [&](SigBit a, SigBit b, SigBit s) -> SigBit {
|
||||
return ff.is_fine ? ff.module->MuxGate(NEW_ID, a, b, s) : ff.module->Mux(NEW_ID, a, b, s)[0];
|
||||
};
|
||||
|
||||
auto do_or = [&](SigBit a, SigBit b) -> SigBit {
|
||||
return ff.is_fine ? ff.module->OrGate(NEW_ID, a, b) : ff.module->Or(NEW_ID, a, b)[0];
|
||||
};
|
||||
|
||||
SigBit en = active_high(ff.sig_aload, ff.pol_aload);
|
||||
SigBit d = ff.sig_ad;
|
||||
|
||||
if (ff.has_sr) {
|
||||
SigBit set = active_high(ff.sig_set[0], ff.pol_set);
|
||||
SigBit clr = active_high(ff.sig_clr[0], ff.pol_clr);
|
||||
// clr > set > load > hold
|
||||
d = do_mux(d, State::S1, set);
|
||||
d = do_mux(d, State::S0, clr);
|
||||
en = do_or(en, do_or(set, clr));
|
||||
ff.has_sr = false;
|
||||
}
|
||||
if (ff.has_arst) {
|
||||
SigBit arst = active_high(ff.sig_arst[0], ff.pol_arst);
|
||||
d = do_mux(d, ff.val_arst[0], arst);
|
||||
en = do_or(en, arst);
|
||||
ff.has_arst = false;
|
||||
}
|
||||
|
||||
ff.sig_ad = d;
|
||||
ff.sig_aload = en;
|
||||
ff.pol_aload = true;
|
||||
legalize_dlatch(ff);
|
||||
}
|
||||
|
||||
void legalize_dff(FfData &ff) {
|
||||
if (!try_flip(ff, supported_dff)) {
|
||||
if (!supported_dff)
|
||||
|
|
@ -742,8 +793,14 @@ struct DffLegalizePass : public Pass {
|
|||
|
||||
void legalize_adlatch(FfData &ff) {
|
||||
if (!try_flip(ff, supported_adlatch)) {
|
||||
if (!supported_adlatch)
|
||||
fail_ff(ff, "D latches with async set or reset are not supported");
|
||||
if (!supported_adlatch) {
|
||||
if (!supported_dlatch)
|
||||
fail_ff(ff, "D latches with async set or reset are not supported");
|
||||
if (ff.cell)
|
||||
log_warning("Emulating async reset latch with a plain D latch and logic for %s.%s\n", ff.module->name.unescape(), ff.cell->name.unescape());
|
||||
emulate_dlatch(ff);
|
||||
return;
|
||||
}
|
||||
if (!(supported_dlatch & (INIT_0 | INIT_1)))
|
||||
fail_ff(ff, "initialized D latches are not supported");
|
||||
|
||||
|
|
|
|||
133
tests/proc/proc_dlatch.ys
Normal file
133
tests/proc/proc_dlatch.ys
Normal file
|
|
@ -0,0 +1,133 @@
|
|||
read_verilog -formal <<EOT
|
||||
module top(input g, rn, d, output reg q);
|
||||
always @* if (~rn) q <= 0; else if (g) q <= d;
|
||||
always @* begin
|
||||
if (~rn) assert(q == 0);
|
||||
else if (g) assert(q == d);
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$adlatch
|
||||
select -assert-count 0 t:$dlatch
|
||||
select -assert-count 0 t:$dlatchsr
|
||||
|
||||
simplemap
|
||||
select -assert-count 1 t:$_DLATCH_PN0_
|
||||
clk2fflogic
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
module top(input gn, rn, d, output reg q);
|
||||
always @* if (rn==0) q <= 0; else if (gn==0) q <= d;
|
||||
always @* begin
|
||||
if (rn==0) assert(q == 0);
|
||||
else if (gn==0) assert(q == d);
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$adlatch
|
||||
simplemap
|
||||
select -assert-count 1 t:$_DLATCH_NN0_
|
||||
clk2fflogic
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
module top(input g, sn, d, output reg q);
|
||||
always @* if (~sn) q <= 1; else if (g) q <= d;
|
||||
always @* begin
|
||||
if (~sn) assert(q == 1);
|
||||
else if (g) assert(q == d);
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$adlatch
|
||||
simplemap
|
||||
select -assert-count 1 t:$_DLATCH_PN1_
|
||||
clk2fflogic
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
module top(input g, sn, rn, d, output reg q);
|
||||
always @* if (~rn) q <= 0; else if (~sn) q <= 1; else if (g) q <= d;
|
||||
always @* begin
|
||||
if (~rn) assert(q == 0);
|
||||
else if (~sn) assert(q == 1);
|
||||
else if (g) assert(q == d);
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 0 t:$adlatch
|
||||
select -assert-count 0 t:$dlatchsr
|
||||
select -assert-count 1 t:$dlatch
|
||||
clk2fflogic
|
||||
sat -tempinduct -verify -prove-asserts
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module top(input g, d, output reg q);
|
||||
always @* if (g) q <= d;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 t:$dlatch
|
||||
select -assert-count 0 t:$adlatch
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
module gold(input g, rn, d, zero, output reg q);
|
||||
always @* if (~rn | g) q <= (~rn ? zero : d);
|
||||
always @* assume(zero == 1'b0);
|
||||
endmodule
|
||||
module gate(input g, rn, d, zero, output reg q);
|
||||
always @* if (~rn) q <= 1'b0; else if (g) q <= d;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 -module gold t:$dlatch
|
||||
select -assert-count 1 -module gate t:$adlatch
|
||||
select -clear
|
||||
equiv_make gold gate equiv
|
||||
hierarchy -top equiv
|
||||
clk2fflogic
|
||||
equiv_induct -set-assumes
|
||||
equiv_status -assert
|
||||
|
||||
design -reset
|
||||
|
||||
read_verilog -formal <<EOT
|
||||
module gold(input g, sn, d, one, output reg q);
|
||||
always @* if (~sn | g) q <= (~sn ? one : d);
|
||||
always @* assume(one == 1'b1);
|
||||
endmodule
|
||||
module gate(input g, sn, d, one, output reg q);
|
||||
always @* if (~sn) q <= 1'b1; else if (g) q <= d;
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
select -assert-count 1 -module gold t:$dlatch
|
||||
select -assert-count 1 -module gate t:$adlatch
|
||||
select -clear
|
||||
equiv_make gold gate equiv
|
||||
hierarchy -top equiv
|
||||
clk2fflogic
|
||||
equiv_induct -set-assumes
|
||||
equiv_status -assert
|
||||
11
tests/proc/yosys_latch.sv
Normal file
11
tests/proc/yosys_latch.sv
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
module yosys_latch (
|
||||
input logic dlatch_p_d, input logic dlatch_p_g, output logic dlatch_p_q,
|
||||
input logic dlatch_n_d, input logic dlatch_n_gn, output logic dlatch_n_q,
|
||||
input logic dlatch_pn0_d, input logic dlatch_pn0_rn, input logic dlatch_pn0_g, output logic dlatch_pn0_q,
|
||||
input logic dlatch_nn0_d, input logic dlatch_nn0_rn, input logic dlatch_nn0_gn, output logic dlatch_nn0_q
|
||||
);
|
||||
always_latch if (dlatch_p_g) dlatch_p_q <= dlatch_p_d;
|
||||
always_latch if (~dlatch_n_gn) dlatch_n_q <= dlatch_n_d;
|
||||
always_latch if (~dlatch_pn0_rn) dlatch_pn0_q <= 1'b0; else if (dlatch_pn0_g) dlatch_pn0_q <= dlatch_pn0_d;
|
||||
always @* if (dlatch_nn0_rn == 1'b0) dlatch_nn0_q <= 1'b0; else if (dlatch_nn0_gn == 1'b0) dlatch_nn0_q <= dlatch_nn0_d;
|
||||
endmodule
|
||||
20
tests/proc/yosys_latch.ys
Normal file
20
tests/proc/yosys_latch.ys
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
# https://github.com/YosysHQ/yosys/issues/5910
|
||||
|
||||
read_verilog -sv yosys_latch.sv
|
||||
hierarchy -check -top yosys_latch
|
||||
proc
|
||||
design -save gold
|
||||
opt
|
||||
select -assert-count 2 t:$adlatch
|
||||
select -assert-count 2 t:$dlatch
|
||||
simplemap
|
||||
opt_clean
|
||||
select -assert-count 1 t:$_DLATCH_P_
|
||||
select -assert-count 1 t:$_DLATCH_N_
|
||||
select -assert-count 1 t:$_DLATCH_PN0_
|
||||
select -assert-count 1 t:$_DLATCH_NN0_
|
||||
select -assert-count 4 t:*
|
||||
design -load gold
|
||||
equiv_opt -assert -multiclock simplemap
|
||||
|
||||
design -reset
|
||||
25
tests/techmap/dfflegalize_dlatch_emu.ys
Normal file
25
tests/techmap/dfflegalize_dlatch_emu.ys
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
read_verilog -icells <<EOT
|
||||
|
||||
module top(input E, S, R, D, output [5:0] Q);
|
||||
$_DLATCH_PP0_ ff0 (.E(E), .R(R), .D(D), .Q(Q[0]));
|
||||
$_DLATCH_PN0_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1]));
|
||||
$_DLATCH_PP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2]));
|
||||
$_DLATCH_PN1_ ff3 (.E(E), .R(R), .D(D), .Q(Q[3]));
|
||||
$_DLATCHSR_PPP_ ff4 (.E(E), .S(S), .R(R), .D(D), .Q(Q[4]));
|
||||
$_DLATCHSR_PNP_ ff5 (.E(E), .S(S), .R(R), .D(D), .Q(Q[5]));
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
design -save orig
|
||||
|
||||
logger -expect warning "Emulating async reset latch with a plain D latch" 4
|
||||
logger -expect warning "Emulating async set \+ reset latch with a plain D latch" 2
|
||||
equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_P_ x
|
||||
logger -check-expected
|
||||
|
||||
design -load orig
|
||||
dfflegalize -cell $_DLATCH_P_ x
|
||||
select -assert-count 6 t:$_DLATCH_P_
|
||||
select -assert-count 0 t:$_DLATCHSR_???_
|
||||
select -assert-count 0 t:$_DLATCH_??0_
|
||||
select -assert-count 0 t:$_DLATCH_??1_
|
||||
Loading…
Add table
Add a link
Reference in a new issue