summaryrefslogtreecommitdiff
path: root/passes/equiv
diff options
context:
space:
mode:
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/Makefile.inc2
-rw-r--r--passes/equiv/equiv_make.cc86
-rw-r--r--passes/equiv/equiv_opt.cc157
3 files changed, 239 insertions, 6 deletions
diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc
index dd7b3be0..27ea54b2 100644
--- a/passes/equiv/Makefile.inc
+++ b/passes/equiv/Makefile.inc
@@ -9,4 +9,4 @@ OBJS += passes/equiv/equiv_induct.o
OBJS += passes/equiv/equiv_struct.o
OBJS += passes/equiv/equiv_purge.o
OBJS += passes/equiv/equiv_mark.o
-
+OBJS += passes/equiv/equiv_opt.o
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index b1f88d55..dbd8682e 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -40,6 +40,16 @@ struct EquivMakeWorker
pool<SigBit> undriven_bits;
SigMap assign_map;
+ dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells
+
+ CellTypes comb_ct;
+
+ EquivMakeWorker()
+ {
+ comb_ct.setup_internals();
+ comb_ct.setup_stdcells();
+ }
+
void read_blacklists()
{
for (auto fn : blacklists)
@@ -278,16 +288,31 @@ struct EquivMakeWorker
}
}
+ init_bit2driven();
+
+ pool<Cell*> visited_cells;
for (auto c : cells_list)
for (auto &conn : c->connections())
if (!ct.cell_output(c->type, conn.first)) {
SigSpec old_sig = assign_map(conn.second);
SigSpec new_sig = rd_signal_map(old_sig);
- if (old_sig != new_sig) {
- log("Changing input %s of cell %s (%s): %s -> %s\n",
- log_id(conn.first), log_id(c), log_id(c->type),
- log_signal(old_sig), log_signal(new_sig));
- c->setPort(conn.first, new_sig);
+
+ if(old_sig != new_sig) {
+ SigSpec tmp_sig = old_sig;
+ for (int i = 0; i < GetSize(old_sig); i++) {
+ SigBit old_bit = old_sig[i], new_bit = new_sig[i];
+
+ visited_cells.clear();
+ if (check_signal_in_fanout(visited_cells, old_bit, new_bit))
+ continue;
+
+ log("Changing input %s of cell %s (%s): %s -> %s\n",
+ log_id(conn.first), log_id(c), log_id(c->type),
+ log_signal(old_bit), log_signal(new_bit));
+
+ tmp_sig[i] = new_bit;
+ }
+ c->setPort(conn.first, tmp_sig);
}
}
@@ -378,6 +403,57 @@ struct EquivMakeWorker
}
}
+ void init_bit2driven()
+ {
+ for (auto cell : equiv_mod->cells()) {
+ if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
+ continue;
+ for (auto &conn : cell->connections())
+ {
+ if (yosys_celltypes.cell_input(cell->type, conn.first))
+ for (auto bit : assign_map(conn.second))
+ {
+ bit2driven[bit].insert(cell);
+ }
+ }
+ }
+ }
+
+ bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit)
+ {
+ if (source_bit == target_bit)
+ return true;
+
+ if (bit2driven.count(source_bit) == 0)
+ return false;
+
+ auto driven_cells = bit2driven.at(source_bit);
+ for (auto driven_cell: driven_cells)
+ {
+ bool is_comb = comb_ct.cell_known(driven_cell->type);
+ if (!is_comb)
+ continue;
+
+ if (visited_cells.count(driven_cell) > 0)
+ continue;
+ visited_cells.insert(driven_cell);
+
+ for (auto &conn: driven_cell->connections())
+ {
+ if (yosys_celltypes.cell_input(driven_cell->type, conn.first))
+ continue;
+
+ for (auto bit: conn.second) {
+ bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit);
+ if (is_in_fanout == true)
+ return true;
+ }
+ }
+ }
+
+ return false;
+ }
+
void run()
{
copy_to_equiv();
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
new file mode 100644
index 00000000..86550a69
--- /dev/null
+++ b/passes/equiv/equiv_opt.cc
@@ -0,0 +1,157 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2018 whitequark <whitequark@whitequark.org>
+ *
+ * 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/register.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EquivOptPass:public ScriptPass
+{
+ EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
+
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" equiv_opt [options] [command]\n");
+ log("\n");
+ log("This command checks circuit equivalence before and after an optimization pass.\n");
+ log("\n");
+ log(" -run <from_label>:<to_label>\n");
+ log(" only run the commands between the labels (see below). an empty\n");
+ log(" from label is synonymous to the start of the command list, and empty to\n");
+ log(" label is synonymous to the end of the command list.\n");
+ log("\n");
+ log(" -map <filename>\n");
+ log(" expand the modules in this file before proving equivalence. this is\n");
+ log(" useful for handling architecture-specific primitives.\n");
+ log("\n");
+ log(" -assert\n");
+ log(" produce an error if the circuits are not equivalent\n");
+ log("\n");
+ log("The following commands are executed by this verification command:\n");
+ help_script();
+ log("\n");
+ }
+
+ std::string command, techmap_opts;
+ bool assert;
+
+ void clear_flags() YS_OVERRIDE
+ {
+ command = "";
+ techmap_opts = "";
+ assert = false;
+ }
+
+ void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
+ {
+ string run_from, run_to;
+ clear_flags();
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-run" && argidx + 1 < args.size()) {
+ size_t pos = args[argidx + 1].find(':');
+ if (pos == std::string::npos)
+ break;
+ run_from = args[++argidx].substr(0, pos);
+ run_to = args[argidx].substr(pos + 1);
+ continue;
+ }
+ if (args[argidx] == "-map" && argidx + 1 < args.size()) {
+ techmap_opts += " -map " + args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-assert") {
+ assert = true;
+ continue;
+ }
+ break;
+ }
+
+ for (; argidx < args.size(); argidx++) {
+ if (command.empty()) {
+ if (args[argidx].substr(0, 1) == "-")
+ cmd_error(args, argidx, "Unknown option.");
+ } else {
+ command += " ";
+ }
+ command += args[argidx];
+ }
+
+ if (command.empty())
+ log_cmd_error("No optimization pass specified!\n");
+
+ if (!design->full_selection())
+ log_cmd_error("This command only operates on fully selected designs!\n");
+
+ log_header(design, "Executing EQUIV_OPT pass.\n");
+ log_push();
+
+ run_script(design, run_from, run_to);
+
+ log_pop();
+ }
+
+ void script() YS_OVERRIDE
+ {
+ if (check_label("run_pass")) {
+ run("hierarchy -auto-top");
+ run("design -save preopt");
+ if (help_mode)
+ run("[command]");
+ else
+ run(command);
+ run("design -stash postopt");
+ }
+
+ if (check_label("prepare")) {
+ run("design -copy-from preopt -as gold A:top");
+ run("design -copy-from postopt -as gate A:top");
+ }
+
+ if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)")) {
+ string opts;
+ if (help_mode)
+ opts = " -map <filename> ...";
+ else
+ opts = techmap_opts;
+ run("techmap -D EQUIV -autoproc" + opts);
+ }
+
+ if (check_label("prove")) {
+ run("equiv_make gold gate equiv");
+ run("equiv_induct equiv");
+ if (help_mode)
+ run("equiv_status [-assert] equiv");
+ else if (assert)
+ run("equiv_status -assert equiv");
+ else
+ run("equiv_status equiv");
+ }
+
+ if (check_label("restore")) {
+ run("design -load preopt");
+ }
+ }
+} EquivOptPass;
+
+PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-30 14:16:29 +0000