From db039c598727884acb7c8d74e3a3d5cf75e61958 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 6 Mar 2026 11:41:33 -0800 Subject: [PATCH 01/27] Added Makefile with passed required for SAT --- Makefile | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Makefile b/Makefile index ec93a0bb6..fccf456eb 100644 --- a/Makefile +++ b/Makefile @@ -763,6 +763,9 @@ 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/techmap/extract.o OBJS += passes/techmap/extract_reduce.o OBJS += passes/techmap/alumacc.o @@ -773,6 +776,7 @@ 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 include $(YOSYS_SRC)/passes/hierarchy/Makefile.inc include $(YOSYS_SRC)/passes/memory/Makefile.inc From 8006d148de3ff599bb15702399945d49e5208d02 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 13 Mar 2026 16:08:10 -0700 Subject: [PATCH 02/27] New abc --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index bb9bc209f..004bb53ed 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit bb9bc209ff23e6690865935a70bcc9294101c5ce +Subproject commit 004bb53ed9ae20fe61db7d7d9a0ed467c8eeff1e From 11af3b5872bc70ba35a9a3d3c2cde480b310bece Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 13 Mar 2026 16:37:05 -0700 Subject: [PATCH 03/27] Added abc logs --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index 004bb53ed..a14aabd1e 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit 004bb53ed9ae20fe61db7d7d9a0ed467c8eeff1e +Subproject commit a14aabd1e9a043472eac6e6b75a8609e800101f8 From aff1836869aa1962da4317b8f1fbbf1ca9f55a93 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 13 Mar 2026 16:40:23 -0700 Subject: [PATCH 04/27] Abc printing to normal file --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index a14aabd1e..b232cbf52 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit a14aabd1e9a043472eac6e6b75a8609e800101f8 +Subproject commit b232cbf521eb6b78d16616bf5062543bdb9ca6eb From a3ffc5da30a15058992fd919d150e0ca05d74e0e Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Wed, 18 Mar 2026 11:53:47 -0700 Subject: [PATCH 05/27] Added new passes/sat/struct_partition.cc pass to propagate the ports out --- Makefile | 1 + passes/sat/Makefile.inc | 1 + passes/sat/struct_partition.cc | 614 +++++++++++++++++++++++++++++++++ 3 files changed, 616 insertions(+) create mode 100644 passes/sat/struct_partition.cc diff --git a/Makefile b/Makefile index fccf456eb..07582f645 100644 --- a/Makefile +++ b/Makefile @@ -765,6 +765,7 @@ OBJS += passes/sat/recover_names.o OBJS += passes/sat/sim.o OBJS += passes/sat/sat.o OBJS += passes/sat/miter.o +OBJS += passes/sat/struct_partition.o OBJS += passes/sat/async2sync.o OBJS += passes/techmap/extract.o OBJS += passes/techmap/extract_reduce.o diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index d9bf69dcb..11a415ba4 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -15,6 +15,7 @@ OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o OBJS += passes/sat/cutpoint.o +OBJS += passes/sat/struct_partition.o OBJS += passes/sat/fminit.o OBJS += passes/sat/recover_names.o ifeq ($(DISABLE_SPAWN),0) diff --git a/passes/sat/struct_partition.cc b/passes/sat/struct_partition.cc new file mode 100644 index 000000000..1511e66f4 --- /dev/null +++ b/passes/sat/struct_partition.cc @@ -0,0 +1,614 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Structural-isomorphism partitioning for equivalence checking. + * + * Given two modules (typically named "gold" and "gate") with matching + * port signatures, this pass: + * + * 1. Builds a bottom-up structural hash for every cell in each module. + * The hash captures cell type, parameters, and the recursive structure + * of each input driver chain back to primary inputs. Wire and cell + * names are deliberately ignored — only connectivity and function + * matter. + * + * 2. Finds hash groups where cells from BOTH modules appear. Every cell + * in such a group computes the same Boolean function of the same + * primary inputs, so they are structurally equivalent. + * + * 3. For each matched group, replaces every cell's output in both + * modules with a shared new primary-input port (a "cutpoint"). + * The matched cells and all transitively dead fanin logic are then + * removed. + * + * The result is a pair of simplified modules whose remaining logic is + * exactly the part that differs — or that could not be structurally + * matched — ready to be fed into `miter -equiv` and a SAT/PDR solver. + * + * The key insight is that structurally identical subcircuits do not need + * to be proved equivalent by the solver; replacing them with free inputs + * shrinks the problem while preserving soundness. + * + * Algorithm notes + * --------------- + * - Primary inputs hash by their port name (shared between gold/gate). + * - Constants hash by their value. + * - Flip-flop Q outputs break feedback loops: when computing the hash + * of a FF, we do NOT recurse through Q. Instead, Q is treated as a + * fresh leaf ("secondary PI") in the downstream combinational cone. + * The FF itself IS hashed (by type + params + input drivers), so two + * structurally identical FFs will match. + * - The hash is a tuple-like structure (not a numeric hash), so there + * are no collisions — matching is exact. + * + * 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/log.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +// --------------------------------------------------------------------------- +// StructuralHash — collision-free structural identity +// --------------------------------------------------------------------------- +// +// Each cell's "structural hash" is a tree-shaped value that encodes: +// (cell_type, {parameters}, {port -> driver_hash, ...}) +// +// We serialise these trees into interned integer IDs so that comparison +// is O(1) after the initial bottom-up pass. Two cells get the same ID +// if and only if they are structurally identical. + +struct StructuralHasher { + // Intern table: canonical representation -> unique ID + dict, int> intern_table; + int next_id = 1; + + // Sentinel IDs for leaves + enum { CONST_BASE = -1000000, PI_BASE = -2000000, CYCLE_GUARD = 0 }; + + int intern(const std::vector &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; + } + + // Intern a primary-input identity. We use the port name's hash to + // generate a stable integer that is the same in both gold and gate. + dict pi_ids; + int intern_pi(IdString port_name) { + auto it = pi_ids.find(port_name); + if (it != pi_ids.end()) + return it->second; + int id = PI_BASE - (int)pi_ids.size(); + pi_ids[port_name] = id; + return id; + } + + // Intern a constant value. + dict 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 +// --------------------------------------------------------------------------- + +struct ModuleAnalysis { + RTLIL::Module *module; + SigMap sigmap; + CellTypes ct; + + // bit -> (cell, port) that drives it + dict> bit_driver; + + // cell -> structural hash ID + dict cell_hash; + + // Which SigBits are primary inputs (module input ports) + dict pi_bits; // bit -> port_name + + // Set of cells being visited (cycle detection) + pool visiting; + + // Set of cells that are flip-flops / sequential + pool ff_cells; + + ModuleAnalysis(RTLIL::Module *mod, Design *design) : module(mod), sigmap(mod) { + ct.setup(design); + + // Record primary-input bits + 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; + } + } + + // Build bit -> driver map + 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}; + } + } + } + } + + // Compute structural hash for a single SigBit + int hash_bit(SigBit bit, StructuralHasher &hasher) { + bit = sigmap(bit); + + // Constant + if (bit.wire == nullptr) + return hasher.intern_const(Const(bit.data)); + + // Primary input + auto pi_it = pi_bits.find(bit); + if (pi_it != pi_bits.end()) + return hasher.intern_pi(pi_it->second); + + // Driven by a cell + 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; + + // For FFs, treat Q as a secondary PI (to break cycles). + // The FF itself will get its own hash via hash_cell. + if (ff_cells.count(drv_cell) && drv_port == ID::Q) { + int ff_hash = hash_cell(drv_cell, hasher); + // Encode "output bit i of ff with hash ff_hash" + 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 key = {ff_hash, bit_idx, -99}; + return hasher.intern(key); + } + + int ch = hash_cell(drv_cell, hasher); + // Multi-bit output: encode which bit of the output we're reading + 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 key = {ch, bit_idx, (int)drv_port.index_}; + return hasher.intern(key); + } + + // Undriven wire — treat as a unique unknown + return hasher.intern_const(Const(State::Sx)); + } + + // Compute structural hash for a SigSpec (multi-bit signal) + int hash_sig(const SigSpec &sig, StructuralHasher &hasher) { + SigSpec mapped = sigmap(sig); + if (GetSize(mapped) == 1) + return hash_bit(mapped[0], hasher); + + std::vector key; + key.reserve(GetSize(mapped) + 1); + key.push_back(-77); // tag for "concatenated signal" + for (auto &bit : mapped) + key.push_back(hash_bit(bit, hasher)); + return hasher.intern(key); + } + + // Compute structural hash for a cell + int hash_cell(Cell *cell, StructuralHasher &hasher) { + auto it = cell_hash.find(cell); + if (it != cell_hash.end()) + return it->second; + + // Cycle guard + if (visiting.count(cell)) { + cell_hash[cell] = StructuralHasher::CYCLE_GUARD; + return StructuralHasher::CYCLE_GUARD; + } + visiting.insert(cell); + + // Build the key: cell_type, sorted parameters, sorted input hashes + std::vector key; + + // Cell type + key.push_back((int)cell->type.index_); + + // Parameters (sorted by name for determinism) + std::vector> 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); // separator + for (auto &[pname, pval] : sorted_params) { + key.push_back((int)pname.index_); + key.push_back(hasher.intern_const(pval)); + } + + // Input connections (sorted by port name) + key.push_back(-99); // separator + std::vector> 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; + } + + // Hash all cells in the module + void hash_all_cells(StructuralHasher &hasher) { + for (auto cell : module->cells()) + hash_cell(cell, hasher); + } +}; + +// --------------------------------------------------------------------------- +// Core: find matches and apply cutpoints +// --------------------------------------------------------------------------- + +struct StructPartitionWorker { + Design *design; + Module *gold_mod; + Module *gate_mod; + bool verbose; + + int total_cutpoints = 0; + int total_cells_removed = 0; + + StructPartitionWorker(Design *d, Module *gold, Module *gate, bool v) + : design(d), gold_mod(gold), gate_mod(gate), verbose(v) {} + + void run() { + // A single shared hasher ensures the same intern IDs across both modules + StructuralHasher hasher; + + log("Structural partitioning: analyzing module `%s'.\n", gold_mod->name.c_str()); + ModuleAnalysis gold_analysis(gold_mod, design); + gold_analysis.hash_all_cells(hasher); + + log("Structural partitioning: analyzing module `%s'.\n", gate_mod->name.c_str()); + ModuleAnalysis gate_analysis(gate_mod, design); + gate_analysis.hash_all_cells(hasher); + + // Group cells by structural hash across both modules + dict> gold_by_hash, gate_by_hash; + for (auto &[cell, h] : gold_analysis.cell_hash) + if (h != StructuralHasher::CYCLE_GUARD) + gold_by_hash[h].push_back(cell); + for (auto &[cell, h] : gate_analysis.cell_hash) + if (h != StructuralHasher::CYCLE_GUARD) + gate_by_hash[h].push_back(cell); + + // Find hashes present in BOTH modules — these are the structural matches. + // ALL cells with a matching hash (in both modules) get the same cutpoint. + struct CutpointGroup { + std::vector gold_cells; + std::vector gate_cells; + }; + std::vector groups; + + for (auto &[h, gold_cells] : gold_by_hash) { + auto it = gate_by_hash.find(h); + if (it == gate_by_hash.end()) + continue; + groups.push_back({gold_cells, it->second}); + } + + if (groups.empty()) { + log("No structural matches found between `%s' and `%s'.\n", + gold_mod->name.c_str(), gate_mod->name.c_str()); + return; + } + + log("Found %d structurally matched groups.\n", (int)groups.size()); + + // For each group, create cutpoint PIs and rewire + for (auto &group : groups) + apply_cutpoint_group(group.gold_cells, group.gate_cells, + gold_analysis, gate_analysis); + + // Remove transitively dead cells from both modules + remove_dead_cells(gold_mod); + remove_dead_cells(gate_mod); + + gold_mod->fixup_ports(); + gate_mod->fixup_ports(); + + log("Structural partitioning: created %d cutpoints, removed %d cells.\n", + total_cutpoints, total_cells_removed); + } + +private: + // Create a cutpoint for one matched group. + // + // Every cell in gold_cells and gate_cells computes the same function. + // We pick the output port(s) of the cell type, create a fresh input + // port with the same width on BOTH modules (same name), and rewire + // all the cells' outputs to that port. Then we remove the cells. + void apply_cutpoint_group( + const std::vector &gold_cells, + const std::vector &gate_cells, + ModuleAnalysis &/*gold_an*/, + ModuleAnalysis &/*gate_an*/) + { + if (gold_cells.empty() || gate_cells.empty()) + return; + + Cell *representative = gold_cells[0]; + + // Determine output ports for this cell type + std::vector out_ports; + for (auto &conn : representative->connections()) + if (representative->output(conn.first)) + out_ports.push_back(conn.first); + + if (out_ports.empty()) + return; + + for (auto out_port : out_ports) { + SigSpec rep_sig = representative->getPort(out_port); + int width = GetSize(rep_sig); + if (width == 0) + continue; + + // Create a unique cutpoint name + std::string cut_name = stringf("\\cut_%d", total_cutpoints); + total_cutpoints++; + + if (verbose) + log(" Cutpoint %s (width %d) for %d+%d cells of type %s.\n", + cut_name.c_str(), width, + (int)gold_cells.size(), (int)gate_cells.size(), + representative->type.c_str()); + + // Create the new input port on both modules + Wire *gold_cut = gold_mod->addWire(cut_name, width); + gold_cut->port_input = true; + + Wire *gate_cut = gate_mod->addWire(cut_name, width); + gate_cut->port_input = true; + + // Rewire all gold cells: connect their output to the cutpoint wire + for (auto cell : gold_cells) { + SigSpec old_sig = cell->getPort(out_port); + if (GetSize(old_sig) != width) continue; + gold_mod->connect(old_sig, gold_cut); + } + + // Rewire all gate cells: connect their output to the cutpoint wire + for (auto cell : gate_cells) { + SigSpec old_sig = cell->getPort(out_port); + if (GetSize(old_sig) != width) continue; + gate_mod->connect(old_sig, gate_cut); + } + } + + // Remove the matched cells + for (auto cell : gold_cells) { + if (verbose) + log_debug(" Removing gold cell `%s'.\n", cell->name.c_str()); + gold_mod->remove(cell); + total_cells_removed++; + } + for (auto cell : gate_cells) { + if (verbose) + log_debug(" Removing gate cell `%s'.\n", cell->name.c_str()); + gate_mod->remove(cell); + total_cells_removed++; + } + } + + // Remove cells whose outputs are entirely unconnected. + // Iterate to fixpoint since removing one cell may make its drivers dead. + void remove_dead_cells(Module *mod) { + SigMap sigmap(mod); + + bool changed = true; + while (changed) { + changed = false; + + // Collect all bits that are used as inputs somewhere + pool used_bits; + for (auto cell : mod->cells()) + for (auto &conn : cell->connections()) + if (cell->input(conn.first)) + for (auto bit : sigmap(conn.second)) + if (bit.wire) + used_bits.insert(bit); + + // Module output ports are "used" + for (auto wire : mod->wires()) + if (wire->port_output) + for (auto bit : sigmap(wire)) + used_bits.insert(bit); + + // Also count bits used in module-level connections (LHS = driven) + for (auto &conn : mod->connections()) { + for (auto bit : sigmap(conn.first)) + if (bit.wire) + used_bits.insert(bit); + for (auto bit : sigmap(conn.second)) + if (bit.wire) + used_bits.insert(bit); + } + + // Remove cells whose outputs are entirely unused + std::vector to_remove; + for (auto cell : mod->cells()) { + bool any_output_used = false; + bool has_output = false; + for (auto &conn : cell->connections()) { + if (!cell->output(conn.first)) + continue; + has_output = true; + for (auto bit : sigmap(conn.second)) { + if (used_bits.count(bit)) { + any_output_used = true; + break; + } + } + if (any_output_used) break; + } + // Only remove cells that have outputs but none are used. + // Keep cells with no outputs (side effects like $assert). + if (has_output && !any_output_used && !cell->has_keep_attr()) + to_remove.push_back(cell); + } + + for (auto cell : to_remove) { + if (verbose) + log_debug(" Dead cell removal: `%s' (%s).\n", + cell->name.c_str(), cell->type.c_str()); + mod->remove(cell); + total_cells_removed++; + changed = true; + } + + if (changed) + sigmap.set(mod); + } + } +}; + +// --------------------------------------------------------------------------- +// Pass registration +// --------------------------------------------------------------------------- + +struct StructPartitionPass : public Pass { + StructPartitionPass() : Pass("struct_partition", + "partition equivalent subcircuits between two modules") { } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" struct_partition [options] gold_module gate_module\n"); + log("\n"); + log("This pass identifies structurally identical subcircuits between two modules\n"); + log("(typically a gold and gate design for equivalence checking) and replaces\n"); + log("matched logic with shared primary-input cutpoints.\n"); + log("\n"); + log("The structural matching is purely based on cell types, parameters, and\n"); + log("input connectivity — cell and wire names are ignored entirely.\n"); + log("\n"); + log("For each group of cells that are structurally identical across both modules,\n"); + log("ALL cells in the group are removed and their outputs are replaced by a new\n"); + log("input port with the same name in both modules. Transitively dead fanin\n"); + log("logic is also removed.\n"); + log("\n"); + log("This shrinks the subsequent `miter -equiv` + SAT/PDR problem by eliminating\n"); + log("logic that is provably identical by construction.\n"); + log("\n"); + log(" -v\n"); + log(" verbose output: log each cutpoint and removed cell\n"); + log("\n"); + log("Typical usage:\n"); + log("\n"); + log(" read_rtlil gold.il\n"); + log(" read_rtlil gate.il\n"); + log(" struct_partition gold gate\n"); + log(" miter -equiv gold gate miter\n"); + log(" ...\n"); + log("\n"); + } + + void execute(std::vector args, RTLIL::Design *design) override + { + bool verbose = false; + + log_header(design, "Executing STRUCT_PARTITION pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-v") { + verbose = true; + 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()); + + // Verify port compatibility + 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); + } + + StructPartitionWorker worker(design, gold_mod, gate_mod, verbose); + worker.run(); + } +} StructPartitionPass; + +PRIVATE_NAMESPACE_END From dc73249d8f12364f2b71de58c15b79b44f1b71bc Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Wed, 18 Mar 2026 16:23:41 -0700 Subject: [PATCH 06/27] Added support for printing the signal map --- Makefile | 1 + passes/techmap/abc.cc | 31 +++++++++++++++++++++++++++++++ 2 files changed, 32 insertions(+) diff --git a/Makefile b/Makefile index 07582f645..0e41ee2cb 100644 --- a/Makefile +++ b/Makefile @@ -790,6 +790,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 diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 9e8e3f3a2..b62fb6f9b 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -148,6 +148,7 @@ 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; }; struct AbcSigVal { @@ -1217,6 +1218,28 @@ void RunAbcState::run(ConcurrentStack &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(), "wt"); + if (mf == nullptr) { + logs.log("Opening %s for writing failed: %s\n", config.signal_map_file, strerror(errno)); + } else { + fprintf(mf, "# ABC signal name -> Yosys signal name\n"); + 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); @@ -2046,6 +2069,10 @@ 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 \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(" -reserved_cores \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"); @@ -2258,6 +2285,10 @@ 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; + } break; } extra_args(args, argidx, design); From 52fad78b40b23d6b0edc8e9764ab305e174cc518 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 09:23:12 -0700 Subject: [PATCH 07/27] Removed is_port for non-trigger outputs. TODO: add a flag which does this so POs are only those ones --- passes/techmap/abc.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index b62fb6f9b..1df3d9027 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -1205,11 +1205,23 @@ void RunAbcState::run(ConcurrentStack &process_pool) fprintf(f, " dummy_input\n"); fprintf(f, "\n"); + // Only keep the output port whose signal originates from the miter equiv NOT cell + 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 (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; } From 26db947b5736a974bf1070d77d0f2f591d0cec29 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 10:08:52 -0700 Subject: [PATCH 08/27] Added zinit --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 0e41ee2cb..29949995b 100644 --- a/Makefile +++ b/Makefile @@ -778,6 +778,7 @@ 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 From 8536ab69c16ddfc7fdfd026a4bd70e6b79c5389a Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 10:09:11 -0700 Subject: [PATCH 09/27] Added -o option for output file in struct_partition --- passes/sat/struct_partition.cc | 56 ++++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 12 deletions(-) diff --git a/passes/sat/struct_partition.cc b/passes/sat/struct_partition.cc index 1511e66f4..dea616ac5 100644 --- a/passes/sat/struct_partition.cc +++ b/passes/sat/struct_partition.cc @@ -61,6 +61,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -303,22 +304,35 @@ struct StructPartitionWorker { Module *gold_mod; Module *gate_mod; bool verbose; + FILE *log_file; int total_cutpoints = 0; int total_cells_removed = 0; - StructPartitionWorker(Design *d, Module *gold, Module *gate, bool v) - : design(d), gold_mod(gold), gate_mod(gate), verbose(v) {} + StructPartitionWorker(Design *d, Module *gold, Module *gate, bool v, FILE *lf = nullptr) + : design(d), gold_mod(gold), gate_mod(gate), verbose(v), log_file(lf) {} + + 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); + } void run() { // A single shared hasher ensures the same intern IDs across both modules StructuralHasher hasher; - log("Structural partitioning: analyzing module `%s'.\n", gold_mod->name.c_str()); + vlog("Structural partitioning: analyzing module `%s'.\n", gold_mod->name.c_str()); ModuleAnalysis gold_analysis(gold_mod, design); gold_analysis.hash_all_cells(hasher); - log("Structural partitioning: analyzing module `%s'.\n", gate_mod->name.c_str()); + vlog("Structural partitioning: analyzing module `%s'.\n", gate_mod->name.c_str()); ModuleAnalysis gate_analysis(gate_mod, design); gate_analysis.hash_all_cells(hasher); @@ -347,12 +361,12 @@ struct StructPartitionWorker { } if (groups.empty()) { - log("No structural matches found between `%s' and `%s'.\n", + vlog("No structural matches found between `%s' and `%s'.\n", gold_mod->name.c_str(), gate_mod->name.c_str()); return; } - log("Found %d structurally matched groups.\n", (int)groups.size()); + vlog("Found %d structurally matched groups.\n", (int)groups.size()); // For each group, create cutpoint PIs and rewire for (auto &group : groups) @@ -366,7 +380,7 @@ struct StructPartitionWorker { gold_mod->fixup_ports(); gate_mod->fixup_ports(); - log("Structural partitioning: created %d cutpoints, removed %d cells.\n", + vlog("Structural partitioning: created %d cutpoints, removed %d cells.\n", total_cutpoints, total_cells_removed); } @@ -408,7 +422,7 @@ private: total_cutpoints++; if (verbose) - log(" Cutpoint %s (width %d) for %d+%d cells of type %s.\n", + vlog(" Cutpoint %s (width %d) for %d+%d cells of type %s.\n", cut_name.c_str(), width, (int)gold_cells.size(), (int)gate_cells.size(), representative->type.c_str()); @@ -438,13 +452,13 @@ private: // Remove the matched cells for (auto cell : gold_cells) { if (verbose) - log_debug(" Removing gold cell `%s'.\n", cell->name.c_str()); + vlog(" Removing gold cell `%s'.\n", cell->name.c_str()); gold_mod->remove(cell); total_cells_removed++; } for (auto cell : gate_cells) { if (verbose) - log_debug(" Removing gate cell `%s'.\n", cell->name.c_str()); + vlog(" Removing gate cell `%s'.\n", cell->name.c_str()); gate_mod->remove(cell); total_cells_removed++; } @@ -509,7 +523,7 @@ private: for (auto cell : to_remove) { if (verbose) - log_debug(" Dead cell removal: `%s' (%s).\n", + vlog(" Dead cell removal: `%s' (%s).\n", cell->name.c_str(), cell->type.c_str()); mod->remove(cell); total_cells_removed++; @@ -554,6 +568,9 @@ struct StructPartitionPass : public Pass { log(" -v\n"); log(" verbose output: log each cutpoint and removed cell\n"); log("\n"); + log(" -o \n"); + log(" write verbose log output to instead of standard log\n"); + log("\n"); log("Typical usage:\n"); log("\n"); log(" read_rtlil gold.il\n"); @@ -567,6 +584,7 @@ struct StructPartitionPass : public Pass { void execute(std::vector args, RTLIL::Design *design) override { bool verbose = false; + std::string log_file_path; log_header(design, "Executing STRUCT_PARTITION pass.\n"); @@ -576,6 +594,10 @@ struct StructPartitionPass : public Pass { verbose = true; continue; } + if (args[argidx] == "-o" && argidx + 1 < args.size()) { + log_file_path = args[++argidx]; + continue; + } break; } @@ -606,8 +628,18 @@ struct StructPartitionPass : public Pass { gold_wire->name.c_str(), gold_wire->width, gate_wire->width); } - StructPartitionWorker worker(design, gold_mod, gate_mod, verbose); + 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()); + } + + StructPartitionWorker worker(design, gold_mod, gate_mod, verbose, log_file); worker.run(); + + if (log_file) + fclose(log_file); } } StructPartitionPass; From 522ead01df0a39771082ba248fdb16defe2dd4d4 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 15:04:13 -0700 Subject: [PATCH 10/27] Added small fixes --- passes/sat/struct_partition.cc | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/passes/sat/struct_partition.cc b/passes/sat/struct_partition.cc index dea616ac5..1c3aaa8b7 100644 --- a/passes/sat/struct_partition.cc +++ b/passes/sat/struct_partition.cc @@ -94,15 +94,19 @@ struct StructuralHasher { return id; } - // Intern a primary-input identity. We use the port name's hash to - // generate a stable integer that is the same in both gold and gate. - dict pi_ids; - int intern_pi(IdString port_name) { - auto it = pi_ids.find(port_name); + // Intern a primary-input bit identity. We use the port name AND bit + // index to generate a stable integer that is the same in both gold + // and gate. Each bit of a multi-bit port must get a distinct ID, + // otherwise cones differing only in which bit they read would + // incorrectly appear structurally identical. + dict, 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[port_name] = id; + pi_ids[key] = id; return id; } @@ -134,7 +138,7 @@ struct ModuleAnalysis { dict cell_hash; // Which SigBits are primary inputs (module input ports) - dict pi_bits; // bit -> port_name + dict> pi_bits; // bit -> (port_name, bit_idx) // Set of cells being visited (cycle detection) pool visiting; @@ -150,7 +154,7 @@ struct ModuleAnalysis { if (wire->port_input) { SigSpec sig = sigmap(wire); for (int i = 0; i < GetSize(sig); i++) - pi_bits[sig[i]] = wire->name; + pi_bits[sig[i]] = {wire->name, i}; } } @@ -186,7 +190,7 @@ struct ModuleAnalysis { // Primary input auto pi_it = pi_bits.find(bit); if (pi_it != pi_bits.end()) - return hasher.intern_pi(pi_it->second); + return hasher.intern_pi(pi_it->second.first, pi_it->second.second); // Driven by a cell auto drv_it = bit_driver.find(bit); From 1711da5506dbfcfb61f264c2e8eba3474a19310d Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 15:06:50 -0700 Subject: [PATCH 11/27] Moved the struct_partition pass to Silimate --- Makefile | 1 - passes/silimate/Makefile.inc | 1 + passes/{sat => silimate}/struct_partition.cc | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename passes/{sat => silimate}/struct_partition.cc (100%) diff --git a/Makefile b/Makefile index 29949995b..6f3f3f247 100644 --- a/Makefile +++ b/Makefile @@ -765,7 +765,6 @@ OBJS += passes/sat/recover_names.o OBJS += passes/sat/sim.o OBJS += passes/sat/sat.o OBJS += passes/sat/miter.o -OBJS += passes/sat/struct_partition.o OBJS += passes/sat/async2sync.o OBJS += passes/techmap/extract.o OBJS += passes/techmap/extract_reduce.o diff --git a/passes/silimate/Makefile.inc b/passes/silimate/Makefile.inc index f57fcab15..1518a9bc0 100644 --- a/passes/silimate/Makefile.inc +++ b/passes/silimate/Makefile.inc @@ -15,6 +15,7 @@ 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/struct_partition.o OBJS += passes/silimate/opt_expand.o GENFILES += passes/silimate/peepopt_expand.h diff --git a/passes/sat/struct_partition.cc b/passes/silimate/struct_partition.cc similarity index 100% rename from passes/sat/struct_partition.cc rename to passes/silimate/struct_partition.cc From daf51084342491b81ce223e66136266277157965 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 19 Mar 2026 16:30:11 -0700 Subject: [PATCH 12/27] Added inital cone_parition.cc pass. TODO: check with larger designs --- passes/silimate/Makefile.inc | 1 + passes/silimate/cone_partition.cc | 511 ++++++++++++++++++++++++++++++ 2 files changed, 512 insertions(+) create mode 100644 passes/silimate/cone_partition.cc diff --git a/passes/silimate/Makefile.inc b/passes/silimate/Makefile.inc index 1518a9bc0..86685e05a 100644 --- a/passes/silimate/Makefile.inc +++ b/passes/silimate/Makefile.inc @@ -16,6 +16,7 @@ OBJS += passes/silimate/splitlarge.o OBJS += passes/silimate/splitnetlist.o OBJS += passes/silimate/opt_timing_balance.o OBJS += passes/silimate/struct_partition.o +OBJS += passes/silimate/cone_partition.o OBJS += passes/silimate/opt_expand.o GENFILES += passes/silimate/peepopt_expand.h diff --git a/passes/silimate/cone_partition.cc b/passes/silimate/cone_partition.cc new file mode 100644 index 000000000..7007f7b57 --- /dev/null +++ b/passes/silimate/cone_partition.cc @@ -0,0 +1,511 @@ +/* + * 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. + * + * 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/log.h" +#include + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +// --------------------------------------------------------------------------- +// StructuralHash — collision-free structural identity (same as struct_partition) +// --------------------------------------------------------------------------- + +struct StructuralHasher { + dict, int> intern_table; + int next_id = 1; + + enum { CONST_BASE = -1000000, PI_BASE = -2000000, CYCLE_GUARD = 0 }; + + int intern(const std::vector &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, 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_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> bit_driver; + dict cell_hash; + dict> pi_bits; + pool visiting; + pool 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 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 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 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 key; + key.push_back((int)cell->type.index_); + + std::vector> 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> 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; + + 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) {} + + 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); + } + + 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); + + // Only consider FF cells for matching + dict> 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 gold_cells; + std::vector gate_cells; + }; + std::vector groups; + + 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}); + } + + if (groups.empty()) { + vlog("No structural FF matches found between `%s' and `%s'.\n", + gold_mod->name.c_str(), gate_mod->name.c_str()); + return; + } + + 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); + cone_idx++; + } + + gold_mod->fixup_ports(); + gate_mod->fixup_ports(); + + vlog("Cone partitioning: created %d POs and %d PIs.\n", + total_pos, total_pis); + } + +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 &gold_cells, + const std::vector &gate_cells, + int cone_idx) + { + 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 &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; + + // Fresh internal wire so the FF is isolated + std::string q_int_name = stringf("\\cone_%d_q_%d", cone_idx, ff_idx); + Wire *q_int = mod->addWire(q_int_name, q_width); + + // Redirect the FF's Q to the internal wire + cell->setPort(ID::Q, SigSpec(q_int)); + + // Old Q wire is now driven by the PI (downstream consumers get PI) + mod->connect(old_q, SigSpec(pi_wire)); + + // PO observes the FF's actual output (only need one) + if (!po_connected) { + mod->connect(SigSpec(po_wire), SigSpec(q_int)); + po_connected = true; + } + + ff_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("The result is a pair of modules where each matched FF cone is individually\n"); + log("observable through dedicated PI/PO ports, suitable for per-cone\n"); + log("equivalence checking.\n"); + log("\n"); + log(" -v\n"); + log(" verbose output: log each created port\n"); + log("\n"); + log(" -o \n"); + log(" write verbose log output to 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 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 From 59dd03973e0eb52544354d5d3331e106c2cb6276 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 20 Mar 2026 10:37:47 -0700 Subject: [PATCH 13/27] Added printing differnt clock domains in signal map --- passes/techmap/abc.cc | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 1df3d9027..df68ebd78 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -288,6 +288,10 @@ struct RunAbcState { DeferredLogs logs; dict 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 &process_pool); }; @@ -1140,6 +1144,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) { @@ -1231,11 +1239,16 @@ void RunAbcState::run(ConcurrentStack &process_pool) 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(), "wt"); + 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 { - fprintf(mf, "# ABC signal name -> Yosys signal name\n"); + 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)) From e2a641f5a8e945ce71fb379a93eebad4b7bbaa04 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 20 Mar 2026 11:32:06 -0700 Subject: [PATCH 14/27] Added support for printing the cdc map file --- passes/techmap/abc.cc | 38 ++++++++++++++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 4 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index df68ebd78..66ea5e7dd 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -149,6 +149,7 @@ struct AbcConfig 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; }; struct AbcSigVal { @@ -1868,7 +1869,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 *> &cell_sets, - AbcSigMap &assign_map) + AbcSigMap &assign_map, const std::string &cdc_file) { pool cells_in_no_set; for (RTLIL::Cell *cell : module->cells()) { @@ -1877,6 +1878,8 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vector signal_cell_set; + // Maps each signal that crosses clock domains to the pair of domain indices it bridges. + dict> 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); @@ -1887,6 +1890,7 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vectorsecond >= 0 && it->second != i) { + clock_domain_cross_signal_map[bit] = {it->second, i}; it->second = -1; assign_map.addVal(bit, AbcSigVal(true)); } @@ -1899,11 +1903,29 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vectorsecond >= 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 { @@ -2098,6 +2120,10 @@ struct AbcPass : public Pass { 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 \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(" -reserved_cores \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"); @@ -2314,6 +2340,10 @@ struct AbcPass : public Pass { config.signal_map_file = args[++argidx]; continue; } + if (arg == "-cdc_map" && argidx+1 < args.size()) { + config.cdc_file = args[++argidx]; + continue; + } break; } extra_args(args, argidx, design); @@ -2557,7 +2587,7 @@ struct AbcPass : public Pass { // Populate assign_map with cell connections std::vector 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); @@ -2858,7 +2888,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 From 2fc0591b2cbe767229e24958476fa7d448d427a0 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 20 Mar 2026 12:42:24 -0700 Subject: [PATCH 15/27] Added clkmerge pass --- passes/silimate/clkmerge.cc | 136 ++++++++++++++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 passes/silimate/clkmerge.cc diff --git a/passes/silimate/clkmerge.cc b/passes/silimate/clkmerge.cc new file mode 100644 index 000000000..fc03ff4db --- /dev/null +++ b/passes/silimate/clkmerge.cc @@ -0,0 +1,136 @@ +/* + * 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 ] [selection]\n"); + log("\n"); + log("This command rewrites all flip-flop clock ports in the selected modules to\n"); + log("use a single clock signal, effectively merging all clock domains into one.\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 for what is logically the same\n"); + log("clock. Without merging, ABC's -dff mode will partition them into separate\n"); + log("clock domains, creating spurious cross-domain ports that degrade SAT\n"); + log("performance.\n"); + log("\n"); + log(" -target \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.\n"); + log("\n"); + } + void execute(std::vector 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); + + dict clk_domain_count; + std::vector> ff_clk_pairs; + + for (auto cell : module->selected_cells()) + { + if (!cell->is_builtin_ff()) + continue; + + FfData ff(nullptr, cell); + if (!ff.has_clk) + continue; + + SigSpec clk = sigmap(ff.sig_clk); + ff_clk_pairs.push_back({cell, clk}); + + for (auto bit : clk) + clk_domain_count[bit]++; + } + + if (ff_clk_pairs.empty()) + continue; + + // Determine target clock + SigSpec target_clk; + 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_clk_pairs[0].second; + } + + // Collect distinct clocks + pool all_clks; + for (auto &pair : ff_clk_pairs) + all_clks.insert(pair.second); + + if (all_clks.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\n", + log_id(module), GetSize(all_clks), log_signal(target_clk)); + + int rewritten = 0; + for (auto &pair : ff_clk_pairs) + { + Cell *cell = pair.first; + SigSpec old_clk = pair.second; + + if (old_clk == target_clk) + continue; + + // Fine-grain cells use ID::C, coarse-grain use ID::CLK + if (cell->hasPort(ID::C)) + cell->setPort(ID::C, target_clk); + else if (cell->hasPort(ID::CLK)) + cell->setPort(ID::CLK, target_clk); + + rewritten++; + } + + log(" Rewrote clock on %d flip-flops.\n", rewritten); + } + } +} ClkMergePass; + +PRIVATE_NAMESPACE_END From f9f31afcb453ca5f72a04f6dc0e622ea1a80df0c Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 20 Mar 2026 12:42:51 -0700 Subject: [PATCH 16/27] Makefile pass changes --- Makefile | 1 + passes/silimate/Makefile.inc | 1 + 2 files changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 6f3f3f247..083d33407 100644 --- a/Makefile +++ b/Makefile @@ -766,6 +766,7 @@ 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 diff --git a/passes/silimate/Makefile.inc b/passes/silimate/Makefile.inc index 86685e05a..f39b7af07 100644 --- a/passes/silimate/Makefile.inc +++ b/passes/silimate/Makefile.inc @@ -17,6 +17,7 @@ OBJS += passes/silimate/splitnetlist.o OBJS += passes/silimate/opt_timing_balance.o OBJS += passes/silimate/struct_partition.o OBJS += passes/silimate/cone_partition.o +OBJS += passes/silimate/clkmerge.o OBJS += passes/silimate/opt_expand.o GENFILES += passes/silimate/peepopt_expand.h From b9ba2c3552d5ad2c0261f083f8400130a86e305a Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 20 Mar 2026 15:05:03 -0700 Subject: [PATCH 17/27] Checked out abc to the yosys-experimental branch --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index b232cbf52..bb9bc209f 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit b232cbf521eb6b78d16616bf5062543bdb9ca6eb +Subproject commit bb9bc209ff23e6690865935a70bcc9294101c5ce From f7a9af5252dda6f131831f3aa0844358a0285bf0 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Tue, 24 Mar 2026 14:39:21 -0700 Subject: [PATCH 18/27] Make the signal_map flag optional --- passes/techmap/abc.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 66ea5e7dd..a01fcd08d 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -2193,6 +2193,8 @@ 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", ""); if (config.cleanup) config.global_tempdir_name = get_base_tmpdir() + "/"; From 92e659f42a10b0074c27fe9847249d9868396182 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Tue, 24 Mar 2026 20:00:24 -0700 Subject: [PATCH 19/27] Added new port outputs anding the clock domain. TODO: fix if they belong to the same one and there's multiple --- passes/silimate/clkmerge.cc | 113 +++++++++----- passes/silimate/cone_partition.cc | 235 ++++++++++++++++++++++++++++-- 2 files changed, 297 insertions(+), 51 deletions(-) diff --git a/passes/silimate/clkmerge.cc b/passes/silimate/clkmerge.cc index fc03ff4db..ce78234da 100644 --- a/passes/silimate/clkmerge.cc +++ b/passes/silimate/clkmerge.cc @@ -32,18 +32,20 @@ struct ClkMergePass : public Pass { log("\n"); log(" clkmerge [-target ] [selection]\n"); log("\n"); - log("This command rewrites all flip-flop clock ports in the selected modules to\n"); - log("use a single clock signal, effectively merging all clock domains into one.\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 for what is logically the same\n"); - log("clock. Without merging, ABC's -dff mode will partition them into separate\n"); - log("clock domains, creating spurious cross-domain ports that degrade SAT\n"); - log("performance.\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 \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.\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 args, RTLIL::Design *design) override @@ -64,8 +66,13 @@ struct ClkMergePass : public Pass { { SigMap sigmap(module); - dict clk_domain_count; - std::vector> ff_clk_pairs; + struct FfInfo { + Cell *cell; + SigSpec clk; + bool pol_clk; + }; + + std::vector ff_list; for (auto cell : module->selected_cells()) { @@ -76,59 +83,93 @@ struct ClkMergePass : public Pass { if (!ff.has_clk) continue; - SigSpec clk = sigmap(ff.sig_clk); - ff_clk_pairs.push_back({cell, clk}); - - for (auto bit : clk) - clk_domain_count[bit]++; + ff_list.push_back({cell, sigmap(ff.sig_clk), ff.pol_clk}); } - if (ff_clk_pairs.empty()) + if (ff_list.empty()) continue; - // Determine target clock + // 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_clk_pairs[0].second; + target_clk = ff_list[0].clk; + target_pol = ff_list[0].pol_clk; } - // Collect distinct clocks - pool all_clks; - for (auto &pair : ff_clk_pairs) - all_clks.insert(pair.second); + // Collect distinct (signal, polarity) pairs + pool> all_domains; + for (auto &info : ff_list) + all_domains.insert({info.clk, info.pol_clk}); - if (all_clks.size() <= 1) { + 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\n", - log_id(module), GetSize(all_clks), log_signal(target_clk)); + log("Module %s: merging %d clock domains into %s%s\n", + log_id(module), GetSize(all_domains), + target_pol ? "" : "!", log_signal(target_clk)); - int rewritten = 0; - for (auto &pair : ff_clk_pairs) + 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 = pair.first; - SigSpec old_clk = pair.second; + Cell *cell = info.cell; + bool needs_clk_change = (info.clk != target_clk); + bool needs_pol_change = (info.pol_clk != target_pol); - if (old_clk == target_clk) + if (!needs_clk_change && !needs_pol_change) continue; - // Fine-grain cells use ID::C, coarse-grain use ID::CLK - if (cell->hasPort(ID::C)) - cell->setPort(ID::C, target_clk); - else if (cell->hasPort(ID::CLK)) - cell->setPort(ID::CLK, target_clk); + 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++; + } - 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 on %d flip-flops.\n", rewritten); + log(" Rewrote clock signal on %d FFs, polarity on %d FFs.\n", + clk_rewritten, pol_rewritten); } } } ClkMergePass; diff --git a/passes/silimate/cone_partition.cc b/passes/silimate/cone_partition.cc index 7007f7b57..53834a06d 100644 --- a/passes/silimate/cone_partition.cc +++ b/passes/silimate/cone_partition.cc @@ -21,6 +21,17 @@ * 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. @@ -44,6 +55,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "kernel/celltypes.h" +#include "kernel/ff.h" #include "kernel/log.h" #include @@ -252,10 +264,54 @@ struct ConePartitionWorker { 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_ 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, int> clk_domain_to_guard; + int next_guard_idx = 0; + dict, 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); @@ -268,6 +324,20 @@ struct ConePartitionWorker { log("%s", buf); } + // Collect the set of clock domains (clk_signal, polarity) for all FFs in a module. + pool> collect_clock_domains(ModuleAnalysis &analysis, SigMap &sigmap) { + pool> 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; @@ -279,6 +349,43 @@ struct ConePartitionWorker { 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> gold_ff_by_hash, gate_ff_by_hash; for (auto &[cell, h] : gold_analysis.cell_hash) @@ -294,32 +401,62 @@ struct ConePartitionWorker { }; std::vector groups; + pool 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()); - return; + } else { + vlog("Found %d structurally matched FF groups.\n", (int)groups.size()); } - 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); + 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 and %d PIs.\n", - total_pos, total_pis); + vlog("Cone partitioning: created %d POs, %d PIs, %d clock guard PIs.\n", + total_pos, total_pis, total_guards); } private: @@ -334,7 +471,9 @@ private: void expose_matched_ff_group( const std::vector &gold_cells, const std::vector &gate_cells, - int cone_idx) + int cone_idx, + SigMap &/*gold_sigmap*/, + SigMap &/*gate_sigmap*/) { if (gold_cells.empty() || gate_cells.empty()) return; @@ -347,10 +486,11 @@ private: std::string pi_name = stringf("\\cone_%d_ff_pi", cone_idx); std::string po_name = stringf("\\cone_%d_po", cone_idx); - if (verbose) + 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); @@ -379,17 +519,13 @@ private: if (GetSize(old_q) != q_width) continue; - // Fresh internal wire so the FF is isolated std::string q_int_name = stringf("\\cone_%d_q_%d", cone_idx, ff_idx); Wire *q_int = mod->addWire(q_int_name, q_width); - // Redirect the FF's Q to the internal wire cell->setPort(ID::Q, SigSpec(q_int)); - // Old Q wire is now driven by the PI (downstream consumers get PI) mod->connect(old_q, SigSpec(pi_wire)); - // PO observes the FF's actual output (only need one) if (!po_connected) { mod->connect(SigSpec(po_wire), SigSpec(q_int)); po_connected = true; @@ -399,6 +535,59 @@ private: } } + // 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); + } + } + }; // --------------------------------------------------------------------------- @@ -428,9 +617,25 @@ struct ConePartitionPass : public Pass { 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("The result is a pair of modules where each matched FF cone is individually\n"); - log("observable through dedicated PI/PO ports, suitable for per-cone\n"); - log("equivalence checking.\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"); From f84fd46a17f4fd1f3c96f97e8f55aa4f96676c8e Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Wed, 25 Mar 2026 15:06:58 -0700 Subject: [PATCH 20/27] Added test cases for clkmerge and cone_partition passes --- tests/silimate/clkmerge.ys | 316 +++++++++++++++ tests/silimate/cone_partition.ys | 363 ++++++++++++++++++ tests/silimate/cone_partition_clk_mismatch.ys | 23 ++ .../silimate/cone_partition_port_mismatch.ys | 17 + 4 files changed, 719 insertions(+) create mode 100644 tests/silimate/clkmerge.ys create mode 100644 tests/silimate/cone_partition.ys create mode 100644 tests/silimate/cone_partition_clk_mismatch.ys create mode 100644 tests/silimate/cone_partition_port_mismatch.ys diff --git a/tests/silimate/clkmerge.ys b/tests/silimate/clkmerge.ys new file mode 100644 index 000000000..e3c7a52c8 --- /dev/null +++ b/tests/silimate/clkmerge.ys @@ -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 < Date: Fri, 20 Mar 2026 15:00:17 -0700 Subject: [PATCH 21/27] Added initial clkmerge pass for multiple clock domains --- passes/silimate/clkmerge.cc | 136 ++++++++++++++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 passes/silimate/clkmerge.cc diff --git a/passes/silimate/clkmerge.cc b/passes/silimate/clkmerge.cc new file mode 100644 index 000000000..fc03ff4db --- /dev/null +++ b/passes/silimate/clkmerge.cc @@ -0,0 +1,136 @@ +/* + * 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 ] [selection]\n"); + log("\n"); + log("This command rewrites all flip-flop clock ports in the selected modules to\n"); + log("use a single clock signal, effectively merging all clock domains into one.\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 for what is logically the same\n"); + log("clock. Without merging, ABC's -dff mode will partition them into separate\n"); + log("clock domains, creating spurious cross-domain ports that degrade SAT\n"); + log("performance.\n"); + log("\n"); + log(" -target \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.\n"); + log("\n"); + } + void execute(std::vector 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); + + dict clk_domain_count; + std::vector> ff_clk_pairs; + + for (auto cell : module->selected_cells()) + { + if (!cell->is_builtin_ff()) + continue; + + FfData ff(nullptr, cell); + if (!ff.has_clk) + continue; + + SigSpec clk = sigmap(ff.sig_clk); + ff_clk_pairs.push_back({cell, clk}); + + for (auto bit : clk) + clk_domain_count[bit]++; + } + + if (ff_clk_pairs.empty()) + continue; + + // Determine target clock + SigSpec target_clk; + 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_clk_pairs[0].second; + } + + // Collect distinct clocks + pool all_clks; + for (auto &pair : ff_clk_pairs) + all_clks.insert(pair.second); + + if (all_clks.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\n", + log_id(module), GetSize(all_clks), log_signal(target_clk)); + + int rewritten = 0; + for (auto &pair : ff_clk_pairs) + { + Cell *cell = pair.first; + SigSpec old_clk = pair.second; + + if (old_clk == target_clk) + continue; + + // Fine-grain cells use ID::C, coarse-grain use ID::CLK + if (cell->hasPort(ID::C)) + cell->setPort(ID::C, target_clk); + else if (cell->hasPort(ID::CLK)) + cell->setPort(ID::CLK, target_clk); + + rewritten++; + } + + log(" Rewrote clock on %d flip-flops.\n", rewritten); + } + } +} ClkMergePass; + +PRIVATE_NAMESPACE_END From 972e4780c90167e154eb625b31ee3dc07062ff0f Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 26 Mar 2026 16:58:09 -0700 Subject: [PATCH 22/27] Removed extra struct partition pass --- passes/silimate/Makefile.inc | 1 - passes/silimate/struct_partition.cc | 650 ---------------------------- 2 files changed, 651 deletions(-) delete mode 100644 passes/silimate/struct_partition.cc diff --git a/passes/silimate/Makefile.inc b/passes/silimate/Makefile.inc index f39b7af07..7f94710b9 100644 --- a/passes/silimate/Makefile.inc +++ b/passes/silimate/Makefile.inc @@ -15,7 +15,6 @@ 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/struct_partition.o OBJS += passes/silimate/cone_partition.o OBJS += passes/silimate/clkmerge.o diff --git a/passes/silimate/struct_partition.cc b/passes/silimate/struct_partition.cc deleted file mode 100644 index 1c3aaa8b7..000000000 --- a/passes/silimate/struct_partition.cc +++ /dev/null @@ -1,650 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Structural-isomorphism partitioning for equivalence checking. - * - * Given two modules (typically named "gold" and "gate") with matching - * port signatures, this pass: - * - * 1. Builds a bottom-up structural hash for every cell in each module. - * The hash captures cell type, parameters, and the recursive structure - * of each input driver chain back to primary inputs. Wire and cell - * names are deliberately ignored — only connectivity and function - * matter. - * - * 2. Finds hash groups where cells from BOTH modules appear. Every cell - * in such a group computes the same Boolean function of the same - * primary inputs, so they are structurally equivalent. - * - * 3. For each matched group, replaces every cell's output in both - * modules with a shared new primary-input port (a "cutpoint"). - * The matched cells and all transitively dead fanin logic are then - * removed. - * - * The result is a pair of simplified modules whose remaining logic is - * exactly the part that differs — or that could not be structurally - * matched — ready to be fed into `miter -equiv` and a SAT/PDR solver. - * - * The key insight is that structurally identical subcircuits do not need - * to be proved equivalent by the solver; replacing them with free inputs - * shrinks the problem while preserving soundness. - * - * Algorithm notes - * --------------- - * - Primary inputs hash by their port name (shared between gold/gate). - * - Constants hash by their value. - * - Flip-flop Q outputs break feedback loops: when computing the hash - * of a FF, we do NOT recurse through Q. Instead, Q is treated as a - * fresh leaf ("secondary PI") in the downstream combinational cone. - * The FF itself IS hashed (by type + params + input drivers), so two - * structurally identical FFs will match. - * - The hash is a tuple-like structure (not a numeric hash), so there - * are no collisions — matching is exact. - * - * 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/log.h" -#include - -USING_YOSYS_NAMESPACE -PRIVATE_NAMESPACE_BEGIN - -// --------------------------------------------------------------------------- -// StructuralHash — collision-free structural identity -// --------------------------------------------------------------------------- -// -// Each cell's "structural hash" is a tree-shaped value that encodes: -// (cell_type, {parameters}, {port -> driver_hash, ...}) -// -// We serialise these trees into interned integer IDs so that comparison -// is O(1) after the initial bottom-up pass. Two cells get the same ID -// if and only if they are structurally identical. - -struct StructuralHasher { - // Intern table: canonical representation -> unique ID - dict, int> intern_table; - int next_id = 1; - - // Sentinel IDs for leaves - enum { CONST_BASE = -1000000, PI_BASE = -2000000, CYCLE_GUARD = 0 }; - - int intern(const std::vector &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; - } - - // Intern a primary-input bit identity. We use the port name AND bit - // index to generate a stable integer that is the same in both gold - // and gate. Each bit of a multi-bit port must get a distinct ID, - // otherwise cones differing only in which bit they read would - // incorrectly appear structurally identical. - dict, 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; - } - - // Intern a constant value. - dict 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 -// --------------------------------------------------------------------------- - -struct ModuleAnalysis { - RTLIL::Module *module; - SigMap sigmap; - CellTypes ct; - - // bit -> (cell, port) that drives it - dict> bit_driver; - - // cell -> structural hash ID - dict cell_hash; - - // Which SigBits are primary inputs (module input ports) - dict> pi_bits; // bit -> (port_name, bit_idx) - - // Set of cells being visited (cycle detection) - pool visiting; - - // Set of cells that are flip-flops / sequential - pool ff_cells; - - ModuleAnalysis(RTLIL::Module *mod, Design *design) : module(mod), sigmap(mod) { - ct.setup(design); - - // Record primary-input bits - 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}; - } - } - - // Build bit -> driver map - 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}; - } - } - } - } - - // Compute structural hash for a single SigBit - int hash_bit(SigBit bit, StructuralHasher &hasher) { - bit = sigmap(bit); - - // Constant - if (bit.wire == nullptr) - return hasher.intern_const(Const(bit.data)); - - // Primary input - 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); - - // Driven by a cell - 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; - - // For FFs, treat Q as a secondary PI (to break cycles). - // The FF itself will get its own hash via hash_cell. - if (ff_cells.count(drv_cell) && drv_port == ID::Q) { - int ff_hash = hash_cell(drv_cell, hasher); - // Encode "output bit i of ff with hash ff_hash" - 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 key = {ff_hash, bit_idx, -99}; - return hasher.intern(key); - } - - int ch = hash_cell(drv_cell, hasher); - // Multi-bit output: encode which bit of the output we're reading - 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 key = {ch, bit_idx, (int)drv_port.index_}; - return hasher.intern(key); - } - - // Undriven wire — treat as a unique unknown - return hasher.intern_const(Const(State::Sx)); - } - - // Compute structural hash for a SigSpec (multi-bit signal) - int hash_sig(const SigSpec &sig, StructuralHasher &hasher) { - SigSpec mapped = sigmap(sig); - if (GetSize(mapped) == 1) - return hash_bit(mapped[0], hasher); - - std::vector key; - key.reserve(GetSize(mapped) + 1); - key.push_back(-77); // tag for "concatenated signal" - for (auto &bit : mapped) - key.push_back(hash_bit(bit, hasher)); - return hasher.intern(key); - } - - // Compute structural hash for a cell - int hash_cell(Cell *cell, StructuralHasher &hasher) { - auto it = cell_hash.find(cell); - if (it != cell_hash.end()) - return it->second; - - // Cycle guard - if (visiting.count(cell)) { - cell_hash[cell] = StructuralHasher::CYCLE_GUARD; - return StructuralHasher::CYCLE_GUARD; - } - visiting.insert(cell); - - // Build the key: cell_type, sorted parameters, sorted input hashes - std::vector key; - - // Cell type - key.push_back((int)cell->type.index_); - - // Parameters (sorted by name for determinism) - std::vector> 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); // separator - for (auto &[pname, pval] : sorted_params) { - key.push_back((int)pname.index_); - key.push_back(hasher.intern_const(pval)); - } - - // Input connections (sorted by port name) - key.push_back(-99); // separator - std::vector> 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; - } - - // Hash all cells in the module - void hash_all_cells(StructuralHasher &hasher) { - for (auto cell : module->cells()) - hash_cell(cell, hasher); - } -}; - -// --------------------------------------------------------------------------- -// Core: find matches and apply cutpoints -// --------------------------------------------------------------------------- - -struct StructPartitionWorker { - Design *design; - Module *gold_mod; - Module *gate_mod; - bool verbose; - FILE *log_file; - - int total_cutpoints = 0; - int total_cells_removed = 0; - - StructPartitionWorker(Design *d, Module *gold, Module *gate, bool v, FILE *lf = nullptr) - : design(d), gold_mod(gold), gate_mod(gate), verbose(v), log_file(lf) {} - - 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); - } - - void run() { - // A single shared hasher ensures the same intern IDs across both modules - StructuralHasher hasher; - - vlog("Structural partitioning: analyzing module `%s'.\n", gold_mod->name.c_str()); - ModuleAnalysis gold_analysis(gold_mod, design); - gold_analysis.hash_all_cells(hasher); - - vlog("Structural partitioning: analyzing module `%s'.\n", gate_mod->name.c_str()); - ModuleAnalysis gate_analysis(gate_mod, design); - gate_analysis.hash_all_cells(hasher); - - // Group cells by structural hash across both modules - dict> gold_by_hash, gate_by_hash; - for (auto &[cell, h] : gold_analysis.cell_hash) - if (h != StructuralHasher::CYCLE_GUARD) - gold_by_hash[h].push_back(cell); - for (auto &[cell, h] : gate_analysis.cell_hash) - if (h != StructuralHasher::CYCLE_GUARD) - gate_by_hash[h].push_back(cell); - - // Find hashes present in BOTH modules — these are the structural matches. - // ALL cells with a matching hash (in both modules) get the same cutpoint. - struct CutpointGroup { - std::vector gold_cells; - std::vector gate_cells; - }; - std::vector groups; - - for (auto &[h, gold_cells] : gold_by_hash) { - auto it = gate_by_hash.find(h); - if (it == gate_by_hash.end()) - continue; - groups.push_back({gold_cells, it->second}); - } - - if (groups.empty()) { - vlog("No structural matches found between `%s' and `%s'.\n", - gold_mod->name.c_str(), gate_mod->name.c_str()); - return; - } - - vlog("Found %d structurally matched groups.\n", (int)groups.size()); - - // For each group, create cutpoint PIs and rewire - for (auto &group : groups) - apply_cutpoint_group(group.gold_cells, group.gate_cells, - gold_analysis, gate_analysis); - - // Remove transitively dead cells from both modules - remove_dead_cells(gold_mod); - remove_dead_cells(gate_mod); - - gold_mod->fixup_ports(); - gate_mod->fixup_ports(); - - vlog("Structural partitioning: created %d cutpoints, removed %d cells.\n", - total_cutpoints, total_cells_removed); - } - -private: - // Create a cutpoint for one matched group. - // - // Every cell in gold_cells and gate_cells computes the same function. - // We pick the output port(s) of the cell type, create a fresh input - // port with the same width on BOTH modules (same name), and rewire - // all the cells' outputs to that port. Then we remove the cells. - void apply_cutpoint_group( - const std::vector &gold_cells, - const std::vector &gate_cells, - ModuleAnalysis &/*gold_an*/, - ModuleAnalysis &/*gate_an*/) - { - if (gold_cells.empty() || gate_cells.empty()) - return; - - Cell *representative = gold_cells[0]; - - // Determine output ports for this cell type - std::vector out_ports; - for (auto &conn : representative->connections()) - if (representative->output(conn.first)) - out_ports.push_back(conn.first); - - if (out_ports.empty()) - return; - - for (auto out_port : out_ports) { - SigSpec rep_sig = representative->getPort(out_port); - int width = GetSize(rep_sig); - if (width == 0) - continue; - - // Create a unique cutpoint name - std::string cut_name = stringf("\\cut_%d", total_cutpoints); - total_cutpoints++; - - if (verbose) - vlog(" Cutpoint %s (width %d) for %d+%d cells of type %s.\n", - cut_name.c_str(), width, - (int)gold_cells.size(), (int)gate_cells.size(), - representative->type.c_str()); - - // Create the new input port on both modules - Wire *gold_cut = gold_mod->addWire(cut_name, width); - gold_cut->port_input = true; - - Wire *gate_cut = gate_mod->addWire(cut_name, width); - gate_cut->port_input = true; - - // Rewire all gold cells: connect their output to the cutpoint wire - for (auto cell : gold_cells) { - SigSpec old_sig = cell->getPort(out_port); - if (GetSize(old_sig) != width) continue; - gold_mod->connect(old_sig, gold_cut); - } - - // Rewire all gate cells: connect their output to the cutpoint wire - for (auto cell : gate_cells) { - SigSpec old_sig = cell->getPort(out_port); - if (GetSize(old_sig) != width) continue; - gate_mod->connect(old_sig, gate_cut); - } - } - - // Remove the matched cells - for (auto cell : gold_cells) { - if (verbose) - vlog(" Removing gold cell `%s'.\n", cell->name.c_str()); - gold_mod->remove(cell); - total_cells_removed++; - } - for (auto cell : gate_cells) { - if (verbose) - vlog(" Removing gate cell `%s'.\n", cell->name.c_str()); - gate_mod->remove(cell); - total_cells_removed++; - } - } - - // Remove cells whose outputs are entirely unconnected. - // Iterate to fixpoint since removing one cell may make its drivers dead. - void remove_dead_cells(Module *mod) { - SigMap sigmap(mod); - - bool changed = true; - while (changed) { - changed = false; - - // Collect all bits that are used as inputs somewhere - pool used_bits; - for (auto cell : mod->cells()) - for (auto &conn : cell->connections()) - if (cell->input(conn.first)) - for (auto bit : sigmap(conn.second)) - if (bit.wire) - used_bits.insert(bit); - - // Module output ports are "used" - for (auto wire : mod->wires()) - if (wire->port_output) - for (auto bit : sigmap(wire)) - used_bits.insert(bit); - - // Also count bits used in module-level connections (LHS = driven) - for (auto &conn : mod->connections()) { - for (auto bit : sigmap(conn.first)) - if (bit.wire) - used_bits.insert(bit); - for (auto bit : sigmap(conn.second)) - if (bit.wire) - used_bits.insert(bit); - } - - // Remove cells whose outputs are entirely unused - std::vector to_remove; - for (auto cell : mod->cells()) { - bool any_output_used = false; - bool has_output = false; - for (auto &conn : cell->connections()) { - if (!cell->output(conn.first)) - continue; - has_output = true; - for (auto bit : sigmap(conn.second)) { - if (used_bits.count(bit)) { - any_output_used = true; - break; - } - } - if (any_output_used) break; - } - // Only remove cells that have outputs but none are used. - // Keep cells with no outputs (side effects like $assert). - if (has_output && !any_output_used && !cell->has_keep_attr()) - to_remove.push_back(cell); - } - - for (auto cell : to_remove) { - if (verbose) - vlog(" Dead cell removal: `%s' (%s).\n", - cell->name.c_str(), cell->type.c_str()); - mod->remove(cell); - total_cells_removed++; - changed = true; - } - - if (changed) - sigmap.set(mod); - } - } -}; - -// --------------------------------------------------------------------------- -// Pass registration -// --------------------------------------------------------------------------- - -struct StructPartitionPass : public Pass { - StructPartitionPass() : Pass("struct_partition", - "partition equivalent subcircuits between two modules") { } - - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" struct_partition [options] gold_module gate_module\n"); - log("\n"); - log("This pass identifies structurally identical subcircuits between two modules\n"); - log("(typically a gold and gate design for equivalence checking) and replaces\n"); - log("matched logic with shared primary-input cutpoints.\n"); - log("\n"); - log("The structural matching is purely based on cell types, parameters, and\n"); - log("input connectivity — cell and wire names are ignored entirely.\n"); - log("\n"); - log("For each group of cells that are structurally identical across both modules,\n"); - log("ALL cells in the group are removed and their outputs are replaced by a new\n"); - log("input port with the same name in both modules. Transitively dead fanin\n"); - log("logic is also removed.\n"); - log("\n"); - log("This shrinks the subsequent `miter -equiv` + SAT/PDR problem by eliminating\n"); - log("logic that is provably identical by construction.\n"); - log("\n"); - log(" -v\n"); - log(" verbose output: log each cutpoint and removed cell\n"); - log("\n"); - log(" -o \n"); - log(" write verbose log output to 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(" struct_partition gold gate\n"); - log(" miter -equiv gold gate miter\n"); - log(" ...\n"); - log("\n"); - } - - void execute(std::vector args, RTLIL::Design *design) override - { - bool verbose = false; - std::string log_file_path; - - log_header(design, "Executing STRUCT_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()); - - // Verify port compatibility - 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()); - } - - StructPartitionWorker worker(design, gold_mod, gate_mod, verbose, log_file); - worker.run(); - - if (log_file) - fclose(log_file); - } -} StructPartitionPass; - -PRIVATE_NAMESPACE_END From 113b3e02ce4b707019a384f9515e93d878614f8f Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 26 Mar 2026 16:59:58 -0700 Subject: [PATCH 23/27] Removed adding struct partition object file --- passes/sat/Makefile.inc | 1 - 1 file changed, 1 deletion(-) diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index 11a415ba4..d9bf69dcb 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -15,7 +15,6 @@ OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o OBJS += passes/sat/cutpoint.o -OBJS += passes/sat/struct_partition.o OBJS += passes/sat/fminit.o OBJS += passes/sat/recover_names.o ifeq ($(DISABLE_SPAWN),0) From 5c94a472987b3f9b32fb1c4674b7fc1aee18e0cf Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Thu, 26 Mar 2026 17:02:57 -0700 Subject: [PATCH 24/27] moved verific to main head --- verific | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/verific b/verific index 4feaf1f92..87cb8cf50 160000 --- a/verific +++ b/verific @@ -1 +1 @@ -Subproject commit 4feaf1f923157af0ed064eab8e302647bd5fa1b7 +Subproject commit 87cb8cf50448c4d28a1b2d57bd4afc119b6439af From 20cf9fb4611333d6e18eac86fcdd63e5cda4d9e2 Mon Sep 17 00:00:00 2001 From: Advay Singh <144560982+AdvaySingh1@users.noreply.github.com> Date: Fri, 27 Mar 2026 12:45:57 -0700 Subject: [PATCH 25/27] Update passes/techmap/abc.cc Co-authored-by: greptile-apps[bot] <165735046+greptile-apps[bot]@users.noreply.github.com> --- passes/techmap/abc.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index a01fcd08d..c414e34aa 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -1242,7 +1242,7 @@ void RunAbcState::run(ConcurrentStack &process_pool) 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)); + logs.log("Opening %s for writing failed: %s\n", config.signal_map_file.c_str(), strerror(errno)); } else { if (clk_sig.size() != 0) { std::string clk_str = log_signal(clk_sig); From ad6546b05e79c69c6f39eb3895b1662837fd5d56 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 27 Mar 2026 14:53:38 -0700 Subject: [PATCH 26/27] Revert "Update passes/techmap/abc.cc" This reverts commit 20cf9fb4611333d6e18eac86fcdd63e5cda4d9e2. --- passes/techmap/abc.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index c414e34aa..a01fcd08d 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -1242,7 +1242,7 @@ void RunAbcState::run(ConcurrentStack &process_pool) 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.c_str(), strerror(errno)); + 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); From 8aebec79a850276c3d32b2935900e75d3951c065 Mon Sep 17 00:00:00 2001 From: AdvaySingh1 Date: Fri, 27 Mar 2026 15:41:44 -0700 Subject: [PATCH 27/27] Added -filter_non_trigger_outputs knob --- passes/techmap/abc.cc | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index a01fcd08d..529888e7f 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -150,6 +150,7 @@ struct AbcConfig 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 { @@ -1214,14 +1215,15 @@ void RunAbcState::run(ConcurrentStack &process_pool) fprintf(f, " dummy_input\n"); fprintf(f, "\n"); - // Only keep the output port whose signal originates from the miter equiv NOT cell - 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; + 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; @@ -1229,7 +1231,7 @@ void RunAbcState::run(ConcurrentStack &process_pool) 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)) + 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; @@ -2124,6 +2126,10 @@ struct AbcPass : public Pass { 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 \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"); @@ -2195,6 +2201,7 @@ struct AbcPass : public Pass { 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() + "/"; @@ -2346,6 +2353,10 @@ struct AbcPass : public Pass { 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);