mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
formalff: Add -declockgate option
This commit is contained in:
Jannis Harder
parent
7f7ad87b7b
commit
bd154a7188
2 changed files with 292 additions and 1 deletions
|
|
@ -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
79
tests/various/formalff_declockgate.ys
Normal 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
|
||||
Loading…
Add table
Add a link
Reference in a new issue