mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-11 03:33:36 +00:00
Code Activity

formalff: Add -declockgate option

Browse source
This commit is contained in:
Jannis Harder 2024-11-26 17:20:34 +01:00
parent 2fa7076edc
commit 904b4194cc
2 changed files with 292 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

214
passes/sat/formalff.cc
View file

@ -22,6 +22,7 @@
#include "kernel/ffinit.h"
#include "kernel/ff.h"
#include "kernel/modtools.h"
#include "kernel/mem.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@ -549,6 +550,7 @@ struct FormalFfPass : public Pass {
bool flag_setundef = false;
bool flag_hierarchy = false;
bool flag_assume = false;
bool flag_declockgate = false;
log_header(design, "Executing FORMALFF pass.\n");
@ -583,22 +585,232 @@ struct FormalFfPass : public Pass {
flag_assume = true;
continue;
}
if (args[argidx] == "-declockgate") {
flag_declockgate = true;
continue;
}
break;
}
extra_args(args, argidx, design);
if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume || flag_declockgate))
log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
if (flag_ff2anyinit && flag_anyinit2ff)
log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
if (flag_ff2anyinit && flag_declockgate)
log_cmd_error("The options -ff2anyinit and -declockgate are exclusive.\n");
if (flag_fine && !flag_anyinit2ff)
log_cmd_error("The option -fine requries the -anyinit2ff option.\n");
if (flag_fine && flag_clk2ff)
log_cmd_error("The options -fine and -clk2ff are exclusive.\n");
if (flag_declockgate)
{
for (auto module : design->selected_modules())
{
ModWalker modwalker(design);
modwalker.setup(module);
SigMap &sigmap = modwalker.sigmap;
FfInitVals initvals(&modwalker.sigmap, module);
dict<IdString, Mem> memories;
for (auto mem : Mem::get_selected_memories(module)) {
if (!mem.packed)
continue;
memories.emplace(mem.cell->name, std::move(mem));
}
dict<pair<SigBit, bool>, vector<Cell *>> clk_bits;
pool<SigBit> input_bits;
pool<pair<SigBit, bool>> input_clk_bits;
for (auto cell : module->selected_cells()) {
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
FfData ff(&initvals, cell);
if (!ff.has_clk)
continue;
SigBit clk = sigmap(ff.sig_clk);
clk_bits[{clk, ff.pol_clk}].push_back(cell);
} else if (cell->type == ID($mem_v2)) {
auto const &mem = memories.at(cell->name);
for (auto &rd_port : mem.rd_ports)
if (rd_port.clk_enable)
clk_bits[{rd_port.clk, rd_port.clk_polarity}].push_back(mem.cell);
for (auto &wr_port : mem.wr_ports)
if (wr_port.clk_enable)
clk_bits[{wr_port.clk, wr_port.clk_polarity}].push_back(mem.cell);
}
// XXX $check $print
}
log_debug("%s has %d clk bits\n", log_id(module), GetSize(clk_bits));
for (auto port : module->ports) {
Wire *wire = module->wire(port);
if (!wire->port_input)
continue;
for (auto bit : SigSpec(wire)) {
input_bits.insert(bit);
for (bool pol : {false, true}) {
if (clk_bits.count({bit, pol})) {
input_clk_bits.insert({bit, pol});
clk_bits.erase({bit, pol});
}
}
}
}
log_debug("%s has %d non-input clk bits\n", log_id(module), GetSize(clk_bits));
if (clk_bits.empty())
continue;
for (auto &clk_bit : clk_bits)
{
SigBit clk = clk_bit.first.first;
bool pol_clk = clk_bit.first.second;
vector<Cell *> &clocked_cells = clk_bit.second;
if (!clk.is_wire()) {
log_debug("constant clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
continue;
}
if (input_bits.count(clk)) {
log_debug("input clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
continue;
}
auto found = modwalker.signal_drivers.find(clk);
if (found == modwalker.signal_drivers.end() || found->second.empty()) {
log_debug("undriven clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
continue;
}
if (found->second.size() > 1) {
log_debug("multiple drivers for clk bit %s.%s\n", log_id(module), log_signal(SigSpec(clk)));
continue;
}
auto driver = *found->second.begin();
bool is_gate =
pol_clk ? driver.cell->type.in(ID($and), ID($_AND_)) : driver.cell->type.in(ID($or), ID($_OR_));
if (!is_gate) {
log_debug("unsupported gating logic %s.%s (%s) for clock %s %s.%s\n", log_id(module),
log_id(driver.cell), log_id(driver.cell->type), pol_clk ? "posedge" : "negedge",
log_id(module), log_signal(SigSpec(clk)));
continue;
}
SigBit gate_clock = sigmap(driver.cell->getPort(ID::A)[driver.offset]);
SigBit gate_enable = sigmap(driver.cell->getPort(ID::B)[driver.offset]);
std::swap(gate_clock, gate_enable);
for (int i = 0; i < 2; i++) {
std::swap(gate_clock, gate_enable);
log_debug("clock %s.%s for gated clk bit %s.%s\n", log_id(module), log_signal(SigSpec(gate_clock)),
log_id(module), log_signal(SigSpec(clk)));
log_debug("enable %s.%s for gated clk bit %s.%s\n", log_id(module), log_signal(SigSpec(gate_enable)),
log_id(module), log_signal(SigSpec(clk)));
found = modwalker.signal_drivers.find(gate_enable);
if (found == modwalker.signal_drivers.end() || found->second.empty()) {
log_debug("undriven gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
continue;
}
if (found->second.size() > 1) {
log_debug("multiple drivers for gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
continue;
}
auto gate_driver = *found->second.begin();
if (!RTLIL::builtin_ff_cell_types().count(gate_driver.cell->type)) {
log_debug("non FF driver for gate enable %s.%s of gated clk bit %s.%s\n", log_id(module),
log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)));
continue;
}
FfData ff(&initvals, gate_driver.cell);
if (ff.has_gclk || ff.has_ce || ff.has_sr || ff.has_srst || ff.has_arst || (ff.has_aload && ff.has_clk)) {
log_debug(
"FF driver for gate enable %s.%s of gated clk bit %s.%s has incompatible type: %s\n",
log_id(module), log_signal(SigSpec(gate_enable)), log_id(module), log_signal(SigSpec(clk)),
log_id(gate_driver.cell->type));
continue;
}
if (ff.has_aload) {
// this ff is intentionally not emitted!
ff.has_aload = false;
ff.has_clk = true;
ff.pol_clk = !ff.pol_arst;
ff.sig_clk = ff.sig_aload;
ff.sig_d = ff.sig_ad;
}
if (!ff.has_clk || sigmap(ff.sig_clk) != gate_clock || ff.pol_clk != pol_clk) {
log_debug("FF driver for gate enable %s.%s of gated clk bit %s.%s has incompatible clocking: "
"%s %s.%s\n",
log_id(module), log_signal(SigSpec(gate_enable)), log_id(module),
log_signal(SigSpec(clk)), ff.pol_clk ? "posedge" : "negedge", log_id(module),
log_signal(SigSpec(ff.sig_clk)));
continue;
}
SigBit sig_gate = ff.sig_d[gate_driver.offset];
log_debug("found clock gate, rewriting %d cells\n", GetSize(clocked_cells));
for (auto clocked_cell : clocked_cells) {
log_debug("rewriting cell %s.%s (%s)\n", log_id(module), log_id(clocked_cell),
log_id(clocked_cell->type));
if (RTLIL::builtin_ff_cell_types().count(clocked_cell->type)) {
FfData ff(&initvals, clocked_cell);
log_assert(ff.has_clk);
ff.unmap_ce();
ff.pol_ce = pol_clk;
ff.sig_ce = sig_gate;
ff.has_ce = true;
ff.sig_clk = gate_clock;
ff.emit();
} else if (clocked_cell->type == ID($mem_v2)) {
auto &mem = memories.at(clocked_cell->name);
for (auto &rd_port : mem.rd_ports) {
if (rd_port.clk_enable && rd_port.clk == clk && rd_port.clk_polarity == pol_clk) {
log_warning("patching rd port\n");
rd_port.clk = gate_clock;
SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
SigSpec en_mask = SigSpec(en_bit, GetSize(rd_port.en));
rd_port.en = module->And(NEW_ID, rd_port.en, en_mask);
}
}
for (auto &wr_port : mem.wr_ports) {
if (wr_port.clk_enable && wr_port.clk == clk && wr_port.clk_polarity == pol_clk) {
log_warning("patching wr port\n");
wr_port.clk = gate_clock;
SigBit en_bit = pol_clk ? sig_gate : SigBit(module->Not(NEW_ID, sig_gate));
SigSpec en_mask = SigSpec(en_bit, GetSize(wr_port.en));
wr_port.en = module->And(NEW_ID, wr_port.en, en_mask);
}
}
}
}
break;
}
}
}
}
for (auto module : design->selected_modules())
{
if (flag_setundef)

79
tests/various/formalff_declockgate.ys Normal file
View file

@ -0,0 +1,79 @@
# based on the peepopt_formal.ys test
read_verilog -sv <<EOT
module peepopt_formal_clockgateff_0(
input logic clk_i,
input logic ena_i,
input logic enb_i,
input logic enc_i,
input logic d_0_i,
input logic d_1_i,
output logic clk_o,
output logic d_0_o,
output logic d_1_o,
output logic d_2_o
);
logic en_latched;
initial d_0_o = '0;
initial d_1_o = '0;
initial en_latched = '0;
initial d_2_o = '0;
reg mem [4];
initial begin
mem[0] = 0;
mem[1] = 0;
mem[2] = 0;
mem[3] = 0;
end
reg [1:0] counter = 0;
always_latch
if (!clk_i)
en_latched <= ena_i | enb_i;
assign clk_o = en_latched & clk_i;
always @(posedge clk_o)
d_0_o <= d_0_i;
always @(posedge clk_o)
if (enc_i)
d_1_o <= d_1_i;
always @(posedge clk_o) begin
counter <= counter + 1;
mem[counter] <= mem[counter] + 1;
d_2_o <= mem[counter] + 1;
end;
endmodule
EOT
# Check original design has latch
prep -auto-top
opt_dff
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
# -nopeepopt, otherwise this doesn't test everything
design -save preopt
check -assert
formalff -declockgate
check -assert
design -stash postopt
# Create miter and clk2fflogic without peepopt
design -copy-from preopt -as gold A:top
design -copy-from postopt -as gate A:top
clk2fflogic -nopeepopt
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
memory_map -formal
sat -prove-asserts -seq 16 -show-public -verify equiv