summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-01-22 21:23:01 +0100
committerClifford Wolf <clifford@clifford.at>2015-01-22 21:23:01 +0100
commit1cb4c925d03de289f37a40b6eceb57ced8dce295 (patch)
tree88a08f99571ae64a4456f1b791d26b946920d55f /passes
parent5707ba22c10048bef7d5ad81d090e3dd31d779a4 (diff)
Improvements in equiv_make, equiv_induct
Diffstat (limited to 'passes')
-rw-r--r--passes/equiv/equiv_induct.cc12
-rw-r--r--passes/equiv/equiv_make.cc34
2 files changed, 46 insertions, 0 deletions
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index ccf4f957..38a52d75 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -136,6 +136,18 @@ struct EquivInductPass : public Pass {
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 4)\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)
{
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 07374cfc..be1480e9 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -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()
{
copy_to_equiv();
find_same_wires();
find_same_cells();
+ find_undriven_nets();
}
};