From 76c5d863c52253a5709f44e0608c53a8c33ab3b5 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 19 Jan 2015 13:59:08 +0100 Subject: [PATCH] Added equiv_make command --- kernel/rtlil.cc | 9 ++ kernel/rtlil.h | 3 +- passes/sat/Makefile.inc | 1 + passes/sat/equiv_make.cc | 248 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 260 insertions(+), 1 deletion(-) create mode 100644 passes/sat/equiv_make.cc diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index ec61cb529..52293da29 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1618,6 +1618,15 @@ RTLIL::Cell* RTLIL::Module::addAssert(RTLIL::IdString name, RTLIL::SigSpec sig_a return cell; } +RTLIL::Cell* RTLIL::Module::addEquiv(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y) +{ + RTLIL::Cell *cell = addCell(name, "$equiv"); + cell->setPort("\\A", sig_a); + cell->setPort("\\B", sig_b); + cell->setPort("\\Y", sig_y); + return cell; +} + RTLIL::Cell* RTLIL::Module::addSr(RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity, bool clr_polarity) { RTLIL::Cell *cell = addCell(name, "$sr"); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 53ee24c22..dae684d98 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -439,7 +439,7 @@ namespace RTLIL return result; } - pool to_set() const { return *this; } + pool to_pool() const { return *this; } std::vector to_vector() const { return *this; } }; }; @@ -968,6 +968,7 @@ public: RTLIL::Cell* addConcat (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y); RTLIL::Cell* addLut (RTLIL::IdString name, RTLIL::SigSpec sig_i, RTLIL::SigSpec sig_o, RTLIL::Const lut); RTLIL::Cell* addAssert (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en); + RTLIL::Cell* addEquiv (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y); RTLIL::Cell* addSr (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true); RTLIL::Cell* addDff (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true); diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index 4fa6bf0d4..eb919eb21 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -4,4 +4,5 @@ OBJS += passes/sat/freduce.o OBJS += passes/sat/eval.o OBJS += passes/sat/miter.o OBJS += passes/sat/expose.o +OBJS += passes/sat/equiv_make.o diff --git a/passes/sat/equiv_make.cc b/passes/sat/equiv_make.cc new file mode 100644 index 000000000..07374cfc3 --- /dev/null +++ b/passes/sat/equiv_make.cc @@ -0,0 +1,248 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf + * + * 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" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct EquivMakeWorker +{ + Module *gold_mod, *gate_mod, *equiv_mod; + pool wire_names, cell_names; + CellTypes ct; + + void copy_to_equiv() + { + Module *gold_clone = gold_mod->clone(); + Module *gate_clone = gate_mod->clone(); + + for (auto it : gold_clone->wires().to_vector()) { if (it->name[0] == '\\') wire_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); } + for (auto it : gold_clone->cells().to_vector()) { if (it->name[0] == '\\') cell_names.insert(it->name); gold_clone->rename(it, it->name.str() + "_gold"); } + for (auto it : gate_clone->wires().to_vector()) { if (it->name[0] == '\\') wire_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); } + for (auto it : gate_clone->cells().to_vector()) { if (it->name[0] == '\\') cell_names.insert(it->name); gate_clone->rename(it, it->name.str() + "_gate"); } + + gold_clone->cloneInto(equiv_mod); + gate_clone->cloneInto(equiv_mod); + delete gold_clone; + delete gate_clone; + } + + void find_same_wires() + { + SigMap assign_map(equiv_mod); + SigMap rd_signal_map; + + // list of cells without added $equiv cells + auto cells_list = equiv_mod->cells().to_vector(); + + for (auto id : wire_names) + { + IdString gold_id = id.str() + "_gold"; + IdString gate_id = id.str() + "_gate"; + + Wire *gold_wire = equiv_mod->wire(gold_id); + Wire *gate_wire = equiv_mod->wire(gate_id); + + if (gold_wire == nullptr || gate_wire == nullptr || gold_wire->width != gate_wire->width) { + if (gold_wire && gold_wire->port_id) + log_error("Can't match gold port `%s' to a gate port.\n", log_id(gold_wire)); + if (gate_wire && gate_wire->port_id) + log_error("Can't match gate port `%s' to a gold port.\n", log_id(gate_wire)); + continue; + } + + log("Presumably equivalent wires: %s (%s), %s (%s) -> %s\n", + log_id(gold_wire), log_signal(assign_map(gold_wire)), + log_id(gate_wire), log_signal(assign_map(gate_wire)), log_id(id)); + + if (gold_wire->port_output || gate_wire->port_output) + { + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + wire->port_output = true; + gold_wire->port_input = false; + gate_wire->port_input = false; + gold_wire->port_output = false; + gate_wire->port_output = false; + + for (int i = 0; i < wire->width; i++) + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + + rd_signal_map.add(assign_map(gold_wire), wire); + rd_signal_map.add(assign_map(gate_wire), wire); + } + else + if (gold_wire->port_input || gate_wire->port_input) + { + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + wire->port_input = true; + gold_wire->port_input = false; + gate_wire->port_input = false; + equiv_mod->connect(gold_wire, wire); + equiv_mod->connect(gate_wire, wire); + } + else + { + Wire *wire = equiv_mod->addWire(id, gold_wire->width); + + for (int i = 0; i < wire->width; i++) + equiv_mod->addEquiv(NEW_ID, SigSpec(gold_wire, i), SigSpec(gate_wire, i), SigSpec(wire, i)); + + rd_signal_map.add(assign_map(gold_wire), wire); + rd_signal_map.add(assign_map(gate_wire), wire); + } + } + + for (auto c : cells_list) + for (auto &conn : c->connections()) + if (ct.cell_input(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); + } + } + + equiv_mod->fixup_ports(); + } + + void find_same_cells() + { + SigMap assign_map(equiv_mod); + + for (auto id : cell_names) + { + IdString gold_id = id.str() + "_gold"; + IdString gate_id = id.str() + "_gate"; + + Cell *gold_cell = equiv_mod->cell(gold_id); + Cell *gate_cell = equiv_mod->cell(gate_id); + + if (gold_cell == nullptr || gate_cell == nullptr || gold_cell->type != gate_cell->type || !ct.cell_known(gold_cell->type) || + gold_cell->parameters != gate_cell->parameters || GetSize(gold_cell->connections()) != GetSize(gate_cell->connections())) + try_next_cell_name: + continue; + + for (auto gold_conn : gold_cell->connections()) + if (!gate_cell->connections().count(gold_conn.first)) + goto try_next_cell_name; + + log("Presumably equivalent cells: %s %s (%s) -> %s\n", + log_id(gold_cell), log_id(gate_cell), log_id(gold_cell->type), log_id(id)); + + for (auto gold_conn : gold_cell->connections()) + { + SigSpec gold_sig = assign_map(gold_conn.second); + SigSpec gate_sig = assign_map(gate_cell->getPort(gold_conn.first)); + + if (ct.cell_output(gold_cell->type, gold_conn.first)) { + equiv_mod->connect(gate_sig, gold_sig); + continue; + } + + for (int i = 0; i < GetSize(gold_sig); i++) + if (gold_sig[i] != gate_sig[i]) { + Wire *w = equiv_mod->addWire(NEW_ID); + equiv_mod->addEquiv(NEW_ID, gold_sig[i], gate_sig[i], w); + gold_sig[i] = w; + } + + gold_cell->setPort(gold_conn.first, gold_sig); + } + + equiv_mod->remove(gate_cell); + equiv_mod->rename(gold_cell, id); + } + } + + void run() + { + copy_to_equiv(); + find_same_wires(); + find_same_cells(); + } +}; + +struct EquivMakePass : public Pass { + EquivMakePass() : Pass("equiv_make", "prepare a circuit for equivalence checking") { } + virtual void help() + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" equiv_make [options] gold_module gate_module equiv_module\n"); + log("\n"); + log("This creates a module annotated with $equiv cells from two presumably\n"); + log("equivalent modules. Use commands such as 'equiv_simple' and 'equiv_status'\n"); + log("to work with the created equivalent checking module.\n"); + log("\n"); + log("Note: The circuit created by this command is not a miter (with something like\n"); + log("a trigger output), but instead uses $equiv cells to encode the equivalence\n"); + log("checking problem. Use 'miter -equiv' if you want to create a miter circuit.\n"); + log("\n"); + } + virtual void execute(std::vector args, RTLIL::Design *design) + { + EquivMakeWorker worker; + worker.ct.setup(design); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + // if (args[argidx] == "-foo" && argidx+1 < args.size()) { + // log("foo> %s\n", args[++argidx].c_str()); + // continue; + // } + break; + } + + if (argidx+3 != args.size()) + log_cmd_error("Invalid number of arguments.\n"); + + worker.gold_mod = design->module(RTLIL::escape_id(args[argidx])); + worker.gate_mod = design->module(RTLIL::escape_id(args[argidx+1])); + worker.equiv_mod = design->module(RTLIL::escape_id(args[argidx+2])); + + if (worker.gold_mod == nullptr) + log_cmd_error("Can't find gold module %s.\n", args[argidx].c_str()); + + if (worker.gate_mod == nullptr) + log_cmd_error("Can't find gate module %s.\n", args[argidx+1].c_str()); + + if (worker.equiv_mod != nullptr) + log_cmd_error("Equiv module %s already exists.\n", args[argidx+2].c_str()); + + if (worker.gold_mod->has_memories() || worker.gold_mod->has_processes()) + log_cmd_error("Gold module contains memories or procresses. Run 'memory' or 'proc' respectively.\n"); + + if (worker.gate_mod->has_memories() || worker.gate_mod->has_processes()) + log_cmd_error("Gate module contains memories or procresses. Run 'memory' or 'proc' respectively.\n"); + + log_header("Executing EQUIV_MAKE pass (creating equiv checking module).\n"); + + worker.equiv_mod = design->addModule(RTLIL::escape_id(args[argidx+2])); + worker.run(); + } +} EquivMakePass; + +PRIVATE_NAMESPACE_END -- 2.30.2