mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-21 05:13:40 +00:00
Code Activity

formalff: Fix -declockgate test and missing emit for memories

Browse source
This commit is contained in:
Jannis Harder 2025-04-18 18:57:59 +02:00
parent b982da9f6a
commit 31d6d0ac17
2 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

9
passes/sat/formalff.cc
View file

@ -790,9 +790,11 @@ struct FormalFfPass : public Pass {
ff.emit(); ff.emit();
} else if (clocked_cell->type == ID($mem_v2)) { } else if (clocked_cell->type == ID($mem_v2)) {
auto &mem = memories.at(clocked_cell->name); auto &mem = memories.at(clocked_cell->name);
bool changed = false;
for (auto &rd_port : mem.rd_ports) { for (auto &rd_port : mem.rd_ports) {
if (rd_port.clk_enable && rd_port.clk == clk && rd_port.clk_polarity == pol_clk) { if (rd_port.clk_enable && rd_port.clk == clk && rd_port.clk_polarity == pol_clk) {
log_warning("patching rd port\n"); log_debug("patching rd port\n");
changed = true;
rd_port.clk = gate_clock; rd_port.clk = gate_clock;
SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate)); SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
SigSpec en_mask = SigSpec(en_bit, GetSize(rd_port.en)); SigSpec en_mask = SigSpec(en_bit, GetSize(rd_port.en));
@ -801,13 +803,16 @@ struct FormalFfPass : public Pass {
} }
for (auto &wr_port : mem.wr_ports) { for (auto &wr_port : mem.wr_ports) {
if (wr_port.clk_enable && wr_port.clk == clk && wr_port.clk_polarity == pol_clk) { if (wr_port.clk_enable && wr_port.clk == clk && wr_port.clk_polarity == pol_clk) {
log_warning("patching wr port\n"); log_debug("patching wr port\n");
changed = true;
wr_port.clk = gate_clock; wr_port.clk = gate_clock;
SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate)); SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
SigSpec en_mask = SigSpec(en_bit, GetSize(wr_port.en)); SigSpec en_mask = SigSpec(en_bit, GetSize(wr_port.en));
wr_port.en = module->And(NEW_ID, wr_port.en, en_mask); wr_port.en = module->And(NEW_ID, wr_port.en, en_mask);
} }
} }
if (changed)
mem.emit();
} }
} }

12
tests/various/formalff_declockgate.ys
View file

@ -58,16 +58,20 @@ EOT
prep -auto-top prep -auto-top
opt_dff opt_dff
select -assert-count 1 t:$dlatch select -assert-count 1 t:$dlatch
select -assert-count 1 t:$dff
select -assert-count 1 t:$dffe
# Manually execute equiv_opt like pattern so clk2fflogic is called with # Manually execute equiv_opt like pattern so clk2fflogic is called with
# -nopeepopt, otherwise this doesn't test everything # -nopeepopt, otherwise this doesn't test everything
design -save preopt design -save preopt
check -assert check -assert
formalff -declockgate formalff -declockgate
check -assert
design -stash postopt design -save postopt
delete -output */clk_o
clean -purge
select -assert-count 0 t:$dlatch
design -reset
# Create miter and clk2fflogic without peepopt # Create miter and clk2fflogic without peepopt
design -copy-from preopt -as gold A:top design -copy-from preopt -as gold A:top