mirror of https://github.com/YosysHQ/yosys.git
Added new port outputs anding the clock domain. TODO: fix if they belong to the same one and there's multiple
This commit is contained in:
parent
f7a9af5252
commit
92e659f42a
|
|
@ -32,18 +32,20 @@ struct ClkMergePass : public Pass {
|
|||
log("\n");
|
||||
log(" clkmerge [-target <signal>] [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 <signal>\n");
|
||||
log(" use the specified signal as the merged clock. if not given, the\n");
|
||||
log(" clock signal of the first FF encountered is used.\n");
|
||||
log(" clock signal of the first FF encountered is used. all FFs will\n");
|
||||
log(" be set to positive-edge triggered on this signal.\n");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
|
|
@ -64,8 +66,13 @@ struct ClkMergePass : public Pass {
|
|||
{
|
||||
SigMap sigmap(module);
|
||||
|
||||
dict<SigBit, int> clk_domain_count;
|
||||
std::vector<std::pair<Cell*, SigSpec>> ff_clk_pairs;
|
||||
struct FfInfo {
|
||||
Cell *cell;
|
||||
SigSpec clk;
|
||||
bool pol_clk;
|
||||
};
|
||||
|
||||
std::vector<FfInfo> 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<SigSpec> all_clks;
|
||||
for (auto &pair : ff_clk_pairs)
|
||||
all_clks.insert(pair.second);
|
||||
// Collect distinct (signal, polarity) pairs
|
||||
pool<std::pair<SigSpec, bool>> all_domains;
|
||||
for (auto &info : ff_list)
|
||||
all_domains.insert({info.clk, info.pol_clk});
|
||||
|
||||
if (all_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;
|
||||
|
|
|
|||
|
|
@ -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 <cstdarg>
|
||||
|
||||
|
|
@ -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_<idx> is created in each module for each
|
||||
// clock domain that appears in its FFs. The PO for a cone is ANDed with
|
||||
// the guard so that FFs in different clock domains remain structurally
|
||||
// distinguishable even after clkmerge unifies the actual clock signals.
|
||||
dict<std::pair<std::string, bool>, int> clk_domain_to_guard;
|
||||
int next_guard_idx = 0;
|
||||
dict<std::pair<Module*, int>, Wire*> guard_pi_cache;
|
||||
|
||||
ConePartitionWorker(Design *d, Module *gold, Module *gate, bool v, FILE *lf = nullptr)
|
||||
: design(d), gold_mod(gold), gate_mod(gate), verbose(v), log_file(lf) {}
|
||||
|
||||
int get_or_create_guard_idx(const SigSpec &clk, bool pol, SigMap &sigmap) {
|
||||
SigSpec mapped = sigmap(clk);
|
||||
std::string clk_str = log_signal(mapped);
|
||||
auto key = std::make_pair(clk_str, pol);
|
||||
auto it = clk_domain_to_guard.find(key);
|
||||
if (it != clk_domain_to_guard.end())
|
||||
return it->second;
|
||||
int idx = next_guard_idx++;
|
||||
clk_domain_to_guard[key] = idx;
|
||||
return idx;
|
||||
}
|
||||
|
||||
Wire* get_or_create_guard_pi(Module *mod, int guard_idx) {
|
||||
auto key = std::make_pair(mod, guard_idx);
|
||||
auto it = guard_pi_cache.find(key);
|
||||
if (it != guard_pi_cache.end())
|
||||
return it->second;
|
||||
std::string name = stringf("\\clkguard_%d", guard_idx);
|
||||
Wire *w = mod->addWire(name, 1);
|
||||
w->port_input = true;
|
||||
guard_pi_cache[key] = w;
|
||||
total_guards++;
|
||||
return w;
|
||||
}
|
||||
|
||||
// Returns guard index for an FF cell, or -1 if the FF has no clock.
|
||||
int get_ff_guard_idx(Cell *cell, SigMap &sigmap) {
|
||||
FfData ff(nullptr, cell);
|
||||
if (!ff.has_clk)
|
||||
return -1;
|
||||
return get_or_create_guard_idx(ff.sig_clk, ff.pol_clk, sigmap);
|
||||
}
|
||||
|
||||
void vlog(const char *fmt, ...) __attribute__((format(printf, 2, 3))) {
|
||||
va_list ap;
|
||||
va_start(ap, fmt);
|
||||
|
|
@ -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<std::pair<std::string, bool>> collect_clock_domains(ModuleAnalysis &analysis, SigMap &sigmap) {
|
||||
pool<std::pair<std::string, bool>> domains;
|
||||
for (auto cell : analysis.ff_cells) {
|
||||
FfData ff(nullptr, cell);
|
||||
if (!ff.has_clk)
|
||||
continue;
|
||||
SigSpec mapped = sigmap(ff.sig_clk);
|
||||
std::string clk_str = log_signal(mapped);
|
||||
domains.insert({clk_str, ff.pol_clk});
|
||||
}
|
||||
return domains;
|
||||
}
|
||||
|
||||
void run() {
|
||||
StructuralHasher hasher;
|
||||
|
||||
|
|
@ -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<int, std::vector<Cell*>> gold_ff_by_hash, gate_ff_by_hash;
|
||||
for (auto &[cell, h] : gold_analysis.cell_hash)
|
||||
|
|
@ -294,32 +401,62 @@ struct ConePartitionWorker {
|
|||
};
|
||||
std::vector<ConeGroup> groups;
|
||||
|
||||
pool<Cell*> matched_gold_ffs, matched_gate_ffs;
|
||||
|
||||
for (auto &[h, gold_cells] : gold_ff_by_hash) {
|
||||
auto it = gate_ff_by_hash.find(h);
|
||||
if (it == gate_ff_by_hash.end())
|
||||
continue;
|
||||
groups.push_back({gold_cells, it->second});
|
||||
for (auto c : gold_cells) matched_gold_ffs.insert(c);
|
||||
for (auto c : it->second) matched_gate_ffs.insert(c);
|
||||
}
|
||||
|
||||
if (groups.empty()) {
|
||||
vlog("No structural FF matches found between `%s' and `%s'.\n",
|
||||
gold_mod->name.c_str(), gate_mod->name.c_str());
|
||||
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<Cell*> &gold_cells,
|
||||
const std::vector<Cell*> &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");
|
||||
|
|
|
|||
Loading…
Reference in New Issue