diff --git a/Makefile b/Makefile index ec93a0bb6..083d33407 100644 --- a/Makefile +++ b/Makefile @@ -763,6 +763,10 @@ include $(YOSYS_SRC)/passes/silimate/Makefile.inc OBJS += passes/sat/recover_names.o OBJS += passes/sat/sim.o +OBJS += passes/sat/sat.o +OBJS += passes/sat/miter.o +OBJS += passes/sat/async2sync.o +OBJS += passes/sat/clk2fflogic.o OBJS += passes/techmap/extract.o OBJS += passes/techmap/extract_reduce.o OBJS += passes/techmap/alumacc.o @@ -773,6 +777,8 @@ OBJS += passes/techmap/muxcover.o OBJS += passes/techmap/aigmap.o OBJS += passes/techmap/attrmap.o OBJS += passes/techmap/clockgate.o +OBJS += passes/techmap/dffunmap.o +OBJS += passes/techmap/zinit.o include $(YOSYS_SRC)/passes/hierarchy/Makefile.inc include $(YOSYS_SRC)/passes/memory/Makefile.inc @@ -785,6 +791,7 @@ include $(YOSYS_SRC)/passes/techmap/Makefile.inc include $(YOSYS_SRC)/backends/verilog/Makefile.inc include $(YOSYS_SRC)/backends/rtlil/Makefile.inc include $(YOSYS_SRC)/backends/json/Makefile.inc +include $(YOSYS_SRC)/backends/blif/Makefile.inc include $(YOSYS_SRC)/techlibs/common/Makefile.inc diff --git a/passes/silimate/Makefile.inc b/passes/silimate/Makefile.inc index f57fcab15..7f94710b9 100644 --- a/passes/silimate/Makefile.inc +++ b/passes/silimate/Makefile.inc @@ -15,6 +15,8 @@ OBJS += passes/silimate/splitfanout.o OBJS += passes/silimate/splitlarge.o OBJS += passes/silimate/splitnetlist.o OBJS += passes/silimate/opt_timing_balance.o +OBJS += passes/silimate/cone_partition.o +OBJS += passes/silimate/clkmerge.o OBJS += passes/silimate/opt_expand.o GENFILES += passes/silimate/peepopt_expand.h diff --git a/passes/silimate/clkmerge.cc b/passes/silimate/clkmerge.cc new file mode 100644 index 000000000..ce78234da --- /dev/null +++ b/passes/silimate/clkmerge.cc @@ -0,0 +1,177 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2026 Silimate Inc. + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/ff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct ClkMergePass : public Pass { + ClkMergePass() : Pass("clkmerge", "merge multiple clock domains into one") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" clkmerge [-target ] [selection]\n"); + log("\n"); + log("This command rewrites all flip-flop clock ports and polarities in the\n"); + log("selected modules to use a single clock domain, merging both different\n"); + log("clock signals and different clock polarities (posedge vs negedge).\n"); + log("\n"); + log("This is useful for miter-based equivalence checking where gold and gate\n"); + log("copies may use different clock signal names or opposite edges for what\n"); + log("is logically the same clock. Without merging, ABC's -dff mode will\n"); + log("partition them into separate clock domains, creating spurious cross-domain\n"); + log("ports that degrade SAT performance.\n"); + log("\n"); + log(" -target \n"); + log(" use the specified signal as the merged clock. if not given, the\n"); + log(" clock signal of the first FF encountered is used. all FFs will\n"); + log(" be set to positive-edge triggered on this signal.\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *design) override + { + std::string target_clk_name; + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-target" && argidx + 1 < args.size()) { + target_clk_name = args[++argidx]; + continue; + } + break; + } + extra_args(args, argidx, design); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + + struct FfInfo { + Cell *cell; + SigSpec clk; + bool pol_clk; + }; + + std::vector ff_list; + + for (auto cell : module->selected_cells()) + { + if (!cell->is_builtin_ff()) + continue; + + FfData ff(nullptr, cell); + if (!ff.has_clk) + continue; + + ff_list.push_back({cell, sigmap(ff.sig_clk), ff.pol_clk}); + } + + if (ff_list.empty()) + continue; + + // Determine target clock signal and polarity + SigSpec target_clk; + bool target_pol = true; // default to posedge + + if (!target_clk_name.empty()) { + RTLIL::SigSpec sig; + if (!SigSpec::parse_sel(sig, design, module, target_clk_name)) + log_cmd_error("Failed to parse target clock expression '%s'.\n", target_clk_name.c_str()); + target_clk = sigmap(sig); + } else { + target_clk = ff_list[0].clk; + target_pol = ff_list[0].pol_clk; + } + + // Collect distinct (signal, polarity) pairs + pool> all_domains; + for (auto &info : ff_list) + all_domains.insert({info.clk, info.pol_clk}); + + if (all_domains.size() <= 1) { + log("Module %s: only one clock domain found, nothing to merge.\n", log_id(module)); + continue; + } + + log("Module %s: merging %d clock domains into %s%s\n", + log_id(module), GetSize(all_domains), + target_pol ? "" : "!", log_signal(target_clk)); + + for (auto &dom : all_domains) + log(" found domain: %s%s\n", + dom.second ? "" : "!", log_signal(dom.first)); + + int clk_rewritten = 0, pol_rewritten = 0; + for (auto &info : ff_list) + { + Cell *cell = info.cell; + bool needs_clk_change = (info.clk != target_clk); + bool needs_pol_change = (info.pol_clk != target_pol); + + if (!needs_clk_change && !needs_pol_change) + continue; + + if (needs_clk_change) { + if (cell->hasPort(ID::C)) + cell->setPort(ID::C, target_clk); + else if (cell->hasPort(ID::CLK)) + cell->setPort(ID::CLK, target_clk); + clk_rewritten++; + } + + if (needs_pol_change) { + // Coarse-grain FFs ($dff, $dffe, etc.) use CLK_POLARITY param + if (cell->hasParam(ID::CLK_POLARITY)) { + cell->setParam(ID::CLK_POLARITY, target_pol ? State::S1 : State::S0); + pol_rewritten++; + } + // Fine-grain FFs encode polarity in the type name, so + // we need to swap the cell type (e.g. $_DFF_N_ <-> $_DFF_P_) + else { + std::string type = cell->type.str(); + // Fine-grain FF types have P/N at position 6 for the clock polarity: + // $_DFF_P_, $_DFF_N_, $_DFFE_PP_, $_DFFE_NP_, etc. + // The clock polarity is always the first letter after "$_DFF_" or "$_DFFE_" + size_t pos = type.find("_DFF_"); + if (pos != std::string::npos) { + pos += 5; // skip "_DFF_" + if (pos < type.size()) { + if (type[pos] == 'P' && !target_pol) + type[pos] = 'N'; + else if (type[pos] == 'N' && target_pol) + type[pos] = 'P'; + cell->type = RTLIL::IdString(type); + pol_rewritten++; + } + } + } + } + } + + log(" Rewrote clock signal on %d FFs, polarity on %d FFs.\n", + clk_rewritten, pol_rewritten); + } + } +} ClkMergePass; + +PRIVATE_NAMESPACE_END diff --git a/passes/silimate/cone_partition.cc b/passes/silimate/cone_partition.cc new file mode 100644 index 000000000..53834a06d --- /dev/null +++ b/passes/silimate/cone_partition.cc @@ -0,0 +1,716 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Cone partitioning for equivalence checking. + * + * Given two modules (typically "gold" and "gate") with matching port + * signatures, this pass: + * + * 1. Builds bottom-up structural hashes for every cell in each module + * (identical algorithm to struct_partition). + * + * 2. Finds hash groups where FF cells from BOTH modules match — these + * are structurally equivalent sequential boundaries. + * + * 3. For each matched FF group: + * - The FF's Q output is disconnected from the rest of the circuit + * and exposed as a new output port (PO). + * - A new input port (PI) is created to replace the FF's Q output + * for any downstream logic that was consuming it. + * - The cone's transitive fanin is traced backwards, stopping at + * existing module PIs or at other matched FFs (whose PIs are + * reused). Any other leaf signals become new PIs. + * + * 4. Multi-clock-domain handling: + * - If both gold and gate have multiple clock domains, unmatched + * FFs (those not in any structural cone) are individually + * exposed as PI/PO pairs with the PO ANDed with a 1-bit clock + * guard PI for the FF's clock domain. + * - If only one module has multiple clock domains while the other + * has one, the pass errors out declaring the designs inequivalent. + * - Each unique (clock_signal, polarity) pair gets one guard PI + * (\clkguard_N). The guard ensures the SAT solver treats FFs in + * different domains as distinguishable even after clkmerge. + * + * The result is a pair of modules where every structurally matched + * FF cone is individually observable through its own PI/PO pair, ready + * for per-cone equivalence checking. + * + * Copyright (C) 2025 Silimate Inc. + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + +#include "kernel/yosys.h" +#include "kernel/sigtools.h" +#include "kernel/celltypes.h" +#include "kernel/ff.h" +#include "kernel/log.h" +#include + +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; + 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); + char buf[4096]; + vsnprintf(buf, sizeof(buf), fmt, ap); + va_end(ap); + if (log_file) + fputs(buf, log_file); + else + log("%s", buf); + } + + // Collect the set of clock domains (clk_signal, polarity) for all FFs in a module. + pool> 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; + + vlog("Cone partitioning: analyzing module `%s'.\n", gold_mod->name.c_str()); + ModuleAnalysis gold_analysis(gold_mod, design); + gold_analysis.hash_all_cells(hasher); + + vlog("Cone partitioning: analyzing module `%s'.\n", gate_mod->name.c_str()); + ModuleAnalysis gate_analysis(gate_mod, design); + gate_analysis.hash_all_cells(hasher); + + SigMap gold_sigmap(gold_mod); + SigMap gate_sigmap(gate_mod); + + // Collect clock domains from each module + auto gold_domains = collect_clock_domains(gold_analysis, gold_sigmap); + auto gate_domains = collect_clock_domains(gate_analysis, gate_sigmap); + + bool gold_multi = gold_domains.size() > 1; + bool gate_multi = gate_domains.size() > 1; + + vlog("Gold module has %d clock domain(s), gate module has %d clock domain(s).\n", + (int)gold_domains.size(), (int)gate_domains.size()); + + if (gold_multi != gate_multi) { + vlog("ERROR: Clock domain count mismatch — gold has %d, gate has %d.\n", + (int)gold_domains.size(), (int)gate_domains.size()); + vlog("One module has multiple clock domains while the other does not.\n"); + vlog("The designs are NOT equivalent.\n"); + log_cmd_error("Designs are inequivalent: clock domain count mismatch " + "(gold=%d, gate=%d). One module has multiple clock domains " + "while the other does not.\n", + (int)gold_domains.size(), (int)gate_domains.size()); + return; + } + + bool multi_clock = gold_multi && gate_multi; + if (multi_clock) { + if (gold_domains != gate_domains) { + vlog("WARNING: Gold and gate have different clock domain sets.\n"); + for (auto &d : gold_domains) + vlog(" gold domain: %s%s\n", d.second ? "" : "!", d.first.c_str()); + for (auto &d : gate_domains) + vlog(" gate domain: %s%s\n", d.second ? "" : "!", d.first.c_str()); + } + vlog("Multi-clock mode: unmatched FFs will be guarded with clock domain PIs.\n"); + } + + // Only consider FF cells for matching + dict> 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; + + 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()); + } else { + vlog("Found %d structurally matched FF groups.\n", (int)groups.size()); + } + + int cone_idx = 0; + for (auto &group : groups) { + expose_matched_ff_group(group.gold_cells, group.gate_cells, + cone_idx, gold_sigmap, gate_sigmap); + cone_idx++; + } + + // In multi-clock mode, expose unmatched FFs with clock-domain guard ANDs. + // These are FFs that didn't end up in any cone (no hash match). Each + // unmatched FF gets its own PO, and that PO is ANDed with the clock + // guard PI for the FF's clock domain. + if (multi_clock) { + int unmatched_gold = 0, unmatched_gate = 0; + for (auto cell : gold_analysis.ff_cells) { + if (matched_gold_ffs.count(cell)) + continue; + int guard_idx = get_ff_guard_idx(cell, gold_sigmap); + expose_unmatched_ff(gold_mod, cell, cone_idx, guard_idx); + cone_idx++; + unmatched_gold++; + } + for (auto cell : gate_analysis.ff_cells) { + if (matched_gate_ffs.count(cell)) + continue; + int guard_idx = get_ff_guard_idx(cell, gate_sigmap); + expose_unmatched_ff(gate_mod, cell, cone_idx, guard_idx); + cone_idx++; + unmatched_gate++; + } + vlog("Multi-clock: guarded %d unmatched gold FFs, %d unmatched gate FFs.\n", + unmatched_gold, unmatched_gate); + } + + gold_mod->fixup_ports(); + gate_mod->fixup_ports(); + + vlog("Cone partitioning: created %d POs, %d PIs, %d clock guard PIs.\n", + total_pos, total_pis, total_guards); + } + +private: + // For a single matched FF group: + // 1. Create a PI wire (same name in both modules) to replace the FF's Q + // for all downstream consumers. + // 2. Create a PO wire (same name in both modules) that observes the FF's + // actual Q output. + // 3. Redirect each FF's Q port to a fresh internal wire so the FF is fully + // severed from the rest of the circuit. The internal wire drives only + // the PO. The old Q wire is now driven by the PI. + void expose_matched_ff_group( + const std::vector &gold_cells, + const std::vector &gate_cells, + int cone_idx, + SigMap &/*gold_sigmap*/, + SigMap &/*gate_sigmap*/) + { + if (gold_cells.empty() || gate_cells.empty()) + return; + + Cell *gold_rep = gold_cells[0]; + int q_width = GetSize(gold_rep->getPort(ID::Q)); + if (q_width == 0) + return; + + std::string pi_name = stringf("\\cone_%d_ff_pi", cone_idx); + std::string po_name = stringf("\\cone_%d_po", cone_idx); + + if (verbose) { + vlog(" Cone %d: PI %s, PO %s (width %d) for %d+%d FFs.\n", + cone_idx, pi_name.c_str(), po_name.c_str(), q_width, + (int)gold_cells.size(), (int)gate_cells.size()); + } + + rewire_ff_group(gold_mod, gold_cells, pi_name, po_name, q_width, cone_idx); + rewire_ff_group(gate_mod, gate_cells, pi_name, po_name, q_width, cone_idx); + + total_pis++; + total_pos++; + } + + void rewire_ff_group(Module *mod, const std::vector &ff_cells, + const std::string &pi_name, const std::string &po_name, + int q_width, int cone_idx) + { + if (mod->wire(pi_name) || mod->wire(po_name)) + return; + + Wire *pi_wire = mod->addWire(pi_name, q_width); + pi_wire->port_input = true; + + Wire *po_wire = mod->addWire(po_name, q_width); + po_wire->port_output = true; + + bool po_connected = false; + int ff_idx = 0; + for (auto cell : ff_cells) { + SigSpec old_q = cell->getPort(ID::Q); + if (GetSize(old_q) != q_width) + continue; + + std::string q_int_name = stringf("\\cone_%d_q_%d", cone_idx, ff_idx); + Wire *q_int = mod->addWire(q_int_name, q_width); + + cell->setPort(ID::Q, SigSpec(q_int)); + + mod->connect(old_q, SigSpec(pi_wire)); + + if (!po_connected) { + mod->connect(SigSpec(po_wire), SigSpec(q_int)); + po_connected = true; + } + + ff_idx++; + } + } + + // Expose a single unmatched FF (one not in any cone) as its own PI/PO pair, + // with the PO ANDed with the clock-domain guard PI. This ensures the SAT + // solver sees the FF's domain even though no structural cone was created. + void expose_unmatched_ff(Module *mod, Cell *cell, int cone_idx, + int guard_idx) + { + SigSpec old_q = cell->getPort(ID::Q); + int q_width = GetSize(old_q); + if (q_width == 0) + return; + + std::string pi_name = stringf("\\ucone_%d_ff_pi", cone_idx); + std::string po_name = stringf("\\ucone_%d_po", cone_idx); + + if (mod->wire(pi_name) || mod->wire(po_name)) + return; + + Wire *pi_wire = mod->addWire(pi_name, q_width); + pi_wire->port_input = true; + + Wire *po_wire = mod->addWire(po_name, q_width); + po_wire->port_output = true; + + std::string q_int_name = stringf("\\ucone_%d_q", cone_idx); + Wire *q_int = mod->addWire(q_int_name, q_width); + + cell->setPort(ID::Q, SigSpec(q_int)); + mod->connect(old_q, SigSpec(pi_wire)); + + if (guard_idx >= 0) { + Wire *guard_pi = get_or_create_guard_pi(mod, guard_idx); + Wire *guarded = mod->addWire( + stringf("\\ucone_%d_guarded", cone_idx), q_width); + SigSpec guard_bits; + for (int i = 0; i < q_width; i++) + guard_bits.append(SigBit(guard_pi, 0)); + mod->addAnd(stringf("\\ucone_%d_clkand", cone_idx), + SigSpec(q_int), guard_bits, SigSpec(guarded)); + mod->connect(SigSpec(po_wire), SigSpec(guarded)); + } else { + mod->connect(SigSpec(po_wire), SigSpec(q_int)); + } + + total_pis++; + total_pos++; + + if (verbose) { + vlog(" Unmatched FF %s in %s: PI %s, PO %s (width %d) [guard=%d].\n", + cell->name.c_str(), mod->name.c_str(), + pi_name.c_str(), po_name.c_str(), q_width, guard_idx); + } + } + +}; + +// --------------------------------------------------------------------------- +// Pass registration +// --------------------------------------------------------------------------- + +struct ConePartitionPass : public Pass { + ConePartitionPass() : Pass("cone_partition", + "expose matched structural cones as PI/PO pairs") { } + + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" cone_partition [options] gold_module gate_module\n"); + log("\n"); + log("This pass identifies structurally identical flip-flop cones between two\n"); + log("modules (typically a gold and gate design) using the same hashing algorithm\n"); + log("as struct_partition, then exposes each matched cone's boundary as ports:\n"); + log("\n"); + log(" - Each matched FF's Q output is disconnected from the circuit and\n"); + log(" exposed as a new output port (PO).\n"); + log(" - A new input port (PI) replaces the FF's Q output for any downstream\n"); + log(" consumers.\n"); + log(" - The cone's transitive fanin (back through combinational logic) is\n"); + log(" traced until it reaches a module PI, an unmatched FF boundary, or\n"); + log(" another matched FF (whose replacement PI is reused). Leaf signals\n"); + log(" at the cone boundary become new input ports.\n"); + log("\n"); + log("Multi-clock-domain handling:\n"); + log("\n"); + log(" The pass collects the set of clock domains (signal + polarity) from\n"); + log(" all FFs in each module. Three cases:\n"); + log("\n"); + log(" 1. Both modules have a single clock domain (or no clocked FFs):\n"); + log(" no special handling; cones are created as above.\n"); + log("\n"); + log(" 2. Only ONE module has multiple clock domains while the other has\n"); + log(" one: the pass errors out, declaring the designs inequivalent.\n"); + log(" A design cannot gain/lose clock domains and still be equivalent.\n"); + log("\n"); + log(" 3. Both modules have multiple clock domains: after creating cones\n"); + log(" for structurally matched FFs (as above), every UNMATCHED FF\n"); + log(" (one that did not belong to any cone) is individually exposed\n"); + log(" as its own PI/PO pair. The PO is ANDed with a 1-bit clock-\n"); + log(" domain guard PI (clkguard_N) for the FF's domain. This ensures\n"); + log(" the downstream SAT solver treats FFs in different domains as\n"); + log(" distinguishable even after clkmerge unifies clock signals.\n"); + log("\n"); + log(" -v\n"); + log(" verbose output: log each created port\n"); + log("\n"); + log(" -o \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 diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 9e8e3f3a2..529888e7f 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -148,6 +148,9 @@ struct AbcConfig int reserved_cores = 4; // cores reserved for main thread and other work bool abc_node_retention = false; // retain nodes in ABC (off by default) int abc_max_node_retention_origins = 5; // number of node retention origins (default 5) + std::string signal_map_file; + std::string cdc_file; + bool filter_non_trigger_outputs = false; }; struct AbcSigVal { @@ -287,6 +290,10 @@ struct RunAbcState { DeferredLogs logs; dict 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); }; @@ -1139,6 +1146,10 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module mark_port(assign_map, srst_sig); handle_loops(assign_map, module); + + run_abc.state_index = state_index; + run_abc.clk_polarity = clk_polarity; + run_abc.clk_sig = clk_sig; } bool read_until_abc_done(abc_output_filter &filt, int fd, DeferredLogs &logs) { @@ -1204,11 +1215,24 @@ void RunAbcState::run(ConcurrentStack &process_pool) fprintf(f, " dummy_input\n"); fprintf(f, "\n"); + if (config.filter_non_trigger_outputs) { + for (auto &si : signal_list) { + if (!si.is_port || si.type == G(NONE)) + continue; + if (si.type == G(FF) || si.type == G(FF0) || si.type == G(FF1)) + continue; + if (si.bit_str.find("trigger") == std::string::npos) + si.is_port = false; + } + } + int count_output = 0; fprintf(f, ".outputs"); for (auto &si : signal_list) { if (!si.is_port || si.type == G(NONE)) continue; + if (config.filter_non_trigger_outputs && (si.type == G(FF) || si.type == G(FF0) || si.type == G(FF1))) + continue; fprintf(f, " ys__n%d", si.id); po_map[count_output++] = si.bit_str; } @@ -1217,6 +1241,33 @@ void RunAbcState::run(ConcurrentStack &process_pool) for (auto &si : signal_list) fprintf(f, "# ys__n%-5d %s\n", si.id, si.bit_str.c_str()); + if (!config.signal_map_file.empty()) { + FILE *mf = fopen(config.signal_map_file.c_str(), state_index == 0 ? "wt" : "at"); + if (mf == nullptr) { + logs.log("Opening %s for writing failed: %s\n", config.signal_map_file, strerror(errno)); + } else { + if (clk_sig.size() != 0) { + std::string clk_str = log_signal(clk_sig); + fprintf(mf, "# Clock domain %d: %s%s\n", state_index, + clk_polarity ? "" : "!", clk_str.c_str()); + } else + fprintf(mf, "# Clock domain %d: (none)\n", state_index); + fprintf(mf, "# Inputs\n"); + for (auto &si : signal_list) { + if (!si.is_port || si.type != G(NONE)) + continue; + fprintf(mf, "ys__n%d %s\n", si.id, si.bit_str.c_str()); + } + fprintf(mf, "# Outputs\n"); + for (auto &si : signal_list) { + if (!si.is_port || si.type == G(NONE)) + continue; + fprintf(mf, "ys__n%d %s\n", si.id, si.bit_str.c_str()); + } + fclose(mf); + } + } + for (auto &si : signal_list) { if (!si.bit_is_wire) { fprintf(f, ".names ys__n%d\n", si.id); @@ -1820,7 +1871,7 @@ void AbcModuleState::finish() // For every signal that connects cells from different sets, or a cell in a set to a cell not in any set, // mark it as a port in `assign_map`. void assign_cell_connection_ports(RTLIL::Module *module, const std::vector *> &cell_sets, - AbcSigMap &assign_map) + AbcSigMap &assign_map, const std::string &cdc_file) { pool cells_in_no_set; for (RTLIL::Cell *cell : module->cells()) { @@ -1829,6 +1880,8 @@ void assign_cell_connection_ports(RTLIL::Module *module, const std::vector 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); @@ -1839,6 +1892,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)); } @@ -1851,11 +1905,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 { @@ -2046,6 +2118,18 @@ struct AbcPass : public Pass { log(" which means auto (use number of modules). Set to 0 to disable parallel\n"); log(" execution and run everything on the main thread.\n"); log("\n"); + log(" -signal_map \n"); + log(" write a mapping of ABC signal names (ys__nN) to original port names\n"); + log(" for inputs and outputs. useful for interpreting ABC counterexamples.\n"); + log("\n"); + log(" -cdc_map \n"); + log(" write a mapping of signals that cross clock domain boundaries.\n"); + log(" each line lists a signal and the domain indices it bridges.\n"); + log("\n"); + log(" -filter_non_trigger_outputs\n"); + log(" only keep output ports whose signal name contains 'trigger'.\n"); + log(" intended for miter/equivalence-checking flows. off by default.\n"); + log("\n"); log(" -reserved_cores \n"); log(" number of CPU cores to reserve for the main thread and other work.\n"); log(" Default is 4. The actual number of worker threads used is:\n"); @@ -2115,6 +2199,9 @@ struct AbcPass : public Pass { config.markgroups = design->scratchpad_get_bool("abc.markgroups", false); config.max_threads = design->scratchpad_get_int("abc.max_threads", -1); config.reserved_cores = design->scratchpad_get_int("abc.reserved_cores", 4); + config.signal_map_file = design->scratchpad_get_string("abc.signal_map", ""); + config.cdc_file = design->scratchpad_get_string("abc.cdc_map", ""); + config.filter_non_trigger_outputs = design->scratchpad_get_bool("abc.filter_non_trigger_outputs", false); if (config.cleanup) config.global_tempdir_name = get_base_tmpdir() + "/"; @@ -2258,6 +2345,18 @@ struct AbcPass : public Pass { config.reserved_cores = atoi(args[++argidx].c_str()); continue; } + if (arg == "-signal_map" && argidx+1 < args.size()) { + config.signal_map_file = args[++argidx]; + continue; + } + if (arg == "-cdc_map" && argidx+1 < args.size()) { + config.cdc_file = args[++argidx]; + continue; + } + if (arg == "-filter_non_trigger_outputs") { + config.filter_non_trigger_outputs = true; + continue; + } break; } extra_args(args, argidx, design); @@ -2501,7 +2600,7 @@ struct AbcPass : public Pass { // Populate assign_map with cell connections std::vector cells = mod->selected_cells(); - assign_cell_connection_ports(mod, {&cells}, assign_map); + assign_cell_connection_ports(mod, {&cells}, assign_map, config.cdc_file); // Create a map of all signals and their corresponding src attrs SigMap sigmap(mod); @@ -2802,7 +2901,7 @@ struct AbcPass : public Pass { std::get<6>(it.first) ? "" : "!", log_signal(std::get<7>(it.first))); cell_sets.push_back(&it.second); } - assign_cell_connection_ports(mod, cell_sets, assign_map); + assign_cell_connection_ports(mod, cell_sets, assign_map, config.cdc_file); } // Reserve one core for our main thread, and don't create more worker threads 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 <