mirror of https://github.com/YosysHQ/yosys.git
Merge branch 'main' of github.com:silimate/yosys into sim
This commit is contained in:
commit
d2cd4d2cc8
7
Makefile
7
Makefile
|
|
@ -763,6 +763,10 @@ include $(YOSYS_SRC)/passes/silimate/Makefile.inc
|
|||
|
||||
OBJS += passes/sat/recover_names.o
|
||||
OBJS += passes/sat/sim.o
|
||||
OBJS += passes/sat/sat.o
|
||||
OBJS += passes/sat/miter.o
|
||||
OBJS += passes/sat/async2sync.o
|
||||
OBJS += passes/sat/clk2fflogic.o
|
||||
OBJS += passes/techmap/extract.o
|
||||
OBJS += passes/techmap/extract_reduce.o
|
||||
OBJS += passes/techmap/alumacc.o
|
||||
|
|
@ -773,6 +777,8 @@ OBJS += passes/techmap/muxcover.o
|
|||
OBJS += passes/techmap/aigmap.o
|
||||
OBJS += passes/techmap/attrmap.o
|
||||
OBJS += passes/techmap/clockgate.o
|
||||
OBJS += passes/techmap/dffunmap.o
|
||||
OBJS += passes/techmap/zinit.o
|
||||
|
||||
include $(YOSYS_SRC)/passes/hierarchy/Makefile.inc
|
||||
include $(YOSYS_SRC)/passes/memory/Makefile.inc
|
||||
|
|
@ -785,6 +791,7 @@ include $(YOSYS_SRC)/passes/techmap/Makefile.inc
|
|||
include $(YOSYS_SRC)/backends/verilog/Makefile.inc
|
||||
include $(YOSYS_SRC)/backends/rtlil/Makefile.inc
|
||||
include $(YOSYS_SRC)/backends/json/Makefile.inc
|
||||
include $(YOSYS_SRC)/backends/blif/Makefile.inc
|
||||
|
||||
include $(YOSYS_SRC)/techlibs/common/Makefile.inc
|
||||
|
||||
|
|
|
|||
|
|
@ -1593,6 +1593,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
|
|||
Instance *inst;
|
||||
PortRef *pr;
|
||||
Att *attr;
|
||||
pool<Net*> empty_port_nets;
|
||||
|
||||
FOREACH_ATTRIBUTE(nl, mi, attr) {
|
||||
if (!strcmp(attr->Key(), "noblackbox"))
|
||||
|
|
@ -1604,6 +1605,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
|
|||
if (port->Bus())
|
||||
continue;
|
||||
|
||||
if (port->GetAtt(" empty_port")) {
|
||||
if (port->GetNet())
|
||||
empty_port_nets.insert(port->GetNet());
|
||||
continue;
|
||||
}
|
||||
|
||||
if (verific_verbose)
|
||||
log(" importing port %s.\n", port->Name());
|
||||
|
||||
|
|
@ -1687,6 +1694,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
|
|||
|
||||
FOREACH_NET_OF_NETLIST(nl, mi, net)
|
||||
{
|
||||
if (empty_port_nets.count(net))
|
||||
continue;
|
||||
|
||||
if (net->IsRamNet())
|
||||
{
|
||||
RTLIL::Memory *memory = new RTLIL::Memory;
|
||||
|
|
@ -2291,6 +2301,8 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
|
|||
}
|
||||
|
||||
FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
|
||||
if (pr->GetPort()->GetAtt(" empty_port"))
|
||||
continue;
|
||||
if (verific_verbose)
|
||||
log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
|
||||
const char *port_name = pr->GetPort()->Name();
|
||||
|
|
|
|||
|
|
@ -753,6 +753,40 @@ namespace {
|
|||
int n_wr_ports = cell->parameters.at(ID::WR_PORTS).as_int();
|
||||
Const rd_wide_continuation = is_compat ? Const(State::S0, n_rd_ports) : cell->parameters.at(ID::RD_WIDE_CONTINUATION);
|
||||
Const wr_wide_continuation = is_compat ? Const(State::S0, n_wr_ports) : cell->parameters.at(ID::WR_WIDE_CONTINUATION);
|
||||
pool<IdString> bad_params;
|
||||
if (!is_compat) {
|
||||
auto check_param_size = [&](IdString param_name, int expected_size) {
|
||||
const Const ¶m = cell->parameters.at(param_name);
|
||||
if (GetSize(param) != expected_size) {
|
||||
log_warning("Memory cell %s.%s (%s) has inconsistent parameter %s: expected size %d, got %d\n",
|
||||
log_id(cell->module), log_id(cell), log_id(res.memid),
|
||||
log_id(param_name), expected_size, GetSize(param));
|
||||
bad_params.insert(param_name);
|
||||
}
|
||||
};
|
||||
check_param_size(ID::RD_WIDE_CONTINUATION, n_rd_ports);
|
||||
check_param_size(ID::RD_CLK_ENABLE, n_rd_ports);
|
||||
check_param_size(ID::RD_CLK_POLARITY, n_rd_ports);
|
||||
check_param_size(ID::RD_CE_OVER_SRST, n_rd_ports);
|
||||
check_param_size(ID::RD_ARST_VALUE, n_rd_ports * res.width);
|
||||
check_param_size(ID::RD_SRST_VALUE, n_rd_ports * res.width);
|
||||
check_param_size(ID::RD_INIT_VALUE, n_rd_ports * res.width);
|
||||
check_param_size(ID::RD_TRANSPARENCY_MASK, n_rd_ports * n_wr_ports);
|
||||
check_param_size(ID::RD_COLLISION_X_MASK, n_rd_ports * n_wr_ports);
|
||||
check_param_size(ID::WR_WIDE_CONTINUATION, n_wr_ports);
|
||||
check_param_size(ID::WR_CLK_ENABLE, n_wr_ports);
|
||||
check_param_size(ID::WR_CLK_POLARITY, n_wr_ports);
|
||||
check_param_size(ID::WR_PRIORITY_MASK, n_wr_ports * n_wr_ports);
|
||||
if (bad_params.count(ID::RD_WIDE_CONTINUATION))
|
||||
rd_wide_continuation = Const(State::S0, n_rd_ports);
|
||||
if (bad_params.count(ID::WR_WIDE_CONTINUATION))
|
||||
wr_wide_continuation = Const(State::S0, n_wr_ports);
|
||||
}
|
||||
auto safe_param_extract = [&](IdString param_name, int offset, int len) -> Const {
|
||||
if (bad_params.count(param_name))
|
||||
return Const(State::S0, len);
|
||||
return cell->parameters.at(param_name).extract(offset, len);
|
||||
};
|
||||
for (int i = 0, ni; i < n_rd_ports; i = ni) {
|
||||
ni = i + 1;
|
||||
while (ni < n_rd_ports && rd_wide_continuation[ni] == State::S1)
|
||||
|
|
@ -760,8 +794,8 @@ namespace {
|
|||
MemRd mrd;
|
||||
mrd.wide_log2 = ceil_log2(ni - i);
|
||||
log_assert(ni - i == (1 << mrd.wide_log2));
|
||||
mrd.clk_enable = cell->parameters.at(ID::RD_CLK_ENABLE).extract(i, 1).as_bool();
|
||||
mrd.clk_polarity = cell->parameters.at(ID::RD_CLK_POLARITY).extract(i, 1).as_bool();
|
||||
mrd.clk_enable = safe_param_extract(ID::RD_CLK_ENABLE, i, 1).as_bool();
|
||||
mrd.clk_polarity = safe_param_extract(ID::RD_CLK_POLARITY, i, 1).as_bool();
|
||||
mrd.clk = cell->getPort(ID::RD_CLK).extract(i, 1);
|
||||
mrd.en = cell->getPort(ID::RD_EN).extract(i, 1);
|
||||
mrd.addr = cell->getPort(ID::RD_ADDR).extract(i * abits, abits);
|
||||
|
|
@ -774,16 +808,16 @@ namespace {
|
|||
mrd.arst = State::S0;
|
||||
mrd.srst = State::S0;
|
||||
} else {
|
||||
mrd.ce_over_srst = cell->parameters.at(ID::RD_CE_OVER_SRST).extract(i, 1).as_bool();
|
||||
mrd.arst_value = cell->parameters.at(ID::RD_ARST_VALUE).extract(i * res.width, (ni - i) * res.width);
|
||||
mrd.srst_value = cell->parameters.at(ID::RD_SRST_VALUE).extract(i * res.width, (ni - i) * res.width);
|
||||
mrd.init_value = cell->parameters.at(ID::RD_INIT_VALUE).extract(i * res.width, (ni - i) * res.width);
|
||||
mrd.ce_over_srst = safe_param_extract(ID::RD_CE_OVER_SRST, i, 1).as_bool();
|
||||
mrd.arst_value = safe_param_extract(ID::RD_ARST_VALUE, i * res.width, (ni - i) * res.width);
|
||||
mrd.srst_value = safe_param_extract(ID::RD_SRST_VALUE, i * res.width, (ni - i) * res.width);
|
||||
mrd.init_value = safe_param_extract(ID::RD_INIT_VALUE, i * res.width, (ni - i) * res.width);
|
||||
mrd.arst = cell->getPort(ID::RD_ARST).extract(i, 1);
|
||||
mrd.srst = cell->getPort(ID::RD_SRST).extract(i, 1);
|
||||
}
|
||||
if (!is_compat) {
|
||||
Const transparency_mask = cell->parameters.at(ID::RD_TRANSPARENCY_MASK).extract(i * n_wr_ports, n_wr_ports);
|
||||
Const collision_x_mask = cell->parameters.at(ID::RD_COLLISION_X_MASK).extract(i * n_wr_ports, n_wr_ports);
|
||||
Const transparency_mask = safe_param_extract(ID::RD_TRANSPARENCY_MASK, i * n_wr_ports, n_wr_ports);
|
||||
Const collision_x_mask = safe_param_extract(ID::RD_COLLISION_X_MASK, i * n_wr_ports, n_wr_ports);
|
||||
for (int j = 0; j < n_wr_ports; j++)
|
||||
if (wr_wide_continuation[j] != State::S1) {
|
||||
mrd.transparency_mask.push_back(transparency_mask[j] == State::S1);
|
||||
|
|
@ -799,14 +833,14 @@ namespace {
|
|||
MemWr mwr;
|
||||
mwr.wide_log2 = ceil_log2(ni - i);
|
||||
log_assert(ni - i == (1 << mwr.wide_log2));
|
||||
mwr.clk_enable = cell->parameters.at(ID::WR_CLK_ENABLE).extract(i, 1).as_bool();
|
||||
mwr.clk_polarity = cell->parameters.at(ID::WR_CLK_POLARITY).extract(i, 1).as_bool();
|
||||
mwr.clk_enable = safe_param_extract(ID::WR_CLK_ENABLE, i, 1).as_bool();
|
||||
mwr.clk_polarity = safe_param_extract(ID::WR_CLK_POLARITY, i, 1).as_bool();
|
||||
mwr.clk = cell->getPort(ID::WR_CLK).extract(i, 1);
|
||||
mwr.en = cell->getPort(ID::WR_EN).extract(i * res.width, (ni - i) * res.width);
|
||||
mwr.addr = cell->getPort(ID::WR_ADDR).extract(i * abits, abits);
|
||||
mwr.data = cell->getPort(ID::WR_DATA).extract(i * res.width, (ni - i) * res.width);
|
||||
if (!is_compat) {
|
||||
Const priority_mask = cell->parameters.at(ID::WR_PRIORITY_MASK).extract(i * n_wr_ports, n_wr_ports);
|
||||
Const priority_mask = safe_param_extract(ID::WR_PRIORITY_MASK, i * n_wr_ports, n_wr_ports);
|
||||
for (int j = 0; j < n_wr_ports; j++)
|
||||
if (wr_wide_continuation[j] != State::S1)
|
||||
mwr.priority_mask.push_back(priority_mask[j] == State::S1);
|
||||
|
|
@ -832,7 +866,7 @@ namespace {
|
|||
auto &port = res.rd_ports[i];
|
||||
port.transparency_mask.resize(GetSize(res.wr_ports));
|
||||
port.collision_x_mask.resize(GetSize(res.wr_ports));
|
||||
if (!cell->parameters.at(ID::RD_TRANSPARENT).extract(i, 1).as_bool())
|
||||
if (!cell->parameters.at(ID::RD_TRANSPARENT).extract(i, 1, State::S0).as_bool())
|
||||
continue;
|
||||
if (!port.clk_enable)
|
||||
continue;
|
||||
|
|
|
|||
|
|
@ -4568,19 +4568,15 @@ const RTLIL::Const &RTLIL::Cell::getParam(RTLIL::IdString paramname) const
|
|||
std::map<std::string, int> RTLIL::Cell::getParamsAsInts() const
|
||||
{
|
||||
std::map<std::string, int> result;
|
||||
for (auto ¶m : parameters) {
|
||||
std::string key = param.first.str();
|
||||
if (key.size() > 0 && key[0] == '\\')
|
||||
key = key.substr(1);
|
||||
result[key] = param.second.as_int();
|
||||
}
|
||||
for (const auto ¶m : parameters)
|
||||
result[RTLIL::unescape_id(param.first)] = param.second.as_int();
|
||||
return result;
|
||||
}
|
||||
|
||||
double RTLIL::Cell::maxInputConstRatio() const
|
||||
{
|
||||
double max_ratio = 0.0;
|
||||
for (auto &conn : connections_) {
|
||||
for (const auto &conn : connections_) {
|
||||
if (input(conn.first)) {
|
||||
double ratio = conn.second.const_ratio();
|
||||
if (ratio > max_ratio)
|
||||
|
|
@ -4590,6 +4586,24 @@ double RTLIL::Cell::maxInputConstRatio() const
|
|||
return max_ratio;
|
||||
}
|
||||
|
||||
std::vector<std::string> RTLIL::Cell::getOutputPortNames() const
|
||||
{
|
||||
std::vector<std::string> result;
|
||||
for (const auto &conn : connections_) {
|
||||
if (output(conn.first))
|
||||
result.push_back(RTLIL::unescape_id(conn.first));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
std::map<std::string, int> RTLIL::Cell::getConnectionSizes() const
|
||||
{
|
||||
std::map<std::string, int> result;
|
||||
for (const auto &conn : connections_)
|
||||
result[RTLIL::unescape_id(conn.first)] = conn.second.size();
|
||||
return result;
|
||||
}
|
||||
|
||||
void RTLIL::Cell::sort()
|
||||
{
|
||||
connections_.sort(sort_by_id_str());
|
||||
|
|
|
|||
|
|
@ -2539,6 +2539,12 @@ public:
|
|||
// Returns the maximum const_ratio() across all input ports, 0.0 if no input ports
|
||||
double maxInputConstRatio() const;
|
||||
|
||||
// Returns the names of all output ports (backslash-stripped)
|
||||
std::vector<std::string> getOutputPortNames() const;
|
||||
|
||||
// Returns {port_name: sig.size()} for all connections, port names backslash-stripped
|
||||
std::map<std::string, int> getConnectionSizes() const;
|
||||
|
||||
void sort();
|
||||
void check();
|
||||
void fixup_parameters(bool set_a_signed = false, bool set_b_signed = false);
|
||||
|
|
|
|||
|
|
@ -15,6 +15,8 @@ OBJS += passes/silimate/splitfanout.o
|
|||
OBJS += passes/silimate/splitlarge.o
|
||||
OBJS += passes/silimate/splitnetlist.o
|
||||
OBJS += passes/silimate/opt_timing_balance.o
|
||||
OBJS += passes/silimate/cone_partition.o
|
||||
OBJS += passes/silimate/clkmerge.o
|
||||
|
||||
OBJS += passes/silimate/opt_expand.o
|
||||
GENFILES += passes/silimate/peepopt_expand.h
|
||||
|
|
|
|||
|
|
@ -0,0 +1,177 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) 2026 Silimate Inc.
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/ff.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct ClkMergePass : public Pass {
|
||||
ClkMergePass() : Pass("clkmerge", "merge multiple clock domains into one") { }
|
||||
void help() override
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" clkmerge [-target <signal>] [selection]\n");
|
||||
log("\n");
|
||||
log("This command rewrites all flip-flop clock ports and polarities in the\n");
|
||||
log("selected modules to use a single clock domain, merging both different\n");
|
||||
log("clock signals and different clock polarities (posedge vs negedge).\n");
|
||||
log("\n");
|
||||
log("This is useful for miter-based equivalence checking where gold and gate\n");
|
||||
log("copies may use different clock signal names or opposite edges for what\n");
|
||||
log("is logically the same clock. Without merging, ABC's -dff mode will\n");
|
||||
log("partition them into separate clock domains, creating spurious cross-domain\n");
|
||||
log("ports that degrade SAT performance.\n");
|
||||
log("\n");
|
||||
log(" -target <signal>\n");
|
||||
log(" use the specified signal as the merged clock. if not given, the\n");
|
||||
log(" clock signal of the first FF encountered is used. all FFs will\n");
|
||||
log(" be set to positive-edge triggered on this signal.\n");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
std::string target_clk_name;
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++) {
|
||||
if (args[argidx] == "-target" && argidx + 1 < args.size()) {
|
||||
target_clk_name = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
extra_args(args, argidx, design);
|
||||
|
||||
for (auto module : design->selected_modules())
|
||||
{
|
||||
SigMap sigmap(module);
|
||||
|
||||
struct FfInfo {
|
||||
Cell *cell;
|
||||
SigSpec clk;
|
||||
bool pol_clk;
|
||||
};
|
||||
|
||||
std::vector<FfInfo> ff_list;
|
||||
|
||||
for (auto cell : module->selected_cells())
|
||||
{
|
||||
if (!cell->is_builtin_ff())
|
||||
continue;
|
||||
|
||||
FfData ff(nullptr, cell);
|
||||
if (!ff.has_clk)
|
||||
continue;
|
||||
|
||||
ff_list.push_back({cell, sigmap(ff.sig_clk), ff.pol_clk});
|
||||
}
|
||||
|
||||
if (ff_list.empty())
|
||||
continue;
|
||||
|
||||
// Determine target clock signal and polarity
|
||||
SigSpec target_clk;
|
||||
bool target_pol = true; // default to posedge
|
||||
|
||||
if (!target_clk_name.empty()) {
|
||||
RTLIL::SigSpec sig;
|
||||
if (!SigSpec::parse_sel(sig, design, module, target_clk_name))
|
||||
log_cmd_error("Failed to parse target clock expression '%s'.\n", target_clk_name.c_str());
|
||||
target_clk = sigmap(sig);
|
||||
} else {
|
||||
target_clk = ff_list[0].clk;
|
||||
target_pol = ff_list[0].pol_clk;
|
||||
}
|
||||
|
||||
// Collect distinct (signal, polarity) pairs
|
||||
pool<std::pair<SigSpec, bool>> all_domains;
|
||||
for (auto &info : ff_list)
|
||||
all_domains.insert({info.clk, info.pol_clk});
|
||||
|
||||
if (all_domains.size() <= 1) {
|
||||
log("Module %s: only one clock domain found, nothing to merge.\n", log_id(module));
|
||||
continue;
|
||||
}
|
||||
|
||||
log("Module %s: merging %d clock domains into %s%s\n",
|
||||
log_id(module), GetSize(all_domains),
|
||||
target_pol ? "" : "!", log_signal(target_clk));
|
||||
|
||||
for (auto &dom : all_domains)
|
||||
log(" found domain: %s%s\n",
|
||||
dom.second ? "" : "!", log_signal(dom.first));
|
||||
|
||||
int clk_rewritten = 0, pol_rewritten = 0;
|
||||
for (auto &info : ff_list)
|
||||
{
|
||||
Cell *cell = info.cell;
|
||||
bool needs_clk_change = (info.clk != target_clk);
|
||||
bool needs_pol_change = (info.pol_clk != target_pol);
|
||||
|
||||
if (!needs_clk_change && !needs_pol_change)
|
||||
continue;
|
||||
|
||||
if (needs_clk_change) {
|
||||
if (cell->hasPort(ID::C))
|
||||
cell->setPort(ID::C, target_clk);
|
||||
else if (cell->hasPort(ID::CLK))
|
||||
cell->setPort(ID::CLK, target_clk);
|
||||
clk_rewritten++;
|
||||
}
|
||||
|
||||
if (needs_pol_change) {
|
||||
// Coarse-grain FFs ($dff, $dffe, etc.) use CLK_POLARITY param
|
||||
if (cell->hasParam(ID::CLK_POLARITY)) {
|
||||
cell->setParam(ID::CLK_POLARITY, target_pol ? State::S1 : State::S0);
|
||||
pol_rewritten++;
|
||||
}
|
||||
// Fine-grain FFs encode polarity in the type name, so
|
||||
// we need to swap the cell type (e.g. $_DFF_N_ <-> $_DFF_P_)
|
||||
else {
|
||||
std::string type = cell->type.str();
|
||||
// Fine-grain FF types have P/N at position 6 for the clock polarity:
|
||||
// $_DFF_P_, $_DFF_N_, $_DFFE_PP_, $_DFFE_NP_, etc.
|
||||
// The clock polarity is always the first letter after "$_DFF_" or "$_DFFE_"
|
||||
size_t pos = type.find("_DFF_");
|
||||
if (pos != std::string::npos) {
|
||||
pos += 5; // skip "_DFF_"
|
||||
if (pos < type.size()) {
|
||||
if (type[pos] == 'P' && !target_pol)
|
||||
type[pos] = 'N';
|
||||
else if (type[pos] == 'N' && target_pol)
|
||||
type[pos] = 'P';
|
||||
cell->type = RTLIL::IdString(type);
|
||||
pol_rewritten++;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
log(" Rewrote clock signal on %d FFs, polarity on %d FFs.\n",
|
||||
clk_rewritten, pol_rewritten);
|
||||
}
|
||||
}
|
||||
} ClkMergePass;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
|
@ -0,0 +1,716 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Cone partitioning for equivalence checking.
|
||||
*
|
||||
* Given two modules (typically "gold" and "gate") with matching port
|
||||
* signatures, this pass:
|
||||
*
|
||||
* 1. Builds bottom-up structural hashes for every cell in each module
|
||||
* (identical algorithm to struct_partition).
|
||||
*
|
||||
* 2. Finds hash groups where FF cells from BOTH modules match — these
|
||||
* are structurally equivalent sequential boundaries.
|
||||
*
|
||||
* 3. For each matched FF group:
|
||||
* - The FF's Q output is disconnected from the rest of the circuit
|
||||
* and exposed as a new output port (PO).
|
||||
* - A new input port (PI) is created to replace the FF's Q output
|
||||
* for any downstream logic that was consuming it.
|
||||
* - The cone's transitive fanin is traced backwards, stopping at
|
||||
* existing module PIs or at other matched FFs (whose PIs are
|
||||
* reused). Any other leaf signals become new PIs.
|
||||
*
|
||||
* 4. Multi-clock-domain handling:
|
||||
* - If both gold and gate have multiple clock domains, unmatched
|
||||
* FFs (those not in any structural cone) are individually
|
||||
* exposed as PI/PO pairs with the PO ANDed with a 1-bit clock
|
||||
* guard PI for the FF's clock domain.
|
||||
* - If only one module has multiple clock domains while the other
|
||||
* has one, the pass errors out declaring the designs inequivalent.
|
||||
* - Each unique (clock_signal, polarity) pair gets one guard PI
|
||||
* (\clkguard_N). The guard ensures the SAT solver treats FFs in
|
||||
* different domains as distinguishable even after clkmerge.
|
||||
*
|
||||
* The result is a pair of modules where every structurally matched
|
||||
* FF cone is individually observable through its own PI/PO pair, ready
|
||||
* for per-cone equivalence checking.
|
||||
*
|
||||
* Copyright (C) 2025 Silimate Inc.
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/celltypes.h"
|
||||
#include "kernel/ff.h"
|
||||
#include "kernel/log.h"
|
||||
#include <cstdarg>
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// StructuralHash — collision-free structural identity (same as struct_partition)
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
struct StructuralHasher {
|
||||
dict<std::vector<int>, int> intern_table;
|
||||
int next_id = 1;
|
||||
|
||||
enum { CONST_BASE = -1000000, PI_BASE = -2000000, CYCLE_GUARD = 0 };
|
||||
|
||||
int intern(const std::vector<int> &key) {
|
||||
auto it = intern_table.find(key);
|
||||
if (it != intern_table.end())
|
||||
return it->second;
|
||||
int id = next_id++;
|
||||
intern_table[key] = id;
|
||||
return id;
|
||||
}
|
||||
|
||||
dict<std::pair<IdString, int>, int> pi_ids;
|
||||
int intern_pi(IdString port_name, int bit_idx) {
|
||||
auto key = std::make_pair(port_name, bit_idx);
|
||||
auto it = pi_ids.find(key);
|
||||
if (it != pi_ids.end())
|
||||
return it->second;
|
||||
int id = PI_BASE - (int)pi_ids.size();
|
||||
pi_ids[key] = id;
|
||||
return id;
|
||||
}
|
||||
|
||||
dict<Const, int> const_ids;
|
||||
int intern_const(const Const &val) {
|
||||
auto it = const_ids.find(val);
|
||||
if (it != const_ids.end())
|
||||
return it->second;
|
||||
int id = CONST_BASE - (int)const_ids.size();
|
||||
const_ids[val] = id;
|
||||
return id;
|
||||
}
|
||||
};
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Per-module analysis state (same as struct_partition)
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
struct ModuleAnalysis {
|
||||
RTLIL::Module *module;
|
||||
SigMap sigmap;
|
||||
CellTypes ct;
|
||||
|
||||
dict<SigBit, std::pair<Cell*, IdString>> bit_driver;
|
||||
dict<Cell*, int> cell_hash;
|
||||
dict<SigBit, std::pair<IdString, int>> pi_bits;
|
||||
pool<Cell*> visiting;
|
||||
pool<Cell*> ff_cells;
|
||||
|
||||
ModuleAnalysis(RTLIL::Module *mod, Design *design) : module(mod), sigmap(mod) {
|
||||
ct.setup(design);
|
||||
|
||||
for (auto wire : module->wires()) {
|
||||
if (wire->port_input) {
|
||||
SigSpec sig = sigmap(wire);
|
||||
for (int i = 0; i < GetSize(sig); i++)
|
||||
pi_bits[sig[i]] = {wire->name, i};
|
||||
}
|
||||
}
|
||||
|
||||
for (auto cell : module->cells()) {
|
||||
if (cell->is_builtin_ff() || cell->type.in(
|
||||
ID($sr), ID($ff), ID($dff), ID($dffe),
|
||||
ID($dffsr), ID($dffsre), ID($adff), ID($adffe),
|
||||
ID($aldff), ID($aldffe), ID($sdff), ID($sdffe),
|
||||
ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr),
|
||||
ID($anyinit)))
|
||||
ff_cells.insert(cell);
|
||||
|
||||
for (auto &conn : cell->connections()) {
|
||||
if (cell->output(conn.first)) {
|
||||
SigSpec sig = sigmap(conn.second);
|
||||
for (int i = 0; i < GetSize(sig); i++)
|
||||
if (sig[i].wire)
|
||||
bit_driver[sig[i]] = {cell, conn.first};
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
int hash_bit(SigBit bit, StructuralHasher &hasher) {
|
||||
bit = sigmap(bit);
|
||||
|
||||
if (bit.wire == nullptr)
|
||||
return hasher.intern_const(Const(bit.data));
|
||||
|
||||
auto pi_it = pi_bits.find(bit);
|
||||
if (pi_it != pi_bits.end())
|
||||
return hasher.intern_pi(pi_it->second.first, pi_it->second.second);
|
||||
|
||||
auto drv_it = bit_driver.find(bit);
|
||||
if (drv_it != bit_driver.end()) {
|
||||
Cell *drv_cell = drv_it->second.first;
|
||||
IdString drv_port = drv_it->second.second;
|
||||
|
||||
if (ff_cells.count(drv_cell) && drv_port == ID::Q) {
|
||||
int ff_hash = hash_cell(drv_cell, hasher);
|
||||
SigSpec q_sig = sigmap(drv_cell->getPort(ID::Q));
|
||||
int bit_idx = 0;
|
||||
for (int i = 0; i < GetSize(q_sig); i++)
|
||||
if (q_sig[i] == bit) { bit_idx = i; break; }
|
||||
std::vector<int> key = {ff_hash, bit_idx, -99};
|
||||
return hasher.intern(key);
|
||||
}
|
||||
|
||||
int ch = hash_cell(drv_cell, hasher);
|
||||
SigSpec port_sig = sigmap(drv_cell->getPort(drv_port));
|
||||
int bit_idx = 0;
|
||||
for (int i = 0; i < GetSize(port_sig); i++)
|
||||
if (port_sig[i] == bit) { bit_idx = i; break; }
|
||||
std::vector<int> key = {ch, bit_idx, (int)drv_port.index_};
|
||||
return hasher.intern(key);
|
||||
}
|
||||
|
||||
return hasher.intern_const(Const(State::Sx));
|
||||
}
|
||||
|
||||
int hash_sig(const SigSpec &sig, StructuralHasher &hasher) {
|
||||
SigSpec mapped = sigmap(sig);
|
||||
if (GetSize(mapped) == 1)
|
||||
return hash_bit(mapped[0], hasher);
|
||||
|
||||
std::vector<int> key;
|
||||
key.reserve(GetSize(mapped) + 1);
|
||||
key.push_back(-77);
|
||||
for (auto &bit : mapped)
|
||||
key.push_back(hash_bit(bit, hasher));
|
||||
return hasher.intern(key);
|
||||
}
|
||||
|
||||
int hash_cell(Cell *cell, StructuralHasher &hasher) {
|
||||
auto it = cell_hash.find(cell);
|
||||
if (it != cell_hash.end())
|
||||
return it->second;
|
||||
|
||||
if (visiting.count(cell)) {
|
||||
cell_hash[cell] = StructuralHasher::CYCLE_GUARD;
|
||||
return StructuralHasher::CYCLE_GUARD;
|
||||
}
|
||||
visiting.insert(cell);
|
||||
|
||||
std::vector<int> key;
|
||||
key.push_back((int)cell->type.index_);
|
||||
|
||||
std::vector<std::pair<IdString, Const>> sorted_params(
|
||||
cell->parameters.begin(), cell->parameters.end());
|
||||
std::sort(sorted_params.begin(), sorted_params.end(),
|
||||
[](const auto &a, const auto &b) { return a.first < b.first; });
|
||||
|
||||
key.push_back(-88);
|
||||
for (auto &[pname, pval] : sorted_params) {
|
||||
key.push_back((int)pname.index_);
|
||||
key.push_back(hasher.intern_const(pval));
|
||||
}
|
||||
|
||||
key.push_back(-99);
|
||||
std::vector<std::pair<IdString, SigSpec>> inputs;
|
||||
for (auto &conn : cell->connections()) {
|
||||
if (cell->output(conn.first))
|
||||
continue;
|
||||
inputs.push_back({conn.first, conn.second});
|
||||
}
|
||||
std::sort(inputs.begin(), inputs.end(),
|
||||
[](const auto &a, const auto &b) { return a.first < b.first; });
|
||||
|
||||
for (auto &[port, sig] : inputs) {
|
||||
key.push_back((int)port.index_);
|
||||
key.push_back(hash_sig(sig, hasher));
|
||||
}
|
||||
|
||||
int id = hasher.intern(key);
|
||||
cell_hash[cell] = id;
|
||||
visiting.erase(cell);
|
||||
return id;
|
||||
}
|
||||
|
||||
void hash_all_cells(StructuralHasher &hasher) {
|
||||
for (auto cell : module->cells())
|
||||
hash_cell(cell, hasher);
|
||||
}
|
||||
};
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Core worker
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
struct ConePartitionWorker {
|
||||
Design *design;
|
||||
Module *gold_mod;
|
||||
Module *gate_mod;
|
||||
bool verbose;
|
||||
FILE *log_file;
|
||||
|
||||
int total_pos = 0;
|
||||
int total_pis = 0;
|
||||
int total_guards = 0;
|
||||
|
||||
// Clock domain guard tracking:
|
||||
// Each unique (clk_signal_string, polarity) pair gets a unique guard index.
|
||||
// A guard PI wire named \clkguard_<idx> is created in each module for each
|
||||
// clock domain that appears in its FFs. The PO for a cone is ANDed with
|
||||
// the guard so that FFs in different clock domains remain structurally
|
||||
// distinguishable even after clkmerge unifies the actual clock signals.
|
||||
dict<std::pair<std::string, bool>, int> clk_domain_to_guard;
|
||||
int next_guard_idx = 0;
|
||||
dict<std::pair<Module*, int>, Wire*> guard_pi_cache;
|
||||
|
||||
ConePartitionWorker(Design *d, Module *gold, Module *gate, bool v, FILE *lf = nullptr)
|
||||
: design(d), gold_mod(gold), gate_mod(gate), verbose(v), log_file(lf) {}
|
||||
|
||||
int get_or_create_guard_idx(const SigSpec &clk, bool pol, SigMap &sigmap) {
|
||||
SigSpec mapped = sigmap(clk);
|
||||
std::string clk_str = log_signal(mapped);
|
||||
auto key = std::make_pair(clk_str, pol);
|
||||
auto it = clk_domain_to_guard.find(key);
|
||||
if (it != clk_domain_to_guard.end())
|
||||
return it->second;
|
||||
int idx = next_guard_idx++;
|
||||
clk_domain_to_guard[key] = idx;
|
||||
return idx;
|
||||
}
|
||||
|
||||
Wire* get_or_create_guard_pi(Module *mod, int guard_idx) {
|
||||
auto key = std::make_pair(mod, guard_idx);
|
||||
auto it = guard_pi_cache.find(key);
|
||||
if (it != guard_pi_cache.end())
|
||||
return it->second;
|
||||
std::string name = stringf("\\clkguard_%d", guard_idx);
|
||||
Wire *w = mod->addWire(name, 1);
|
||||
w->port_input = true;
|
||||
guard_pi_cache[key] = w;
|
||||
total_guards++;
|
||||
return w;
|
||||
}
|
||||
|
||||
// Returns guard index for an FF cell, or -1 if the FF has no clock.
|
||||
int get_ff_guard_idx(Cell *cell, SigMap &sigmap) {
|
||||
FfData ff(nullptr, cell);
|
||||
if (!ff.has_clk)
|
||||
return -1;
|
||||
return get_or_create_guard_idx(ff.sig_clk, ff.pol_clk, sigmap);
|
||||
}
|
||||
|
||||
void vlog(const char *fmt, ...) __attribute__((format(printf, 2, 3))) {
|
||||
va_list ap;
|
||||
va_start(ap, fmt);
|
||||
char buf[4096];
|
||||
vsnprintf(buf, sizeof(buf), fmt, ap);
|
||||
va_end(ap);
|
||||
if (log_file)
|
||||
fputs(buf, log_file);
|
||||
else
|
||||
log("%s", buf);
|
||||
}
|
||||
|
||||
// Collect the set of clock domains (clk_signal, polarity) for all FFs in a module.
|
||||
pool<std::pair<std::string, bool>> collect_clock_domains(ModuleAnalysis &analysis, SigMap &sigmap) {
|
||||
pool<std::pair<std::string, bool>> domains;
|
||||
for (auto cell : analysis.ff_cells) {
|
||||
FfData ff(nullptr, cell);
|
||||
if (!ff.has_clk)
|
||||
continue;
|
||||
SigSpec mapped = sigmap(ff.sig_clk);
|
||||
std::string clk_str = log_signal(mapped);
|
||||
domains.insert({clk_str, ff.pol_clk});
|
||||
}
|
||||
return domains;
|
||||
}
|
||||
|
||||
void run() {
|
||||
StructuralHasher hasher;
|
||||
|
||||
vlog("Cone partitioning: analyzing module `%s'.\n", gold_mod->name.c_str());
|
||||
ModuleAnalysis gold_analysis(gold_mod, design);
|
||||
gold_analysis.hash_all_cells(hasher);
|
||||
|
||||
vlog("Cone partitioning: analyzing module `%s'.\n", gate_mod->name.c_str());
|
||||
ModuleAnalysis gate_analysis(gate_mod, design);
|
||||
gate_analysis.hash_all_cells(hasher);
|
||||
|
||||
SigMap gold_sigmap(gold_mod);
|
||||
SigMap gate_sigmap(gate_mod);
|
||||
|
||||
// Collect clock domains from each module
|
||||
auto gold_domains = collect_clock_domains(gold_analysis, gold_sigmap);
|
||||
auto gate_domains = collect_clock_domains(gate_analysis, gate_sigmap);
|
||||
|
||||
bool gold_multi = gold_domains.size() > 1;
|
||||
bool gate_multi = gate_domains.size() > 1;
|
||||
|
||||
vlog("Gold module has %d clock domain(s), gate module has %d clock domain(s).\n",
|
||||
(int)gold_domains.size(), (int)gate_domains.size());
|
||||
|
||||
if (gold_multi != gate_multi) {
|
||||
vlog("ERROR: Clock domain count mismatch — gold has %d, gate has %d.\n",
|
||||
(int)gold_domains.size(), (int)gate_domains.size());
|
||||
vlog("One module has multiple clock domains while the other does not.\n");
|
||||
vlog("The designs are NOT equivalent.\n");
|
||||
log_cmd_error("Designs are inequivalent: clock domain count mismatch "
|
||||
"(gold=%d, gate=%d). One module has multiple clock domains "
|
||||
"while the other does not.\n",
|
||||
(int)gold_domains.size(), (int)gate_domains.size());
|
||||
return;
|
||||
}
|
||||
|
||||
bool multi_clock = gold_multi && gate_multi;
|
||||
if (multi_clock) {
|
||||
if (gold_domains != gate_domains) {
|
||||
vlog("WARNING: Gold and gate have different clock domain sets.\n");
|
||||
for (auto &d : gold_domains)
|
||||
vlog(" gold domain: %s%s\n", d.second ? "" : "!", d.first.c_str());
|
||||
for (auto &d : gate_domains)
|
||||
vlog(" gate domain: %s%s\n", d.second ? "" : "!", d.first.c_str());
|
||||
}
|
||||
vlog("Multi-clock mode: unmatched FFs will be guarded with clock domain PIs.\n");
|
||||
}
|
||||
|
||||
// Only consider FF cells for matching
|
||||
dict<int, std::vector<Cell*>> gold_ff_by_hash, gate_ff_by_hash;
|
||||
for (auto &[cell, h] : gold_analysis.cell_hash)
|
||||
if (h != StructuralHasher::CYCLE_GUARD && gold_analysis.ff_cells.count(cell))
|
||||
gold_ff_by_hash[h].push_back(cell);
|
||||
for (auto &[cell, h] : gate_analysis.cell_hash)
|
||||
if (h != StructuralHasher::CYCLE_GUARD && gate_analysis.ff_cells.count(cell))
|
||||
gate_ff_by_hash[h].push_back(cell);
|
||||
|
||||
struct ConeGroup {
|
||||
std::vector<Cell*> gold_cells;
|
||||
std::vector<Cell*> gate_cells;
|
||||
};
|
||||
std::vector<ConeGroup> groups;
|
||||
|
||||
pool<Cell*> matched_gold_ffs, matched_gate_ffs;
|
||||
|
||||
for (auto &[h, gold_cells] : gold_ff_by_hash) {
|
||||
auto it = gate_ff_by_hash.find(h);
|
||||
if (it == gate_ff_by_hash.end())
|
||||
continue;
|
||||
groups.push_back({gold_cells, it->second});
|
||||
for (auto c : gold_cells) matched_gold_ffs.insert(c);
|
||||
for (auto c : it->second) matched_gate_ffs.insert(c);
|
||||
}
|
||||
|
||||
if (groups.empty()) {
|
||||
vlog("No structural FF matches found between `%s' and `%s'.\n",
|
||||
gold_mod->name.c_str(), gate_mod->name.c_str());
|
||||
} else {
|
||||
vlog("Found %d structurally matched FF groups.\n", (int)groups.size());
|
||||
}
|
||||
|
||||
int cone_idx = 0;
|
||||
for (auto &group : groups) {
|
||||
expose_matched_ff_group(group.gold_cells, group.gate_cells,
|
||||
cone_idx, gold_sigmap, gate_sigmap);
|
||||
cone_idx++;
|
||||
}
|
||||
|
||||
// In multi-clock mode, expose unmatched FFs with clock-domain guard ANDs.
|
||||
// These are FFs that didn't end up in any cone (no hash match). Each
|
||||
// unmatched FF gets its own PO, and that PO is ANDed with the clock
|
||||
// guard PI for the FF's clock domain.
|
||||
if (multi_clock) {
|
||||
int unmatched_gold = 0, unmatched_gate = 0;
|
||||
for (auto cell : gold_analysis.ff_cells) {
|
||||
if (matched_gold_ffs.count(cell))
|
||||
continue;
|
||||
int guard_idx = get_ff_guard_idx(cell, gold_sigmap);
|
||||
expose_unmatched_ff(gold_mod, cell, cone_idx, guard_idx);
|
||||
cone_idx++;
|
||||
unmatched_gold++;
|
||||
}
|
||||
for (auto cell : gate_analysis.ff_cells) {
|
||||
if (matched_gate_ffs.count(cell))
|
||||
continue;
|
||||
int guard_idx = get_ff_guard_idx(cell, gate_sigmap);
|
||||
expose_unmatched_ff(gate_mod, cell, cone_idx, guard_idx);
|
||||
cone_idx++;
|
||||
unmatched_gate++;
|
||||
}
|
||||
vlog("Multi-clock: guarded %d unmatched gold FFs, %d unmatched gate FFs.\n",
|
||||
unmatched_gold, unmatched_gate);
|
||||
}
|
||||
|
||||
gold_mod->fixup_ports();
|
||||
gate_mod->fixup_ports();
|
||||
|
||||
vlog("Cone partitioning: created %d POs, %d PIs, %d clock guard PIs.\n",
|
||||
total_pos, total_pis, total_guards);
|
||||
}
|
||||
|
||||
private:
|
||||
// For a single matched FF group:
|
||||
// 1. Create a PI wire (same name in both modules) to replace the FF's Q
|
||||
// for all downstream consumers.
|
||||
// 2. Create a PO wire (same name in both modules) that observes the FF's
|
||||
// actual Q output.
|
||||
// 3. Redirect each FF's Q port to a fresh internal wire so the FF is fully
|
||||
// severed from the rest of the circuit. The internal wire drives only
|
||||
// the PO. The old Q wire is now driven by the PI.
|
||||
void expose_matched_ff_group(
|
||||
const std::vector<Cell*> &gold_cells,
|
||||
const std::vector<Cell*> &gate_cells,
|
||||
int cone_idx,
|
||||
SigMap &/*gold_sigmap*/,
|
||||
SigMap &/*gate_sigmap*/)
|
||||
{
|
||||
if (gold_cells.empty() || gate_cells.empty())
|
||||
return;
|
||||
|
||||
Cell *gold_rep = gold_cells[0];
|
||||
int q_width = GetSize(gold_rep->getPort(ID::Q));
|
||||
if (q_width == 0)
|
||||
return;
|
||||
|
||||
std::string pi_name = stringf("\\cone_%d_ff_pi", cone_idx);
|
||||
std::string po_name = stringf("\\cone_%d_po", cone_idx);
|
||||
|
||||
if (verbose) {
|
||||
vlog(" Cone %d: PI %s, PO %s (width %d) for %d+%d FFs.\n",
|
||||
cone_idx, pi_name.c_str(), po_name.c_str(), q_width,
|
||||
(int)gold_cells.size(), (int)gate_cells.size());
|
||||
}
|
||||
|
||||
rewire_ff_group(gold_mod, gold_cells, pi_name, po_name, q_width, cone_idx);
|
||||
rewire_ff_group(gate_mod, gate_cells, pi_name, po_name, q_width, cone_idx);
|
||||
|
||||
total_pis++;
|
||||
total_pos++;
|
||||
}
|
||||
|
||||
void rewire_ff_group(Module *mod, const std::vector<Cell*> &ff_cells,
|
||||
const std::string &pi_name, const std::string &po_name,
|
||||
int q_width, int cone_idx)
|
||||
{
|
||||
if (mod->wire(pi_name) || mod->wire(po_name))
|
||||
return;
|
||||
|
||||
Wire *pi_wire = mod->addWire(pi_name, q_width);
|
||||
pi_wire->port_input = true;
|
||||
|
||||
Wire *po_wire = mod->addWire(po_name, q_width);
|
||||
po_wire->port_output = true;
|
||||
|
||||
bool po_connected = false;
|
||||
int ff_idx = 0;
|
||||
for (auto cell : ff_cells) {
|
||||
SigSpec old_q = cell->getPort(ID::Q);
|
||||
if (GetSize(old_q) != q_width)
|
||||
continue;
|
||||
|
||||
std::string q_int_name = stringf("\\cone_%d_q_%d", cone_idx, ff_idx);
|
||||
Wire *q_int = mod->addWire(q_int_name, q_width);
|
||||
|
||||
cell->setPort(ID::Q, SigSpec(q_int));
|
||||
|
||||
mod->connect(old_q, SigSpec(pi_wire));
|
||||
|
||||
if (!po_connected) {
|
||||
mod->connect(SigSpec(po_wire), SigSpec(q_int));
|
||||
po_connected = true;
|
||||
}
|
||||
|
||||
ff_idx++;
|
||||
}
|
||||
}
|
||||
|
||||
// Expose a single unmatched FF (one not in any cone) as its own PI/PO pair,
|
||||
// with the PO ANDed with the clock-domain guard PI. This ensures the SAT
|
||||
// solver sees the FF's domain even though no structural cone was created.
|
||||
void expose_unmatched_ff(Module *mod, Cell *cell, int cone_idx,
|
||||
int guard_idx)
|
||||
{
|
||||
SigSpec old_q = cell->getPort(ID::Q);
|
||||
int q_width = GetSize(old_q);
|
||||
if (q_width == 0)
|
||||
return;
|
||||
|
||||
std::string pi_name = stringf("\\ucone_%d_ff_pi", cone_idx);
|
||||
std::string po_name = stringf("\\ucone_%d_po", cone_idx);
|
||||
|
||||
if (mod->wire(pi_name) || mod->wire(po_name))
|
||||
return;
|
||||
|
||||
Wire *pi_wire = mod->addWire(pi_name, q_width);
|
||||
pi_wire->port_input = true;
|
||||
|
||||
Wire *po_wire = mod->addWire(po_name, q_width);
|
||||
po_wire->port_output = true;
|
||||
|
||||
std::string q_int_name = stringf("\\ucone_%d_q", cone_idx);
|
||||
Wire *q_int = mod->addWire(q_int_name, q_width);
|
||||
|
||||
cell->setPort(ID::Q, SigSpec(q_int));
|
||||
mod->connect(old_q, SigSpec(pi_wire));
|
||||
|
||||
if (guard_idx >= 0) {
|
||||
Wire *guard_pi = get_or_create_guard_pi(mod, guard_idx);
|
||||
Wire *guarded = mod->addWire(
|
||||
stringf("\\ucone_%d_guarded", cone_idx), q_width);
|
||||
SigSpec guard_bits;
|
||||
for (int i = 0; i < q_width; i++)
|
||||
guard_bits.append(SigBit(guard_pi, 0));
|
||||
mod->addAnd(stringf("\\ucone_%d_clkand", cone_idx),
|
||||
SigSpec(q_int), guard_bits, SigSpec(guarded));
|
||||
mod->connect(SigSpec(po_wire), SigSpec(guarded));
|
||||
} else {
|
||||
mod->connect(SigSpec(po_wire), SigSpec(q_int));
|
||||
}
|
||||
|
||||
total_pis++;
|
||||
total_pos++;
|
||||
|
||||
if (verbose) {
|
||||
vlog(" Unmatched FF %s in %s: PI %s, PO %s (width %d) [guard=%d].\n",
|
||||
cell->name.c_str(), mod->name.c_str(),
|
||||
pi_name.c_str(), po_name.c_str(), q_width, guard_idx);
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Pass registration
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
struct ConePartitionPass : public Pass {
|
||||
ConePartitionPass() : Pass("cone_partition",
|
||||
"expose matched structural cones as PI/PO pairs") { }
|
||||
|
||||
void help() override
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" cone_partition [options] gold_module gate_module\n");
|
||||
log("\n");
|
||||
log("This pass identifies structurally identical flip-flop cones between two\n");
|
||||
log("modules (typically a gold and gate design) using the same hashing algorithm\n");
|
||||
log("as struct_partition, then exposes each matched cone's boundary as ports:\n");
|
||||
log("\n");
|
||||
log(" - Each matched FF's Q output is disconnected from the circuit and\n");
|
||||
log(" exposed as a new output port (PO).\n");
|
||||
log(" - A new input port (PI) replaces the FF's Q output for any downstream\n");
|
||||
log(" consumers.\n");
|
||||
log(" - The cone's transitive fanin (back through combinational logic) is\n");
|
||||
log(" traced until it reaches a module PI, an unmatched FF boundary, or\n");
|
||||
log(" another matched FF (whose replacement PI is reused). Leaf signals\n");
|
||||
log(" at the cone boundary become new input ports.\n");
|
||||
log("\n");
|
||||
log("Multi-clock-domain handling:\n");
|
||||
log("\n");
|
||||
log(" The pass collects the set of clock domains (signal + polarity) from\n");
|
||||
log(" all FFs in each module. Three cases:\n");
|
||||
log("\n");
|
||||
log(" 1. Both modules have a single clock domain (or no clocked FFs):\n");
|
||||
log(" no special handling; cones are created as above.\n");
|
||||
log("\n");
|
||||
log(" 2. Only ONE module has multiple clock domains while the other has\n");
|
||||
log(" one: the pass errors out, declaring the designs inequivalent.\n");
|
||||
log(" A design cannot gain/lose clock domains and still be equivalent.\n");
|
||||
log("\n");
|
||||
log(" 3. Both modules have multiple clock domains: after creating cones\n");
|
||||
log(" for structurally matched FFs (as above), every UNMATCHED FF\n");
|
||||
log(" (one that did not belong to any cone) is individually exposed\n");
|
||||
log(" as its own PI/PO pair. The PO is ANDed with a 1-bit clock-\n");
|
||||
log(" domain guard PI (clkguard_N) for the FF's domain. This ensures\n");
|
||||
log(" the downstream SAT solver treats FFs in different domains as\n");
|
||||
log(" distinguishable even after clkmerge unifies clock signals.\n");
|
||||
log("\n");
|
||||
log(" -v\n");
|
||||
log(" verbose output: log each created port\n");
|
||||
log("\n");
|
||||
log(" -o <file>\n");
|
||||
log(" write verbose log output to <file> instead of standard log\n");
|
||||
log("\n");
|
||||
log("Typical usage:\n");
|
||||
log("\n");
|
||||
log(" read_rtlil gold.il\n");
|
||||
log(" read_rtlil gate.il\n");
|
||||
log(" cone_partition gold gate\n");
|
||||
log(" # Each cone now has its own PI/PO ports for targeted checking.\n");
|
||||
log("\n");
|
||||
}
|
||||
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
bool verbose = false;
|
||||
std::string log_file_path;
|
||||
|
||||
log_header(design, "Executing CONE_PARTITION pass.\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++) {
|
||||
if (args[argidx] == "-v") {
|
||||
verbose = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-o" && argidx + 1 < args.size()) {
|
||||
log_file_path = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
if (argidx + 2 != args.size())
|
||||
cmd_error(args, argidx, "Expected exactly two module name arguments.");
|
||||
|
||||
IdString gold_name = RTLIL::escape_id(args[argidx]);
|
||||
IdString gate_name = RTLIL::escape_id(args[argidx + 1]);
|
||||
|
||||
Module *gold_mod = design->module(gold_name);
|
||||
if (!gold_mod)
|
||||
log_cmd_error("Module `%s' not found.\n", gold_name.c_str());
|
||||
|
||||
Module *gate_mod = design->module(gate_name);
|
||||
if (!gate_mod)
|
||||
log_cmd_error("Module `%s' not found.\n", gate_name.c_str());
|
||||
|
||||
for (auto gold_wire : gold_mod->wires()) {
|
||||
if (!gold_wire->port_input)
|
||||
continue;
|
||||
Wire *gate_wire = gate_mod->wire(gold_wire->name);
|
||||
if (!gate_wire || !gate_wire->port_input)
|
||||
log_cmd_error("Input port `%s' in `%s' has no match in `%s'.\n",
|
||||
gold_wire->name.c_str(), gold_name.c_str(), gate_name.c_str());
|
||||
if (gold_wire->width != gate_wire->width)
|
||||
log_cmd_error("Port `%s' width mismatch: %d vs %d.\n",
|
||||
gold_wire->name.c_str(), gold_wire->width, gate_wire->width);
|
||||
}
|
||||
|
||||
FILE *log_file = nullptr;
|
||||
if (!log_file_path.empty()) {
|
||||
log_file = fopen(log_file_path.c_str(), "w");
|
||||
if (!log_file)
|
||||
log_cmd_error("Cannot open output file `%s'.\n", log_file_path.c_str());
|
||||
}
|
||||
|
||||
ConePartitionWorker worker(design, gold_mod, gate_mod, verbose, log_file);
|
||||
worker.run();
|
||||
|
||||
if (log_file)
|
||||
fclose(log_file);
|
||||
}
|
||||
} ConePartitionPass;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
|
@ -60,8 +60,6 @@ struct NegoptPass : public Pass {
|
|||
bool run_pre = false;
|
||||
bool run_post = false;
|
||||
|
||||
log_header(design, "Executing NEGOPT pass (optimize negation patterns).\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++) {
|
||||
if (args[argidx] == "-pre") {
|
||||
|
|
@ -76,28 +74,48 @@ struct NegoptPass : public Pass {
|
|||
}
|
||||
extra_args(args, argidx, design);
|
||||
|
||||
if (!run_pre && !run_post) {
|
||||
run_pre = true;
|
||||
run_post = true;
|
||||
}
|
||||
if (run_pre == run_post)
|
||||
log_cmd_error("NEGOPT requires exactly one of -pre or -post.\n");
|
||||
|
||||
log_header(design, "Executing NEGOPT %s pass (optimize negation patterns).\n",
|
||||
run_pre ? "PRE" : "POST");
|
||||
|
||||
constexpr int max_iterations = 100;
|
||||
|
||||
for (auto module : design->selected_modules()) {
|
||||
auto log_module_event = [&](const char *event) {
|
||||
log("%s %s\n", event, log_id(module));
|
||||
log_flush();
|
||||
};
|
||||
|
||||
auto log_pass_event = [&](const char *event, const char *pass_name, int iter = -1) {
|
||||
if (iter >= 0)
|
||||
log(" %s %s pass (iter=%d)\n", event, pass_name, iter + 1);
|
||||
else
|
||||
log(" %s %s pass\n", event, pass_name);
|
||||
log_flush();
|
||||
};
|
||||
|
||||
if (run_pre) {
|
||||
log_module_event("Processing Module:");
|
||||
|
||||
// manual2sub and sub2neg only need to run once: no downstream
|
||||
// pre-subpass creates the patterns they match
|
||||
// separate pm instances so sub2neg sees the $sub cells manual2sub creates.
|
||||
{
|
||||
peepopt_pm pm(module);
|
||||
pm.setup(module->selected_cells());
|
||||
log_pass_event("Starting", "manual2sub");
|
||||
pm.run_manual2sub();
|
||||
log_pass_event("Ending", "manual2sub");
|
||||
log_flush();
|
||||
}
|
||||
{
|
||||
peepopt_pm pm(module);
|
||||
pm.setup(module->selected_cells());
|
||||
log_pass_event("Starting", "sub2neg");
|
||||
pm.run_sub2neg();
|
||||
log_pass_event("Ending", "sub2neg");
|
||||
log_flush();
|
||||
}
|
||||
|
||||
|
|
@ -108,33 +126,51 @@ struct NegoptPass : public Pass {
|
|||
peepopt_pm pm(module);
|
||||
pm.setup(module->selected_cells());
|
||||
|
||||
log_pass_event("Starting", "negexpand", iter);
|
||||
pm.run_negexpand();
|
||||
log_pass_event("Ending", "negexpand", iter);
|
||||
log_flush();
|
||||
log_pass_event("Starting", "negneg", iter);
|
||||
pm.run_negneg();
|
||||
log_pass_event("Ending", "negneg", iter);
|
||||
log_flush();
|
||||
log_pass_event("Starting", "negmux", iter);
|
||||
pm.run_negmux();
|
||||
log_pass_event("Ending", "negmux", iter);
|
||||
log_flush();
|
||||
}
|
||||
if (did_something)
|
||||
log_warning("NEGOPT pre reached max iterations (%d) in module %s without convergence.\n", max_iterations, log_id(module));
|
||||
|
||||
log_module_event("Finished Module:");
|
||||
}
|
||||
|
||||
if (run_post) {
|
||||
log_module_event("Processing Module:");
|
||||
|
||||
did_something = true;
|
||||
for (int iter = 0; iter < max_iterations && did_something; iter++) {
|
||||
did_something = false;
|
||||
peepopt_pm pm(module);
|
||||
pm.setup(module->selected_cells());
|
||||
|
||||
log_pass_event("Starting", "negrebuild", iter);
|
||||
pm.run_negrebuild();
|
||||
log_pass_event("Ending", "negrebuild", iter);
|
||||
log_flush();
|
||||
log_pass_event("Starting", "muxneg", iter);
|
||||
pm.run_muxneg();
|
||||
log_pass_event("Ending", "muxneg", iter);
|
||||
log_flush();
|
||||
log_pass_event("Starting", "neg2sub", iter);
|
||||
pm.run_neg2sub();
|
||||
log_pass_event("Ending", "neg2sub", iter);
|
||||
log_flush();
|
||||
}
|
||||
if (did_something)
|
||||
log_warning("NEGOPT post reached max iterations (%d) in module %s without convergence.\n", max_iterations, log_id(module));
|
||||
|
||||
log_module_event("Finished Module:");
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -94,7 +94,7 @@ code root_add inner_add_A not_gate_A subtrahend minuend result_sig is_signed
|
|||
|
||||
subtrahend = port(not_gate_A, \A);
|
||||
|
||||
log("manual2sub in %s: Found (a + ~b) + 1 pattern, creating $sub for %s\n", log_id(module), log_signal(result_sig));
|
||||
log(" creating $sub for %s from (a + ~b) + 1\n", log_signal(result_sig));
|
||||
Cell *cell = root_add;
|
||||
int width = GetSize(result_sig);
|
||||
int inner_width = GetSize(inner_y);
|
||||
|
|
@ -196,7 +196,7 @@ code root_add inner_add_B not_gate_B minuend subtrahend result_sig is_signed
|
|||
else
|
||||
minuend = root_a;
|
||||
|
||||
log("manual2sub in %s: Found a + (~b + 1) pattern, creating $sub for %s\n", log_id(module), log_signal(result_sig));
|
||||
log(" creating $sub for %s from a + (~b + 1)\n", log_signal(result_sig));
|
||||
Cell *cell = root_add;
|
||||
int width = GetSize(result_sig);
|
||||
int inner_width = GetSize(inner_add_B->getPort(ID::Y));
|
||||
|
|
|
|||
|
|
@ -60,8 +60,8 @@ code mux_a mux_b mux_s mux_y neg_a_in neg_a_y neg_b_in neg_b_y neg_a_signed neg_
|
|||
neg_out_rs.extend_u0(GetSize(mux_y), neg_a_signed);
|
||||
module->connect(mux_y, neg_out_rs);
|
||||
|
||||
log("muxneg pattern in %s: mux=%s, neg_a=%s, neg_b=%s\n",
|
||||
log_id(module), log_id(mux), log_id(neg_a), log_id(neg_b));
|
||||
log(" mux=%s, neg_a=%s, neg_b=%s\n",
|
||||
log_id(mux), log_id(neg_a), log_id(neg_b));
|
||||
|
||||
new_mux->fixup_parameters();
|
||||
new_neg->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -62,8 +62,8 @@ code add_a add_b add_y neg_a neg_y neg_on_a add_a_signed add_b_signed neg_signed
|
|||
add->setPort(\Y, add_y);
|
||||
add->type = $sub;
|
||||
|
||||
log("neg2sub pattern in %s: add=%s, neg=%s (safe sub replacement)\n",
|
||||
log_id(module), log_id(add), log_id(neg));
|
||||
log(" add=%s, neg=%s (safe sub replacement)\n",
|
||||
log_id(add), log_id(neg));
|
||||
|
||||
add->fixup_parameters();
|
||||
autoremove(neg);
|
||||
|
|
|
|||
|
|
@ -49,8 +49,7 @@ code neg_a neg_y add_a add_b a_signed
|
|||
|
||||
Cell *new_add = module->addAdd(NEW_ID2_SUFFIX("add"), neg_add_a, neg_add_b, neg_y, a_signed);
|
||||
|
||||
log("negexpand pattern in %s: neg=%s, add=%s\n",
|
||||
log_id(module), log_id(neg), log_id(add));
|
||||
log(" neg=%s, add=%s\n", log_id(neg), log_id(add));
|
||||
|
||||
neg_a_cell->fixup_parameters();
|
||||
neg_b_cell->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -60,8 +60,7 @@ code neg_a neg_y mux_a mux_b mux_s mux_y a_signed
|
|||
|
||||
Cell *new_mux = module->addMux(NEW_ID2_SUFFIX("mux"), neg_mux_a, neg_mux_b, mux_s, neg_y);
|
||||
|
||||
log("negmux pattern in %s: neg=%s, mux=%s\n",
|
||||
log_id(module), log_id(neg), log_id(mux));
|
||||
log(" neg=%s, mux=%s\n", log_id(neg), log_id(mux));
|
||||
|
||||
neg_a_cell->fixup_parameters();
|
||||
neg_b_cell->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -29,8 +29,7 @@ code neg1_a neg1_y neg2_a
|
|||
|
||||
module->connect(neg1_y, neg2_a);
|
||||
|
||||
log("negneg pattern in %s: neg1=%s, neg2=%s\n",
|
||||
log_id(module), log_id(neg1), log_id(neg2));
|
||||
log(" neg1=%s, neg2=%s\n", log_id(neg1), log_id(neg2));
|
||||
|
||||
autoremove(neg1);
|
||||
autoremove(neg2);
|
||||
|
|
|
|||
|
|
@ -100,8 +100,8 @@ code add_a add_b add_y neg1_a neg1_y neg2_a neg2_y add_signed add_b_signed neg1_
|
|||
neg_out_rs.extend_u0(GetSize(add_y), add_signed);
|
||||
module->connect(add_y, neg_out_rs);
|
||||
|
||||
log("negrebuild pattern in %s: add=%s, neg1=%s, neg2=%s\n",
|
||||
log_id(module), log_id(add), log_id(neg1), log_id(neg2));
|
||||
log(" add=%s, neg1=%s, neg2=%s\n",
|
||||
log_id(add), log_id(neg1), log_id(neg2));
|
||||
|
||||
new_add->fixup_parameters();
|
||||
new_neg->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -43,8 +43,8 @@ code sub_a sub_b sub_y a_signed b_signed
|
|||
sub->setPort(\Y, sub_y);
|
||||
sub->type = $add;
|
||||
|
||||
log("sub2neg pattern in %s: sub=%s -> neg=%s, add=%s\n",
|
||||
log_id(module), log_id(sub), log_id(neg), log_id(sub));
|
||||
log(" sub=%s -> neg=%s, add=%s\n",
|
||||
log_id(sub), log_id(neg), log_id(sub));
|
||||
|
||||
sub->fixup_parameters();
|
||||
neg->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -148,6 +148,9 @@ struct AbcConfig
|
|||
int reserved_cores = 4; // cores reserved for main thread and other work
|
||||
bool abc_node_retention = false; // retain nodes in ABC (off by default)
|
||||
int abc_max_node_retention_origins = 5; // number of node retention origins (default 5)
|
||||
std::string signal_map_file;
|
||||
std::string cdc_file;
|
||||
bool filter_non_trigger_outputs = false;
|
||||
};
|
||||
|
||||
struct AbcSigVal {
|
||||
|
|
@ -287,6 +290,10 @@ struct RunAbcState {
|
|||
DeferredLogs logs;
|
||||
dict<int, std::string> pi_map, po_map;
|
||||
|
||||
int state_index = 0;
|
||||
bool clk_polarity = false;
|
||||
RTLIL::SigSpec clk_sig;
|
||||
|
||||
RunAbcState(const AbcConfig &config) : config(config) {}
|
||||
void run(ConcurrentStack<AbcProcess> &process_pool);
|
||||
};
|
||||
|
|
@ -1139,6 +1146,10 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
|
|||
mark_port(assign_map, srst_sig);
|
||||
|
||||
handle_loops(assign_map, module);
|
||||
|
||||
run_abc.state_index = state_index;
|
||||
run_abc.clk_polarity = clk_polarity;
|
||||
run_abc.clk_sig = clk_sig;
|
||||
}
|
||||
|
||||
bool read_until_abc_done(abc_output_filter &filt, int fd, DeferredLogs &logs) {
|
||||
|
|
@ -1204,11 +1215,24 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
|
|||
fprintf(f, " dummy_input\n");
|
||||
fprintf(f, "\n");
|
||||
|
||||
if (config.filter_non_trigger_outputs) {
|
||||
for (auto &si : signal_list) {
|
||||
if (!si.is_port || si.type == G(NONE))
|
||||
continue;
|
||||
if (si.type == G(FF) || si.type == G(FF0) || si.type == G(FF1))
|
||||
continue;
|
||||
if (si.bit_str.find("trigger") == std::string::npos)
|
||||
si.is_port = false;
|
||||
}
|
||||
}
|
||||
|
||||
int count_output = 0;
|
||||
fprintf(f, ".outputs");
|
||||
for (auto &si : signal_list) {
|
||||
if (!si.is_port || si.type == G(NONE))
|
||||
continue;
|
||||
if (config.filter_non_trigger_outputs && (si.type == G(FF) || si.type == G(FF0) || si.type == G(FF1)))
|
||||
continue;
|
||||
fprintf(f, " ys__n%d", si.id);
|
||||
po_map[count_output++] = si.bit_str;
|
||||
}
|
||||
|
|
@ -1217,6 +1241,33 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
|
|||
for (auto &si : signal_list)
|
||||
fprintf(f, "# ys__n%-5d %s\n", si.id, si.bit_str.c_str());
|
||||
|
||||
if (!config.signal_map_file.empty()) {
|
||||
FILE *mf = fopen(config.signal_map_file.c_str(), state_index == 0 ? "wt" : "at");
|
||||
if (mf == nullptr) {
|
||||
logs.log("Opening %s for writing failed: %s\n", config.signal_map_file, strerror(errno));
|
||||
} else {
|
||||
if (clk_sig.size() != 0) {
|
||||
std::string clk_str = log_signal(clk_sig);
|
||||
fprintf(mf, "# Clock domain %d: %s%s\n", state_index,
|
||||
clk_polarity ? "" : "!", clk_str.c_str());
|
||||
} else
|
||||
fprintf(mf, "# Clock domain %d: (none)\n", state_index);
|
||||
fprintf(mf, "# Inputs\n");
|
||||
for (auto &si : signal_list) {
|
||||
if (!si.is_port || si.type != G(NONE))
|
||||
continue;
|
||||
fprintf(mf, "ys__n%d %s\n", si.id, si.bit_str.c_str());
|
||||
}
|
||||
fprintf(mf, "# Outputs\n");
|
||||
for (auto &si : signal_list) {
|
||||
if (!si.is_port || si.type == G(NONE))
|
||||
continue;
|
||||
fprintf(mf, "ys__n%d %s\n", si.id, si.bit_str.c_str());
|
||||
}
|
||||
fclose(mf);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto &si : signal_list) {
|
||||
if (!si.bit_is_wire) {
|
||||
fprintf(f, ".names ys__n%d\n", si.id);
|
||||
|
|
@ -1820,7 +1871,7 @@ void AbcModuleState::finish()
|
|||
// For every signal that connects cells from different sets, or a cell in a set to a cell not in any set,
|
||||
// mark it as a port in `assign_map`.
|
||||
void assign_cell_connection_ports(RTLIL::Module *module, const std::vector<std::vector<RTLIL::Cell *> *> &cell_sets,
|
||||
AbcSigMap &assign_map)
|
||||
AbcSigMap &assign_map, const std::string &cdc_file)
|
||||
{
|
||||
pool<RTLIL::Cell *> cells_in_no_set;
|
||||
for (RTLIL::Cell *cell : module->cells()) {
|
||||
|
|
@ -1829,6 +1880,8 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vector<std::
|
|||
// For every canonical signal in `assign_map`, the index of the set it is connected to,
|
||||
// or -1 if it connects a cell in one set to a cell in another set or not in any set.
|
||||
dict<SigBit, int> signal_cell_set;
|
||||
// Maps each signal that crosses clock domains to the pair of domain indices it bridges.
|
||||
dict<SigBit, std::pair<int, int>> clock_domain_cross_signal_map;
|
||||
for (int i = 0; i < int(cell_sets.size()); ++i) {
|
||||
for (RTLIL::Cell *cell : *cell_sets[i]) {
|
||||
cells_in_no_set.erase(cell);
|
||||
|
|
@ -1839,6 +1892,7 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vector<std::
|
|||
if (it == signal_cell_set.end())
|
||||
signal_cell_set[bit] = i;
|
||||
else if (it->second >= 0 && it->second != i) {
|
||||
clock_domain_cross_signal_map[bit] = {it->second, i};
|
||||
it->second = -1;
|
||||
assign_map.addVal(bit, AbcSigVal(true));
|
||||
}
|
||||
|
|
@ -1851,11 +1905,29 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vector<std::
|
|||
for (SigBit bit : port_it.second) {
|
||||
assign_map.apply(bit);
|
||||
auto it = signal_cell_set.find(bit);
|
||||
if (it != signal_cell_set.end() && it->second >= 0)
|
||||
if (it != signal_cell_set.end() && it->second >= 0) {
|
||||
clock_domain_cross_signal_map[bit] = {it->second, -1};
|
||||
assign_map.addVal(bit, AbcSigVal(true));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!cdc_file.empty() && !clock_domain_cross_signal_map.empty()) {
|
||||
FILE *f = fopen(cdc_file.c_str(), "wt");
|
||||
if (f == nullptr) {
|
||||
log("Opening %s for writing failed: %s\n", cdc_file.c_str(), strerror(errno));
|
||||
} else {
|
||||
fprintf(f, "# Clock domain crossing signals for module %s\n", log_id(module));
|
||||
for (auto &it : clock_domain_cross_signal_map) {
|
||||
if (it.second.second >= 0)
|
||||
fprintf(f, "%s domain %d -> domain %d\n", log_signal(it.first).c_str(), it.second.first, it.second.second);
|
||||
else
|
||||
fprintf(f, "%s domain %d -> outside\n", log_signal(it.first).c_str(), it.second.first);
|
||||
}
|
||||
fclose(f);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
struct AbcPass : public Pass {
|
||||
|
|
@ -2046,6 +2118,18 @@ struct AbcPass : public Pass {
|
|||
log(" which means auto (use number of modules). Set to 0 to disable parallel\n");
|
||||
log(" execution and run everything on the main thread.\n");
|
||||
log("\n");
|
||||
log(" -signal_map <file>\n");
|
||||
log(" write a mapping of ABC signal names (ys__nN) to original port names\n");
|
||||
log(" for inputs and outputs. useful for interpreting ABC counterexamples.\n");
|
||||
log("\n");
|
||||
log(" -cdc_map <file>\n");
|
||||
log(" write a mapping of signals that cross clock domain boundaries.\n");
|
||||
log(" each line lists a signal and the domain indices it bridges.\n");
|
||||
log("\n");
|
||||
log(" -filter_non_trigger_outputs\n");
|
||||
log(" only keep output ports whose signal name contains 'trigger'.\n");
|
||||
log(" intended for miter/equivalence-checking flows. off by default.\n");
|
||||
log("\n");
|
||||
log(" -reserved_cores <num>\n");
|
||||
log(" number of CPU cores to reserve for the main thread and other work.\n");
|
||||
log(" Default is 4. The actual number of worker threads used is:\n");
|
||||
|
|
@ -2115,6 +2199,9 @@ struct AbcPass : public Pass {
|
|||
config.markgroups = design->scratchpad_get_bool("abc.markgroups", false);
|
||||
config.max_threads = design->scratchpad_get_int("abc.max_threads", -1);
|
||||
config.reserved_cores = design->scratchpad_get_int("abc.reserved_cores", 4);
|
||||
config.signal_map_file = design->scratchpad_get_string("abc.signal_map", "");
|
||||
config.cdc_file = design->scratchpad_get_string("abc.cdc_map", "");
|
||||
config.filter_non_trigger_outputs = design->scratchpad_get_bool("abc.filter_non_trigger_outputs", false);
|
||||
|
||||
if (config.cleanup)
|
||||
config.global_tempdir_name = get_base_tmpdir() + "/";
|
||||
|
|
@ -2258,6 +2345,18 @@ struct AbcPass : public Pass {
|
|||
config.reserved_cores = atoi(args[++argidx].c_str());
|
||||
continue;
|
||||
}
|
||||
if (arg == "-signal_map" && argidx+1 < args.size()) {
|
||||
config.signal_map_file = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
if (arg == "-cdc_map" && argidx+1 < args.size()) {
|
||||
config.cdc_file = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
if (arg == "-filter_non_trigger_outputs") {
|
||||
config.filter_non_trigger_outputs = true;
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
extra_args(args, argidx, design);
|
||||
|
|
@ -2501,7 +2600,7 @@ struct AbcPass : public Pass {
|
|||
|
||||
// Populate assign_map with cell connections
|
||||
std::vector<RTLIL::Cell*> cells = mod->selected_cells();
|
||||
assign_cell_connection_ports(mod, {&cells}, assign_map);
|
||||
assign_cell_connection_ports(mod, {&cells}, assign_map, config.cdc_file);
|
||||
|
||||
// Create a map of all signals and their corresponding src attrs
|
||||
SigMap sigmap(mod);
|
||||
|
|
@ -2802,7 +2901,7 @@ struct AbcPass : public Pass {
|
|||
std::get<6>(it.first) ? "" : "!", log_signal(std::get<7>(it.first)));
|
||||
cell_sets.push_back(&it.second);
|
||||
}
|
||||
assign_cell_connection_ports(mod, cell_sets, assign_map);
|
||||
assign_cell_connection_ports(mod, cell_sets, assign_map, config.cdc_file);
|
||||
}
|
||||
|
||||
// Reserve one core for our main thread, and don't create more worker threads
|
||||
|
|
|
|||
|
|
@ -0,0 +1,316 @@
|
|||
# =============================================================================
|
||||
# Test 1: Two coarse-grain $dff on different clocks, merged via -target
|
||||
# After merge + simplemap, verify all become $_DFF_P_ (posedge)
|
||||
# =============================================================================
|
||||
log -header "Two coarse-grain DFFs on different clocks"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, input clk2, input [7:0] d1, d2, output [7:0] q1, q2);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk1), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clk2), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge -target clk1
|
||||
select -assert-count 2 t:$dff
|
||||
simplemap
|
||||
select -assert-count 16 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 2: Single clock domain - nothing to merge
|
||||
# =============================================================================
|
||||
log -header "Single clock domain - no merge needed"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(input clk, input [7:0] d1, d2, output reg [7:0] q1, q2);
|
||||
always @(posedge clk) q1 <= d1;
|
||||
always @(posedge clk) q2 <= d2;
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge
|
||||
select -assert-count 2 t:$dff
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 3: Posedge and negedge on same clock - polarity merge (coarse-grain)
|
||||
# After merge + simplemap, both should be posedge
|
||||
# =============================================================================
|
||||
log -header "Merge posedge and negedge on same clock (coarse-grain)"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk, input [7:0] d1, d2, output [7:0] q1, q2);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b0), .WIDTH(8)) ff2 (.CLK(clk), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge -target clk
|
||||
select -assert-count 2 t:$dff
|
||||
simplemap
|
||||
# Both 8-bit DFFs (16 bits total) should now be posedge
|
||||
select -assert-count 16 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 4: Fine-grain $_DFF_P_ and $_DFF_N_ merged with explicit -target
|
||||
# =============================================================================
|
||||
log -header "Merge fine-grain DFF_P and DFF_N using -target for posedge"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk, input d1, d2, output q1, q2);
|
||||
$_DFF_P_ ff1 (.C(clk), .D(d1), .Q(q1));
|
||||
$_DFF_N_ ff2 (.C(clk), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 1 t:$_DFF_P_
|
||||
select -assert-count 1 t:$_DFF_N_
|
||||
clkmerge -target clk
|
||||
select -assert-count 2 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 5: Fine-grain DFFs on different clocks merged with explicit target
|
||||
# =============================================================================
|
||||
log -header "Fine-grain DFFs on different clocks merged via -target"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2, input d1, d2, output q1, q2);
|
||||
$_DFF_P_ ff1 (.C(clk1), .D(d1), .Q(q1));
|
||||
$_DFF_N_ ff2 (.C(clk2), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 1 t:$_DFF_P_
|
||||
select -assert-count 1 t:$_DFF_N_
|
||||
clkmerge -target clk1
|
||||
select -assert-count 2 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 6: -target option to force specific clock signal (coarse-grain)
|
||||
# =============================================================================
|
||||
log -header "Using -target option to force clk2"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2, input [7:0] d1, d2, output [7:0] q1, q2);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk1), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clk2), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge -target clk2
|
||||
select -assert-count 2 t:$dff
|
||||
simplemap
|
||||
select -assert-count 16 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 7: Three clock domains merged
|
||||
# =============================================================================
|
||||
log -header "Three clock domains merged"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clkA, clkB, clkC, input [7:0] d1, d2, d3, output [7:0] q1, q2, q3);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clkA), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clkB), .D(d2), .Q(q2));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff3 (.CLK(clkC), .D(d3), .Q(q3));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 3 t:$dff
|
||||
clkmerge -target clkA
|
||||
select -assert-count 3 t:$dff
|
||||
simplemap
|
||||
select -assert-count 24 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 8: Coarse-grain $dffe with different clocks and polarities
|
||||
# After merge, both should be posedge
|
||||
# =============================================================================
|
||||
log -header "Coarse-grain DFFE with different clocks and polarities"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2, en, input [7:0] d1, d2, output [7:0] q1, q2);
|
||||
$dffe #(.CLK_POLARITY(1'b1), .EN_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk1), .EN(en), .D(d1), .Q(q1));
|
||||
$dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clk2), .EN(en), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dffe
|
||||
clkmerge -target clk1
|
||||
select -assert-count 2 t:$dffe
|
||||
simplemap
|
||||
# Both should now be posedge-clk, posedge-enable
|
||||
select -assert-count 16 t:$_DFFE_PP_
|
||||
select -assert-count 0 t:$_DFFE_NP_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 9: Non-clocked cells (latches) are ignored
|
||||
# =============================================================================
|
||||
log -header "Non-clocked cells are ignored"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2, en, input [7:0] d1, d2, d3, output [7:0] q1, q2, q3);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk1), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clk2), .D(d2), .Q(q2));
|
||||
$dlatch #(.EN_POLARITY(1'b1), .WIDTH(8)) lat1 (.EN(en), .D(d3), .Q(q3));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dff
|
||||
select -assert-count 1 t:$dlatch
|
||||
clkmerge
|
||||
select -assert-count 2 t:$dff
|
||||
select -assert-count 1 t:$dlatch
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 10: Fine-grain $_DFFE_PP_ on different clocks merged with -target
|
||||
# =============================================================================
|
||||
log -header "Merge fine-grain DFFE_PP on different clocks"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2, en, input d1, d2, output q1, q2);
|
||||
$_DFFE_PP_ ff1 (.C(clk1), .E(en), .D(d1), .Q(q1));
|
||||
$_DFFE_PP_ ff2 (.C(clk2), .E(en), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$_DFFE_PP_
|
||||
clkmerge -target clk1
|
||||
select -assert-count 2 t:$_DFFE_PP_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 11: Module with no FFs - pass should do nothing
|
||||
# =============================================================================
|
||||
log -header "Module with no FFs"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(input a, b, output y);
|
||||
assign y = a & b;
|
||||
endmodule
|
||||
EOF
|
||||
clkmerge
|
||||
select -assert-count 1 t:$and
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 12: Miter-style use case - gold posedge clk1, gate negedge clk2
|
||||
# Verifies both clock signal and polarity are unified
|
||||
# =============================================================================
|
||||
log -header "Miter-style: gold posedge clk1, gate negedge clk2"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module miter(input clk1, clk2, input [7:0] d, output [7:0] q_gold, q_gate);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) gold_ff (.CLK(clk1), .D(d), .Q(q_gold));
|
||||
$dff #(.CLK_POLARITY(1'b0), .WIDTH(8)) gate_ff (.CLK(clk2), .D(d), .Q(q_gate));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge -target clk1
|
||||
select -assert-count 2 t:$dff
|
||||
simplemap
|
||||
# Both should be posedge after merge
|
||||
select -assert-count 16 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 13: Fine-grain $_DFF_PN0_ and $_DFF_NN0_ - async reset variants
|
||||
# =============================================================================
|
||||
log -header "Merge fine-grain DFF with async reset - DFF_PN0 and DFF_NN0"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk, rst, input d1, d2, output q1, q2);
|
||||
$_DFF_PN0_ ff1 (.C(clk), .R(rst), .D(d1), .Q(q1));
|
||||
$_DFF_NN0_ ff2 (.C(clk), .R(rst), .D(d2), .Q(q2));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 1 t:$_DFF_PN0_
|
||||
select -assert-count 1 t:$_DFF_NN0_
|
||||
clkmerge -target clk
|
||||
select -assert-count 2 t:$_DFF_PN0_
|
||||
select -assert-count 0 t:$_DFF_NN0_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 14: Many FFs across two domains - verify all unified
|
||||
# =============================================================================
|
||||
log -header "Many FFs across two clock domains"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -icells <<EOF
|
||||
module top(input clk1, clk2,
|
||||
input [7:0] d1, d2, d3, d4, d5,
|
||||
output [7:0] q1, q2, q3, q4, q5);
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff1 (.CLK(clk1), .D(d1), .Q(q1));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff2 (.CLK(clk1), .D(d2), .Q(q2));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff3 (.CLK(clk1), .D(d3), .Q(q3));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff4 (.CLK(clk2), .D(d4), .Q(q4));
|
||||
$dff #(.CLK_POLARITY(1'b1), .WIDTH(8)) ff5 (.CLK(clk2), .D(d5), .Q(q5));
|
||||
endmodule
|
||||
EOF
|
||||
select -assert-count 5 t:$dff
|
||||
clkmerge -target clk1
|
||||
select -assert-count 5 t:$dff
|
||||
simplemap
|
||||
# 5 * 8 = 40 bits, all posedge
|
||||
select -assert-count 40 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 15: Verilog-level posedge/negedge merging - verify polarity unified
|
||||
# =============================================================================
|
||||
log -header "Verilog-level posedge and negedge merge"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(input clk, input [7:0] d1, d2, output reg [7:0] q1, q2);
|
||||
always @(posedge clk) q1 <= d1;
|
||||
always @(negedge clk) q2 <= d2;
|
||||
endmodule
|
||||
EOF
|
||||
proc
|
||||
select -assert-count 2 t:$dff
|
||||
clkmerge -target clk
|
||||
select -assert-count 2 t:$dff
|
||||
simplemap
|
||||
select -assert-count 16 t:$_DFF_P_
|
||||
select -assert-count 0 t:$_DFF_N_
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
@ -0,0 +1,363 @@
|
|||
# =============================================================================
|
||||
# Test 1: Basic structurally identical gold/gate — single FF, single clock
|
||||
# Both modules have exactly the same structure. The FF should be matched
|
||||
# and exposed as a cone PI/PO pair.
|
||||
# =============================================================================
|
||||
log -header "Basic identical gold/gate single FF"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
select -module gate
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 2: Multiple matched FF groups — two independent FFs
|
||||
# Both modules have two FFs with identical structure. Each FF should get
|
||||
# its own cone.
|
||||
# =============================================================================
|
||||
log -header "Multiple matched FF groups"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c ^ d;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c ^ d;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone_0*
|
||||
select -assert-any w:*cone_1*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 3: No structural match — different FF fanin logic
|
||||
# Gold uses addition, gate uses subtraction for the same FF. The structural
|
||||
# hashes should NOT match, so no cones should be created.
|
||||
# =============================================================================
|
||||
log -header "No structural match"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a - b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-none w:*cone*
|
||||
select -clear
|
||||
select -module gate
|
||||
select -assert-none w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 4: Partial match — one FF matches, one doesn't
|
||||
# Both modules have two FFs; one with identical fanin (a+b), the other
|
||||
# with different fanin (c^d vs c&d). Only the matching FF should be coned.
|
||||
# =============================================================================
|
||||
log -header "Partial match"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c ^ d;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c & d;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone_0*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 5: Wide FFs (32-bit) — structural match on wider registers
|
||||
# =============================================================================
|
||||
log -header "Wide FFs match"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [31:0] a, b, output reg [31:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a & b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [31:0] a, b, output reg [31:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a & b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 6: Negedge clock — both modules use negedge, should still match
|
||||
# =============================================================================
|
||||
log -header "Negedge clock match"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(negedge clk)
|
||||
q <= a | b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(negedge clk)
|
||||
q <= a | b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 7: Chain of combinational logic before FF — deeper cones
|
||||
# The structural hash should still match through the combinational chain.
|
||||
# =============================================================================
|
||||
log -header "Deeper combinational cone"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, c,
|
||||
output reg [7:0] q);
|
||||
wire [7:0] t1 = a + b;
|
||||
wire [7:0] t2 = t1 ^ c;
|
||||
always @(posedge clk)
|
||||
q <= t2;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, c,
|
||||
output reg [7:0] q);
|
||||
wire [7:0] t1 = a + b;
|
||||
wire [7:0] t2 = t1 ^ c;
|
||||
always @(posedge clk)
|
||||
q <= t2;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 8: Verbose output and log file option
|
||||
# Verify that -o flag creates a log file without errors.
|
||||
# =============================================================================
|
||||
log -header "Verbose with log file"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk) q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk) q <= a + b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v -o /tmp/cone_partition_test.log gold gate
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 9: Multiple FFs, some with enable, mixed structure
|
||||
# Gold and gate both have 3 FFs: two match structurally, one doesn't.
|
||||
# =============================================================================
|
||||
log -header "Mixed FFs with enable"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input en,
|
||||
input [7:0] a, b, c, d, e, f,
|
||||
output reg [7:0] q1, q2, q3);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c & d;
|
||||
if (en) q3 <= e ^ f;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input en,
|
||||
input [7:0] a, b, c, d, e, f,
|
||||
output reg [7:0] q1, q2, q3);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c & d;
|
||||
if (en) q3 <= e | f;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_expr; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 10: Identity — gate is exact copy of gold (all FFs should match)
|
||||
# =============================================================================
|
||||
log -header "Exact copy — all FFs match"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, c, d, e, f,
|
||||
output reg [7:0] q1, q2, q3);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c ^ d;
|
||||
q3 <= e & f;
|
||||
end
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, c, d, e, f,
|
||||
output reg [7:0] q1, q2, q3);
|
||||
always @(posedge clk) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c ^ d;
|
||||
q3 <= e & f;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*cone_0*
|
||||
select -assert-any w:*cone_1*
|
||||
select -assert-any w:*cone_2*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 11: Completely different modules — zero matching FFs
|
||||
# Gold and gate have entirely different operations on the same ports.
|
||||
# =============================================================================
|
||||
log -header "Completely different — no cones"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a ^ b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-none w:*cone*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# Test 12: PI/PO wire naming conventions
|
||||
# Verify that matched cones produce wires with the expected naming pattern.
|
||||
# =============================================================================
|
||||
log -header "PI/PO naming"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
cone_partition -v gold gate
|
||||
select -module gold
|
||||
select -assert-any w:*ff_pi*
|
||||
select -assert-any w:*_po*
|
||||
select -clear
|
||||
select -module gate
|
||||
select -assert-any w:*ff_pi*
|
||||
select -assert-any w:*_po*
|
||||
select -clear
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# TODO: Test cases for both gold and gate having the same number of
|
||||
# multiple clock domains (both multi-clock). These would test the
|
||||
# unmatched FF guarding with clkguard PIs and AND gates.
|
||||
# =============================================================================
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
# Clock domain mismatch — gold has two clocks, gate has one.
|
||||
# The pass should error declaring inequivalence.
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk1, input clk2,
|
||||
input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk1) q1 <= a + b;
|
||||
always @(posedge clk2) q2 <= c + d;
|
||||
endmodule
|
||||
|
||||
module gate(input clk1, input clk2,
|
||||
input [7:0] a, b, c, d,
|
||||
output reg [7:0] q1, q2);
|
||||
always @(posedge clk1) begin
|
||||
q1 <= a + b;
|
||||
q2 <= c + d;
|
||||
end
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
logger -expect error "Designs are inequivalent: clock domain count mismatch" 1
|
||||
cone_partition -v gold gate
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
# Port mismatch — gate is missing an input port from gold.
|
||||
# The pass should error because ports don't match.
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module gold(input clk, input [7:0] a, b, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a + b;
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input [7:0] a, output reg [7:0] q);
|
||||
always @(posedge clk)
|
||||
q <= a;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt_clean
|
||||
logger -expect error "Input port.*has no match" 1
|
||||
cone_partition -v gold gate
|
||||
2
verific
2
verific
|
|
@ -1 +1 @@
|
|||
Subproject commit 4feaf1f923157af0ed064eab8e302647bd5fa1b7
|
||||
Subproject commit 87cb8cf50448c4d28a1b2d57bd4afc119b6439af
|
||||
Loading…
Reference in New Issue