mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

Improvements in equiv_make, equiv_induct

Browse source
This commit is contained in:
Clifford Wolf 2015-01-22 21:23:01 +01:00
parent 5707ba22c1
commit 1cb4c925d0
2 changed files with 46 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
passes/equiv/equiv_induct.cc
View file

@ -136,6 +136,18 @@ struct EquivInductPass : public Pass {
log(" -seq <N>\n"); log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 4)\n"); log(" the max. number of time steps to be considered (default = 4)\n");
log("\n"); log("\n");
log("This command is very effective in proving complex sequential circuits, when\n");
log("the internal state of the circuit quickly propagates to $equiv cells.\n");
log("\n");
log("However, this command uses a weak definition of 'equivalence': This command\n");
log("proves that the two circuits will not diverge after they produce equal\n");
log("outputs (observable points via $equiv) for at least <N> cycles (the <N>\n");
log("specified via -seq).\n");
log("\n");
log("Combined with simulation this is very powerful because simulation can give\n");
log("you confidence that the circuits start out synced for at least <N> cycles\n");
log("after reset.\n");
log("\n");
} }
virtual void execute(std::vector<std::string> args, Design *design) virtual void execute(std::vector<std::string> args, Design *design)
{ {

34
passes/equiv/equiv_make.cc
View file

@ -176,11 +176,45 @@ struct EquivMakeWorker
} }
} }
void find_undriven_nets()
{
pool<SigBit> undriven_bits;
SigMap assign_map(equiv_mod);
for (auto wire : equiv_mod->wires()) {
for (auto bit : assign_map(wire))
if (bit.wire)
undriven_bits.insert(bit);
}
for (auto wire : equiv_mod->wires()) {
if (wire->port_input)
for (auto bit : assign_map(wire))
undriven_bits.erase(bit);
}
for (auto cell : equiv_mod->cells()) {
for (auto &conn : cell->connections())
if (!ct.cell_known(cell->type) || ct.cell_output(cell->type, conn.first))
for (auto bit : assign_map(conn.second))
undriven_bits.erase(bit);
}
SigSpec undriven_sig(undriven_bits);
undriven_sig.sort_and_unify();
for (auto chunk : undriven_sig.chunks()) {
log("Setting undriven nets to undef: %s\n", log_signal(chunk));
equiv_mod->connect(chunk, SigSpec(State::Sx, chunk.width));
}
}
void run() void run()
{ {
copy_to_equiv(); copy_to_equiv();
find_same_wires(); find_same_wires();
find_same_cells(); find_same_cells();
find_undriven_nets();
} }
}; };