summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/Makefile.inc9
-rw-r--r--passes/sat/assertpmux.cc240
-rw-r--r--passes/sat/clk2fflogic.cc226
-rw-r--r--passes/sat/eval.cc603
-rw-r--r--passes/sat/example.v85
-rw-r--r--passes/sat/example.ys14
-rw-r--r--passes/sat/expose.cc650
-rw-r--r--passes/sat/freduce.cc840
-rw-r--r--passes/sat/miter.cc421
-rw-r--r--passes/sat/sat.cc1713
10 files changed, 4801 insertions, 0 deletions
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
new file mode 100644
index 00000000..6785b750
--- /dev/null
+++ b/passes/sat/Makefile.inc
@@ -0,0 +1,9 @@
+
+OBJS += passes/sat/sat.o
+OBJS += passes/sat/freduce.o
+OBJS += passes/sat/eval.o
+OBJS += passes/sat/miter.o
+OBJS += passes/sat/expose.o
+OBJS += passes/sat/assertpmux.o
+OBJS += passes/sat/clk2fflogic.o
+
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
new file mode 100644
index 00000000..63a90767
--- /dev/null
+++ b/passes/sat/assertpmux.cc
@@ -0,0 +1,240 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct AssertpmuxWorker
+{
+ Module *module;
+ SigMap sigmap;
+
+ bool flag_noinit;
+ bool flag_always;
+
+ // get<0> ... mux cell
+ // get<1> ... mux port index
+ // get<2> ... mux bit index
+ dict<SigBit, pool<tuple<Cell*, int, int>>> sigbit_muxusers;
+
+ dict<SigBit, SigBit> sigbit_actsignals;
+ dict<SigSpec, SigBit> sigspec_actsignals;
+ dict<tuple<Cell*, int>, SigBit> muxport_actsignal;
+
+ AssertpmuxWorker(Module *module, bool flag_noinit, bool flag_always) :
+ module(module), sigmap(module), flag_noinit(flag_noinit), flag_always(flag_always)
+ {
+ for (auto wire : module->wires())
+ {
+ if (wire->port_output)
+ for (auto bit : sigmap(wire))
+ sigbit_actsignals[bit] = State::S1;
+ }
+
+ for (auto cell : module->cells())
+ {
+ if (cell->type.in("$mux", "$pmux"))
+ {
+ int width = cell->getParam("\\WIDTH").as_int();
+ int numports = cell->type == "$mux" ? 2 : cell->getParam("\\S_WIDTH").as_int() + 1;
+
+ SigSpec sig_a = sigmap(cell->getPort("\\A"));
+ SigSpec sig_b = sigmap(cell->getPort("\\B"));
+ SigSpec sig_s = sigmap(cell->getPort("\\S"));
+
+ for (int i = 0; i < numports; i++) {
+ SigSpec bits = i == 0 ? sig_a : sig_b.extract(width*(i-1), width);
+ for (int k = 0; k < width; k++) {
+ tuple<Cell*, int, int> muxuser(cell, i, k);
+ sigbit_muxusers[bits[k]].insert(muxuser);
+ }
+ }
+ }
+ else
+ {
+ for (auto &conn : cell->connections()) {
+ if (!cell->known() || cell->input(conn.first))
+ for (auto bit : sigmap(conn.second))
+ sigbit_actsignals[bit] = State::S1;
+ }
+ }
+ }
+ }
+
+ SigBit get_bit_activation(SigBit bit)
+ {
+ sigmap.apply(bit);
+
+ if (sigbit_actsignals.count(bit) == 0)
+ {
+ SigSpec output;
+
+ for (auto muxuser : sigbit_muxusers.at(bit))
+ {
+ Cell *cell = std::get<0>(muxuser);
+ int portidx = std::get<1>(muxuser);
+ int bitidx = std::get<2>(muxuser);
+
+ tuple<Cell*, int> muxport(cell, portidx);
+
+ if (muxport_actsignal.count(muxport) == 0) {
+ if (portidx == 0)
+ muxport_actsignal[muxport] = module->LogicNot(NEW_ID, cell->getPort("\\S"));
+ else
+ muxport_actsignal[muxport] = cell->getPort("\\S")[portidx-1];
+ }
+
+ output.append(module->LogicAnd(NEW_ID, muxport_actsignal.at(muxport), get_bit_activation(cell->getPort("\\Y")[bitidx])));
+ }
+
+ output.sort_and_unify();
+
+ if (GetSize(output) == 0)
+ output = State::S0;
+ else if (GetSize(output) > 1)
+ output = module->ReduceOr(NEW_ID, output);
+
+ sigbit_actsignals[bit] = output.as_bit();
+ }
+
+ return sigbit_actsignals.at(bit);
+ }
+
+ SigBit get_activation(SigSpec sig)
+ {
+ sigmap.apply(sig);
+ sig.sort_and_unify();
+
+ if (sigspec_actsignals.count(sig) == 0)
+ {
+ SigSpec output;
+
+ for (auto bit : sig)
+ output.append(get_bit_activation(bit));
+
+ output.sort_and_unify();
+
+ if (GetSize(output) == 0)
+ output = State::S0;
+ else if (GetSize(output) > 1)
+ output = module->ReduceOr(NEW_ID, output);
+
+ sigspec_actsignals[sig] = output.as_bit();
+ }
+
+ return sigspec_actsignals.at(sig);
+ }
+
+ void run(Cell *pmux)
+ {
+ log("Adding assert for $pmux cell %s.%s.\n", log_id(module), log_id(pmux));
+
+ int swidth = pmux->getParam("\\S_WIDTH").as_int();
+ int cntbits = ceil_log2(swidth+1);
+
+ SigSpec sel = pmux->getPort("\\S");
+ SigSpec cnt(State::S0, cntbits);
+
+ for (int i = 0; i < swidth; i++)
+ cnt = module->Add(NEW_ID, cnt, sel[i]);
+
+ SigSpec assert_a = module->Le(NEW_ID, cnt, SigSpec(1, cntbits));
+ SigSpec assert_en;
+
+ if (flag_noinit)
+ assert_en.append(module->LogicNot(NEW_ID, module->Initstate(NEW_ID)));
+
+ if (!flag_always)
+ assert_en.append(get_activation(pmux->getPort("\\Y")));
+
+ if (GetSize(assert_en) == 0)
+ assert_en = State::S1;
+
+ if (GetSize(assert_en) == 2)
+ assert_en = module->LogicAnd(NEW_ID, assert_en[0], assert_en[1]);
+
+ Cell *assert_cell = module->addAssert(NEW_ID, assert_a, assert_en);
+
+ if (pmux->attributes.count("\\src") != 0)
+ assert_cell->attributes["\\src"] = pmux->attributes.at("\\src");
+ }
+};
+
+struct AssertpmuxPass : public Pass {
+ AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" assertpmux [options] [selection]\n");
+ log("\n");
+ log("This command adds asserts to the design that assert that all parallel muxes\n");
+ log("($pmux cells) have a maximum of one of their inputs enable at any time.\n");
+ log("\n");
+ log(" -noinit\n");
+ log(" do not enforce the pmux condition during the init state\n");
+ log("\n");
+ log(" -always\n");
+ log(" usually the $pmux condition is only checked when the $pmux output\n");
+ log(" is used be the mux tree it drives. this option will deactivate this\n");
+ log(" additional constrained and check the $pmux condition always.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ bool flag_noinit = false;
+ bool flag_always = false;
+
+ log_header(design, "Executing ASSERTPMUX pass (add asserts for $pmux cells).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-noinit") {
+ flag_noinit = true;
+ continue;
+ }
+ if (args[argidx] == "-always") {
+ flag_always = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ for (auto module : design->selected_modules())
+ {
+ AssertpmuxWorker worker(module, flag_noinit, flag_always);
+ vector<Cell*> pmux_cells;
+
+ for (auto cell : module->selected_cells())
+ if (cell->type == "$pmux")
+ pmux_cells.push_back(cell);
+
+ for (auto cell : pmux_cells)
+ worker.run(cell);
+ }
+
+ }
+} AssertpmuxPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
new file mode 100644
index 00000000..ef6d5dd7
--- /dev/null
+++ b/passes/sat/clk2fflogic.cc
@@ -0,0 +1,226 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct Clk2fflogicPass : public Pass {
+ Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" clk2fflogic [options] [selection]\n");
+ log("\n");
+ log("This command replaces clocked flip-flops with generic $ff cells that use the\n");
+ log("implicit global clock. This is useful for formal verification of designs with\n");
+ log("multiple clocks.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ // bool flag_noinit = false;
+
+ log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ // if (args[argidx] == "-noinit") {
+ // flag_noinit = true;
+ // continue;
+ // }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ for (auto module : design->selected_modules())
+ {
+ SigMap sigmap(module);
+ dict<SigBit, State> initbits;
+ pool<SigBit> del_initbits;
+
+ for (auto wire : module->wires())
+ if (wire->attributes.count("\\init") > 0)
+ {
+ Const initval = wire->attributes.at("\\init");
+ SigSpec initsig = sigmap(wire);
+
+ for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
+ if (initval[i] == State::S0 || initval[i] == State::S1)
+ initbits[initsig[i]] = initval[i];
+ }
+
+ for (auto cell : vector<Cell*>(module->selected_cells()))
+ {
+ if (cell->type.in("$dlatch"))
+ {
+ bool enpol = cell->parameters["\\EN_POLARITY"].as_bool();
+
+ SigSpec sig_en = cell->getPort("\\EN");
+ SigSpec sig_d = cell->getPort("\\D");
+ SigSpec sig_q = cell->getPort("\\Q");
+
+ log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(sig_en), log_signal(sig_d), log_signal(sig_q));
+
+ Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
+ module->addFf(NEW_ID, sig_q, past_q);
+
+ if (enpol)
+ module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q);
+ else
+ module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q);
+
+ Const initval;
+ bool assign_initval = false;
+ for (int i = 0; i < GetSize(sig_d); i++) {
+ SigBit qbit = sigmap(sig_q[i]);
+ if (initbits.count(qbit)) {
+ initval.bits.push_back(initbits.at(qbit));
+ del_initbits.insert(qbit);
+ } else
+ initval.bits.push_back(State::Sx);
+ if (initval.bits.back() != State::Sx)
+ assign_initval = true;
+ }
+
+ if (assign_initval)
+ past_q->attributes["\\init"] = initval;
+
+ module->remove(cell);
+ continue;
+ }
+
+ if (cell->type.in("$dff", "$adff", "$dffsr"))
+ {
+ bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool();
+
+ SigSpec clk = cell->getPort("\\CLK");
+ Wire *past_clk = module->addWire(NEW_ID);
+ past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0;
+ module->addFf(NEW_ID, clk, past_clk);
+
+ SigSpec sig_d = cell->getPort("\\D");
+ SigSpec sig_q = cell->getPort("\\Q");
+
+ log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_signal(clk), log_signal(sig_d), log_signal(sig_q));
+
+ SigSpec clock_edge_pattern;
+
+ if (clkpol) {
+ clock_edge_pattern.append_bit(State::S0);
+ clock_edge_pattern.append_bit(State::S1);
+ } else {
+ clock_edge_pattern.append_bit(State::S1);
+ clock_edge_pattern.append_bit(State::S0);
+ }
+
+ SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern);
+
+ Wire *past_d = module->addWire(NEW_ID, GetSize(sig_d));
+ Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q));
+ module->addFf(NEW_ID, sig_d, past_d);
+ module->addFf(NEW_ID, sig_q, past_q);
+
+ if (cell->type == "$adff")
+ {
+ SigSpec arst = cell->getPort("\\ARST");
+ SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
+ Const rstval = cell->parameters["\\ARST_VALUE"];
+
+ if (cell->parameters["\\ARST_POLARITY"].as_bool())
+ module->addMux(NEW_ID, qval, rstval, arst, sig_q);
+ else
+ module->addMux(NEW_ID, rstval, qval, arst, sig_q);
+ }
+ else
+ if (cell->type == "$dffsr")
+ {
+ SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
+ SigSpec setval = cell->getPort("\\SET");
+ SigSpec clrval = cell->getPort("\\CLR");
+
+ if (!cell->parameters["\\SET_POLARITY"].as_bool())
+ setval = module->Not(NEW_ID, setval);
+
+ if (cell->parameters["\\CLR_POLARITY"].as_bool())
+ clrval = module->Not(NEW_ID, clrval);
+
+ qval = module->Or(NEW_ID, qval, setval);
+ module->addAnd(NEW_ID, qval, clrval, sig_q);
+ }
+ else
+ {
+ module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q);
+ }
+
+ Const initval;
+ bool assign_initval = false;
+ for (int i = 0; i < GetSize(sig_d); i++) {
+ SigBit qbit = sigmap(sig_q[i]);
+ if (initbits.count(qbit)) {
+ initval.bits.push_back(initbits.at(qbit));
+ del_initbits.insert(qbit);
+ } else
+ initval.bits.push_back(State::Sx);
+ if (initval.bits.back() != State::Sx)
+ assign_initval = true;
+ }
+
+ if (assign_initval) {
+ past_d->attributes["\\init"] = initval;
+ past_q->attributes["\\init"] = initval;
+ }
+
+ module->remove(cell);
+ continue;
+ }
+ }
+
+ for (auto wire : module->wires())
+ if (wire->attributes.count("\\init") > 0)
+ {
+ bool delete_initattr = true;
+ Const initval = wire->attributes.at("\\init");
+ SigSpec initsig = sigmap(wire);
+
+ for (int i = 0; i < GetSize(initval) && i < GetSize(initsig); i++)
+ if (del_initbits.count(initsig[i]) > 0)
+ initval[i] = State::Sx;
+ else if (initval[i] != State::Sx)
+ delete_initattr = false;
+
+ if (delete_initattr)
+ wire->attributes.erase("\\init");
+ else
+ wire->attributes.at("\\init") = initval;
+ }
+ }
+
+ }
+} Clk2fflogicPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
new file mode 100644
index 00000000..09f69cc5
--- /dev/null
+++ b/passes/sat/eval.cc
@@ -0,0 +1,603 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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.
+ *
+ */
+
+// [[CITE]] VlogHammer Verilog Regression Test Suite
+// http://www.clifford.at/yosys/vloghammer.html
+
+#include "kernel/register.h"
+#include "kernel/celltypes.h"
+#include "kernel/consteval.h"
+#include "kernel/sigtools.h"
+#include "kernel/satgen.h"
+#include "kernel/log.h"
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <algorithm>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+/* this should only be used for regression testing of ConstEval -- see vloghammer */
+struct BruteForceEquivChecker
+{
+ RTLIL::Module *mod1, *mod2;
+ RTLIL::SigSpec mod1_inputs, mod1_outputs;
+ RTLIL::SigSpec mod2_inputs, mod2_outputs;
+ int counter, errors;
+ bool ignore_x_mod1;
+
+ void run_checker(RTLIL::SigSpec &inputs)
+ {
+ if (inputs.size() < mod1_inputs.size()) {
+ RTLIL::SigSpec inputs0 = inputs, inputs1 = inputs;
+ inputs0.append(RTLIL::Const(0, 1));
+ inputs1.append(RTLIL::Const(1, 1));
+ run_checker(inputs0);
+ run_checker(inputs1);
+ return;
+ }
+
+ ConstEval ce1(mod1), ce2(mod2);
+ ce1.set(mod1_inputs, inputs.as_const());
+ ce2.set(mod2_inputs, inputs.as_const());
+
+ RTLIL::SigSpec sig1 = mod1_outputs, undef1;
+ RTLIL::SigSpec sig2 = mod2_outputs, undef2;
+
+ if (!ce1.eval(sig1, undef1))
+ log("Failed ConstEval of module 1 outputs at signal %s (input: %s = %s).\n",
+ log_signal(undef1), log_signal(mod1_inputs), log_signal(inputs));
+ if (!ce2.eval(sig2, undef2))
+ log("Failed ConstEval of module 2 outputs at signal %s (input: %s = %s).\n",
+ log_signal(undef2), log_signal(mod1_inputs), log_signal(inputs));
+
+ if (ignore_x_mod1) {
+ for (int i = 0; i < GetSize(sig1); i++)
+ if (sig1[i] == RTLIL::State::Sx)
+ sig2[i] = RTLIL::State::Sx;
+ }
+
+ if (sig1 != sig2) {
+ log("Found counter-example (ignore_x_mod1 = %s):\n", ignore_x_mod1 ? "active" : "inactive");
+ log(" Module 1: %s = %s => %s = %s\n", log_signal(mod1_inputs), log_signal(inputs), log_signal(mod1_outputs), log_signal(sig1));
+ log(" Module 2: %s = %s => %s = %s\n", log_signal(mod2_inputs), log_signal(inputs), log_signal(mod2_outputs), log_signal(sig2));
+ errors++;
+ }
+
+ counter++;
+ }
+
+ BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1) :
+ mod1(mod1), mod2(mod2), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1)
+ {
+ log("Checking for equivalence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str());
+ for (auto &w : mod1->wires_)
+ {
+ RTLIL::Wire *wire1 = w.second;
+ if (wire1->port_id == 0)
+ continue;
+
+ if (mod2->wires_.count(wire1->name) == 0)
+ log_cmd_error("Port %s in module 1 has no counterpart in module 2!\n", wire1->name.c_str());
+
+ RTLIL::Wire *wire2 = mod2->wires_.at(wire1->name);
+ if (wire1->width != wire2->width || wire1->port_input != wire2->port_input || wire1->port_output != wire2->port_output)
+ log_cmd_error("Port %s in module 1 does not match its counterpart in module 2!\n", wire1->name.c_str());
+
+ if (wire1->port_input) {
+ mod1_inputs.append(wire1);
+ mod2_inputs.append(wire2);
+ } else {
+ mod1_outputs.append(wire1);
+ mod2_outputs.append(wire2);
+ }
+ }
+
+ RTLIL::SigSpec inputs;
+ run_checker(inputs);
+ }
+};
+
+/* this should only be used for regression testing of ConstEval -- see vloghammer */
+struct VlogHammerReporter
+{
+ RTLIL::Design *design;
+ std::vector<RTLIL::Module*> modules;
+ std::vector<std::string> module_names;
+ std::vector<RTLIL::IdString> inputs;
+ std::vector<int> input_widths;
+ std::vector<RTLIL::Const> patterns;
+ int total_input_width;
+
+ std::vector<std::string> split(std::string text, const char *delim)
+ {
+ std::vector<std::string> list;
+ char *p = strdup(text.c_str());
+ char *t = strtok(p, delim);
+ while (t != NULL) {
+ list.push_back(t);
+ t = strtok(NULL, delim);
+ }
+ free(p);
+ return list;
+ }
+
+ void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y, bool model_undef)
+ {
+ log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef");
+
+ ezSatPtr ez;
+ SigMap sigmap(module);
+ SatGen satgen(ez.get(), &sigmap);
+ satgen.model_undef = model_undef;
+
+ for (auto &c : module->cells_)
+ if (!satgen.importCell(c.second))
+ log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
+
+ ez->assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals));
+
+ std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y"));
+ std::vector<bool> y_values;
+
+ if (model_undef) {
+ std::vector<int> y_undef_vec = satgen.importUndefSigSpec(module->wires_.at("\\y"));
+ y_vec.insert(y_vec.end(), y_undef_vec.begin(), y_undef_vec.end());
+ }
+
+ log(" Created SAT problem with %d variables and %d clauses.\n",
+ ez->numCnfVariables(), ez->numCnfClauses());
+
+ if (!ez->solve(y_vec, y_values))
+ log_error("Failed to find solution to SAT problem.\n");
+
+ for (int i = 0; i < expected_y.size(); i++) {
+ RTLIL::State solution_bit = y_values.at(i) ? RTLIL::State::S1 : RTLIL::State::S0;
+ RTLIL::State expected_bit = expected_y[i].data;
+ if (model_undef) {
+ if (y_values.at(expected_y.size()+i))
+ solution_bit = RTLIL::State::Sx;
+ } else {
+ if (expected_bit == RTLIL::State::Sx)
+ continue;
+ }
+ if (solution_bit != expected_bit) {
+ std::string sat_bits, rtl_bits;
+ for (int k = expected_y.size()-1; k >= 0; k--) {
+ if (model_undef && y_values.at(expected_y.size()+k))
+ sat_bits += "x";
+ else
+ sat_bits += y_values.at(k) ? "1" : "0";
+ rtl_bits += expected_y[k] == RTLIL::State::Sx ? "x" : expected_y[k] == RTLIL::State::S1 ? "1" : "0";
+ }
+ log_error("Found error in SAT model: y[%d] = %s, should be %s:\n SAT: %s\n RTL: %s\n %*s^\n",
+ int(i), log_signal(solution_bit), log_signal(expected_bit),
+ sat_bits.c_str(), rtl_bits.c_str(), expected_y.size()-i-1, "");
+ }
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> cmp_vars;
+ std::vector<bool> cmp_vals;
+
+ std::vector<bool> y_undef(y_values.begin() + expected_y.size(), y_values.end());
+
+ for (int i = 0; i < expected_y.size(); i++)
+ if (y_undef.at(i))
+ {
+ log(" Toggling undef bit %d to test undef gating.\n", i);
+ if (!ez->solve(y_vec, y_values, ez->IFF(y_vec.at(i), y_values.at(i) ? ez->CONST_FALSE : ez->CONST_TRUE)))
+ log_error("Failed to find solution with toggled bit!\n");
+
+ cmp_vars.push_back(y_vec.at(expected_y.size() + i));
+ cmp_vals.push_back(true);
+ }
+ else
+ {
+ cmp_vars.push_back(y_vec.at(i));
+ cmp_vals.push_back(y_values.at(i));
+
+ cmp_vars.push_back(y_vec.at(expected_y.size() + i));
+ cmp_vals.push_back(false);
+ }
+
+ log(" Testing if SAT solution is unique.\n");
+ ez->assume(ez->vec_ne(cmp_vars, ez->vec_const(cmp_vals)));
+ if (ez->solve(y_vec, y_values))
+ log_error("Found two distinct solutions to SAT problem.\n");
+ }
+ else
+ {
+ log(" Testing if SAT solution is unique.\n");
+ ez->assume(ez->vec_ne(y_vec, ez->vec_const(y_values)));
+ if (ez->solve(y_vec, y_values))
+ log_error("Found two distinct solutions to SAT problem.\n");
+ }
+
+ log(" SAT model verified.\n");
+ }
+
+ void run()
+ {
+ for (int idx = 0; idx < int(patterns.size()); idx++)
+ {
+ log("Creating report for pattern %d: %s\n", idx, log_signal(patterns[idx]));
+ std::string input_pattern_list;
+ RTLIL::SigSpec rtl_sig;
+
+ for (int mod = 0; mod < int(modules.size()); mod++)
+ {
+ RTLIL::SigSpec recorded_set_vars;
+ RTLIL::Const recorded_set_vals;
+ RTLIL::Module *module = modules[mod];
+ std::string module_name = module_names[mod].c_str();
+ ConstEval ce(module);
+
+ std::vector<RTLIL::State> bits(patterns[idx].bits.begin(), patterns[idx].bits.begin() + total_input_width);
+ for (int i = 0; i < int(inputs.size()); i++) {
+ RTLIL::Wire *wire = module->wires_.at(inputs[i]);
+ for (int j = input_widths[i]-1; j >= 0; j--) {
+ ce.set(RTLIL::SigSpec(wire, j), bits.back());
+ recorded_set_vars.append(RTLIL::SigSpec(wire, j));
+ recorded_set_vals.bits.push_back(bits.back());
+ bits.pop_back();
+ }
+ if (module == modules.front()) {
+ RTLIL::SigSpec sig(wire);
+ if (!ce.eval(sig))
+ log_error("Can't read back value for port %s!\n", RTLIL::id2cstr(inputs[i]));
+ input_pattern_list += stringf(" %s", sig.as_const().as_string().c_str());
+ log("++PAT++ %d %s %s #\n", idx, RTLIL::id2cstr(inputs[i]), sig.as_const().as_string().c_str());
+ }
+ }
+
+ if (module->wires_.count("\\y") == 0)
+ log_error("No output wire (y) found in module %s!\n", RTLIL::id2cstr(module->name));
+
+ RTLIL::SigSpec sig(module->wires_.at("\\y"));
+ RTLIL::SigSpec undef;
+
+ while (!ce.eval(sig, undef)) {
+ // log_error("Evaluation of y in module %s failed: sig=%s, undef=%s\n", RTLIL::id2cstr(module->name), log_signal(sig), log_signal(undef));
+ log_warning("Setting signal %s in module %s to undef.\n", log_signal(undef), RTLIL::id2cstr(module->name));
+ ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
+ }
+
+ log("++VAL++ %d %s %s #\n", idx, module_name.c_str(), sig.as_const().as_string().c_str());
+
+ if (module_name == "rtl") {
+ rtl_sig = sig;
+ sat_check(module, recorded_set_vars, recorded_set_vals, sig, false);
+ sat_check(module, recorded_set_vars, recorded_set_vals, sig, true);
+ } else if (rtl_sig.size() > 0) {
+ if (rtl_sig.size() != sig.size())
+ log_error("Output (y) has a different width in module %s compared to rtl!\n", RTLIL::id2cstr(module->name));
+ for (int i = 0; i < GetSize(sig); i++)
+ if (rtl_sig[i] == RTLIL::State::Sx)
+ sig[i] = RTLIL::State::Sx;
+ }
+
+ log("++RPT++ %d%s %s %s\n", idx, input_pattern_list.c_str(), sig.as_const().as_string().c_str(), module_name.c_str());
+ }
+
+ log("++RPT++ ----\n");
+ }
+ log("++OK++\n");
+ }
+
+ VlogHammerReporter(RTLIL::Design *design, std::string module_prefix, std::string module_list, std::string input_list, std::string pattern_list) : design(design)
+ {
+ for (auto name : split(module_list, ",")) {
+ RTLIL::IdString esc_name = RTLIL::escape_id(module_prefix + name);
+ if (design->modules_.count(esc_name) == 0)
+ log_error("Can't find module %s in current design!\n", name.c_str());
+ log("Using module %s (%s).\n", esc_name.c_str(), name.c_str());
+ modules.push_back(design->modules_.at(esc_name));
+ module_names.push_back(name);
+ }
+
+ total_input_width = 0;
+ for (auto name : split(input_list, ",")) {
+ int width = -1;
+ RTLIL::IdString esc_name = RTLIL::escape_id(name);
+ for (auto mod : modules) {
+ if (mod->wires_.count(esc_name) == 0)
+ log_error("Can't find input %s in module %s!\n", name.c_str(), RTLIL::id2cstr(mod->name));
+ RTLIL::Wire *port = mod->wires_.at(esc_name);
+ if (!port->port_input || port->port_output)
+ log_error("Wire %s in module %s is not an input!\n", name.c_str(), RTLIL::id2cstr(mod->name));
+ if (width >= 0 && width != port->width)
+ log_error("Port %s has different sizes in the different modules!\n", name.c_str());
+ width = port->width;
+ }
+ log("Using input port %s with width %d.\n", esc_name.c_str(), width);
+ inputs.push_back(esc_name);
+ input_widths.push_back(width);
+ total_input_width += width;
+ }
+
+ for (auto pattern : split(pattern_list, ",")) {
+ RTLIL::SigSpec sig;
+ bool invert_pattern = false;
+ if (pattern.size() > 0 && pattern[0] == '~') {
+ invert_pattern = true;
+ pattern = pattern.substr(1);
+ }
+ if (!RTLIL::SigSpec::parse(sig, NULL, pattern) || !sig.is_fully_const())
+ log_error("Failed to parse pattern %s!\n", pattern.c_str());
+ if (sig.size() < total_input_width)
+ log_error("Pattern %s is to short!\n", pattern.c_str());
+ patterns.push_back(sig.as_const());
+ if (invert_pattern) {
+ for (auto &bit : patterns.back().bits)
+ if (bit == RTLIL::State::S0)
+ bit = RTLIL::State::S1;
+ else if (bit == RTLIL::State::S1)
+ bit = RTLIL::State::S0;
+ }
+ log("Using pattern %s.\n", patterns.back().as_string().c_str());
+ }
+ }
+};
+
+struct EvalPass : public Pass {
+ EvalPass() : Pass("eval", "evaluate the circuit given an input") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" eval [options] [selection]\n");
+ log("\n");
+ log("This command evaluates the value of a signal given the value of all required\n");
+ log("inputs.\n");
+ log("\n");
+ log(" -set <signal> <value>\n");
+ log(" set the specified signal to the specified value.\n");
+ log("\n");
+ log(" -set-undef\n");
+ log(" set all unspecified source signals to undef (x)\n");
+ log("\n");
+ log(" -table <signal>\n");
+ log(" create a truth table using the specified input signals\n");
+ log("\n");
+ log(" -show <signal>\n");
+ log(" show the value for the specified signal. if no -show option is passed\n");
+ log(" then all output ports of the current module are used.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ std::vector<std::pair<std::string, std::string>> sets;
+ std::vector<std::string> shows, tables;
+ bool set_undef = false;
+
+ log_header(design, "Executing EVAL pass (evaluate the circuit given an input).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-set" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx].c_str();
+ std::string rhs = args[++argidx].c_str();
+ sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ continue;
+ }
+ if (args[argidx] == "-set-undef") {
+ set_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-show" && argidx+1 < args.size()) {
+ shows.push_back(args[++argidx]);
+ continue;
+ }
+ if (args[argidx] == "-table" && argidx+1 < args.size()) {
+ tables.push_back(args[++argidx]);
+ continue;
+ }
+ if ((args[argidx] == "-brute_force_equiv_checker" || args[argidx] == "-brute_force_equiv_checker_x") && argidx+3 == args.size()) {
+ /* this should only be used for regression testing of ConstEval -- see vloghammer */
+ std::string mod1_name = RTLIL::escape_id(args[++argidx]);
+ std::string mod2_name = RTLIL::escape_id(args[++argidx]);
+ if (design->modules_.count(mod1_name) == 0)
+ log_error("Can't find module `%s'!\n", mod1_name.c_str());
+ if (design->modules_.count(mod2_name) == 0)
+ log_error("Can't find module `%s'!\n", mod2_name.c_str());
+ BruteForceEquivChecker checker(design->modules_.at(mod1_name), design->modules_.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x");
+ if (checker.errors > 0)
+ log_cmd_error("Modules are not equivalent!\n");
+ log("Verified %s = %s (using brute-force check on %d cases).\n",
+ mod1_name.c_str(), mod2_name.c_str(), checker.counter);
+ return;
+ }
+ if (args[argidx] == "-vloghammer_report" && argidx+5 == args.size()) {
+ /* this should only be used for regression testing of ConstEval -- see vloghammer */
+ std::string module_prefix = args[++argidx];
+ std::string module_list = args[++argidx];
+ std::string input_list = args[++argidx];
+ std::string pattern_list = args[++argidx];
+ VlogHammerReporter reporter(design, module_prefix, module_list, input_list, pattern_list);
+ reporter.run();
+ return;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ RTLIL::Module *module = NULL;
+ for (auto &mod_it : design->modules_)
+ if (design->selected(mod_it.second)) {
+ if (module)
+ log_cmd_error("Only one module must be selected for the EVAL pass! (selected: %s and %s)\n",
+ RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
+ module = mod_it.second;
+ }
+ if (module == NULL)
+ log_cmd_error("Can't perform EVAL on an empty selection!\n");
+
+ ConstEval ce(module);
+
+ for (auto &it : sets) {
+ RTLIL::SigSpec lhs, rhs;
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, it.first))
+ log_cmd_error("Failed to parse lhs set expression `%s'.\n", it.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, it.second))
+ log_cmd_error("Failed to parse rhs set expression `%s'.\n", it.second.c_str());
+ if (!rhs.is_fully_const())
+ log_cmd_error("Right-hand-side set expression `%s' is not constant.\n", it.second.c_str());
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ it.first.c_str(), log_signal(lhs), lhs.size(), it.second.c_str(), log_signal(rhs), rhs.size());
+ ce.set(lhs, rhs.as_const());
+ }
+
+ if (shows.size() == 0) {
+ for (auto &it : module->wires_)
+ if (it.second->port_output)
+ shows.push_back(it.second->name.str());
+ }
+
+ if (tables.empty())
+ {
+ for (auto &it : shows) {
+ RTLIL::SigSpec signal, value, undef;
+ if (!RTLIL::SigSpec::parse_sel(signal, design, module, it))
+ log_cmd_error("Failed to parse show expression `%s'.\n", it.c_str());
+ value = signal;
+ if (set_undef) {
+ while (!ce.eval(value, undef)) {
+ log("Failed to evaluate signal %s: Missing value for %s. -> setting to undef\n", log_signal(signal), log_signal(undef));
+ ce.set(undef, RTLIL::Const(RTLIL::State::Sx, undef.size()));
+ undef = RTLIL::SigSpec();
+ }
+ log("Eval result: %s = %s.\n", log_signal(signal), log_signal(value));
+ } else {
+ if (!ce.eval(value, undef))
+ log("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(signal), log_signal(undef));
+ else
+ log("Eval result: %s = %s.\n", log_signal(signal), log_signal(value));
+ }
+ }
+ }
+ else
+ {
+ RTLIL::SigSpec tabsigs, signal, value, undef;
+ std::vector<std::vector<std::string>> tab;
+ int tab_sep_colidx = 0;
+
+ for (auto &it : shows) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, it))
+ log_cmd_error("Failed to parse show expression `%s'.\n", it.c_str());
+ signal.append(sig);
+ }
+
+ for (auto &it : tables) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, it))
+ log_cmd_error("Failed to parse table expression `%s'.\n", it.c_str());
+ tabsigs.append(sig);
+ }
+
+ std::vector<std::string> tab_line;
+ for (auto &c : tabsigs.chunks())
+ tab_line.push_back(log_signal(c));
+ tab_sep_colidx = tab_line.size();
+ for (auto &c : signal.chunks())
+ tab_line.push_back(log_signal(c));
+ tab.push_back(tab_line);
+ tab_line.clear();
+
+ RTLIL::Const tabvals(0, tabsigs.size());
+ do
+ {
+ ce.push();
+ ce.set(tabsigs, tabvals);
+ value = signal;
+
+ RTLIL::SigSpec this_undef;
+ while (!ce.eval(value, this_undef)) {
+ if (!set_undef) {
+ log("Failed to evaluate signal %s at %s = %s: Missing value for %s.\n", log_signal(signal),
+ log_signal(tabsigs), log_signal(tabvals), log_signal(this_undef));
+ return;
+ }
+ ce.set(this_undef, RTLIL::Const(RTLIL::State::Sx, this_undef.size()));
+ undef.append(this_undef);
+ this_undef = RTLIL::SigSpec();
+ }
+
+ int pos = 0;
+ for (auto &c : tabsigs.chunks()) {
+ tab_line.push_back(log_signal(RTLIL::SigSpec(tabvals).extract(pos, c.width)));
+ pos += c.width;
+ }
+
+ pos = 0;
+ for (auto &c : signal.chunks()) {
+ tab_line.push_back(log_signal(value.extract(pos, c.width)));
+ pos += c.width;
+ }
+
+ tab.push_back(tab_line);
+ tab_line.clear();
+ ce.pop();
+
+ tabvals = RTLIL::const_add(tabvals, RTLIL::Const(1), false, false, tabvals.bits.size());
+ }
+ while (tabvals.as_bool());
+
+ std::vector<int> tab_column_width;
+ for (auto &row : tab) {
+ if (tab_column_width.size() < row.size())
+ tab_column_width.resize(row.size());
+ for (size_t i = 0; i < row.size(); i++)
+ tab_column_width[i] = max(tab_column_width[i], int(row[i].size()));
+ }
+
+ log("\n");
+ bool first = true;
+ for (auto &row : tab) {
+ for (size_t i = 0; i < row.size(); i++) {
+ int k = int(i) < tab_sep_colidx ? tab_sep_colidx - i - 1 : i;
+ log(" %s%*s", k == tab_sep_colidx ? "| " : "", tab_column_width[k], row[k].c_str());
+ }
+ log("\n");
+ if (first) {
+ for (size_t i = 0; i < row.size(); i++) {
+ int k = int(i) < tab_sep_colidx ? tab_sep_colidx - i - 1 : i;
+ log(" %s", k == tab_sep_colidx ? "| " : "");
+ for (int j = 0; j < tab_column_width[k]; j++)
+ log("-");
+ }
+ log("\n");
+ first = false;
+ }
+ }
+
+ log("\n");
+ if (undef.size() > 0) {
+ undef.sort_and_unify();
+ log("Assumed undef (x) value for the following signals: %s\n\n", log_signal(undef));
+ }
+ }
+ }
+} EvalPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/example.v b/passes/sat/example.v
new file mode 100644
index 00000000..aa0ddb6e
--- /dev/null
+++ b/passes/sat/example.v
@@ -0,0 +1,85 @@
+
+module example001(a, y);
+
+input [15:0] a;
+output y;
+
+wire gt = a > 12345;
+wire lt = a < 12345;
+assign y = !gt && !lt;
+
+endmodule
+
+// ------------------------------------
+
+module example002(a, y);
+
+input [3:0] a;
+output y;
+reg [1:0] t1, t2;
+
+always @* begin
+ casex (a)
+ 16'b1xxx:
+ t1 <= 1;
+ 16'bx1xx:
+ t1 <= 2;
+ 16'bxx1x:
+ t1 <= 3;
+ 16'bxxx1:
+ t1 <= 4;
+ default:
+ t1 <= 0;
+ endcase
+ casex (a)
+ 16'b1xxx:
+ t2 <= 1;
+ 16'b01xx:
+ t2 <= 2;
+ 16'b001x:
+ t2 <= 3;
+ 16'b0001:
+ t2 <= 4;
+ default:
+ t2 <= 0;
+ endcase
+end
+
+assign y = t1 != t2;
+
+endmodule
+
+// ------------------------------------
+
+module example003(a_shl, a_shr, a_sshl, a_sshr, sh, y_shl, y_shr, y_sshl, y_sshr);
+
+input [7:0] a_shl, a_shr;
+input signed [7:0] a_sshl, a_sshr;
+input [3:0] sh;
+
+output [7:0] y_shl = a_shl << sh, y_shr = a_shr >> sh;
+output signed [7:0] y_sshl = a_sshl <<< sh, y_sshr = a_sshr >>> sh;
+
+endmodule
+
+// ------------------------------------
+
+module example004(clk, rst, y);
+
+input clk, rst;
+output y;
+
+reg [3:0] counter;
+
+always @(posedge clk)
+ case (1'b1)
+ rst, counter == 9:
+ counter <= 0;
+ default:
+ counter <= counter+1;
+ endcase
+
+assign y = counter == 12;
+
+endmodule
+
diff --git a/passes/sat/example.ys b/passes/sat/example.ys
new file mode 100644
index 00000000..cc72faac
--- /dev/null
+++ b/passes/sat/example.ys
@@ -0,0 +1,14 @@
+
+read_verilog example.v
+proc; opt_clean
+echo on
+
+sat -set y 1'b1 example001
+sat -set y 1'b1 example002
+sat -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
+sat -set y 1'b1 -ignore_unknown_cells example004
+sat -show rst,counter -set-at 3 y 1'b1 -seq 4 example004
+
+sat -prove y 1'b0 -show rst,counter,y -ignore_unknown_cells example004
+sat -prove y 1'b0 -tempinduct -show rst,counter,y -set-at 1 rst 1'b1 -seq 1 example004
+
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
new file mode 100644
index 00000000..9427547f
--- /dev/null
+++ b/passes/sat/expose.cc
@@ -0,0 +1,650 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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"
+#include "kernel/celltypes.h"
+#include "kernel/sigtools.h"
+#include "kernel/rtlil.h"
+#include "kernel/log.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct dff_map_info_t {
+ RTLIL::SigSpec sig_d, sig_clk, sig_arst;
+ bool clk_polarity, arst_polarity;
+ RTLIL::Const arst_value;
+ std::vector<RTLIL::IdString> cells;
+};
+
+struct dff_map_bit_info_t {
+ RTLIL::SigBit bit_d, bit_clk, bit_arst;
+ bool clk_polarity, arst_polarity;
+ RTLIL::State arst_value;
+ RTLIL::Cell *cell;
+};
+
+bool consider_wire(RTLIL::Wire *wire, std::map<RTLIL::IdString, dff_map_info_t> &dff_dq_map)
+{
+ if (wire->name[0] == '$' || dff_dq_map.count(wire->name))
+ return false;
+ if (wire->port_input)
+ return false;
+ return true;
+}
+
+bool consider_cell(RTLIL::Design *design, std::set<RTLIL::IdString> &dff_cells, RTLIL::Cell *cell)
+{
+ if (cell->name[0] == '$' || dff_cells.count(cell->name))
+ return false;
+ if (cell->type[0] == '\\' && !design->modules_.count(cell->type))
+ return false;
+ return true;
+}
+
+bool compare_wires(RTLIL::Wire *wire1, RTLIL::Wire *wire2)
+{
+ log_assert(wire1->name == wire2->name);
+ if (wire1->width != wire2->width)
+ return false;
+ return true;
+}
+
+bool compare_cells(RTLIL::Cell *cell1, RTLIL::Cell *cell2)
+{
+ log_assert(cell1->name == cell2->name);
+ if (cell1->type != cell2->type)
+ return false;
+ if (cell1->parameters != cell2->parameters)
+ return false;
+ return true;
+}
+
+void find_dff_wires(std::set<RTLIL::IdString> &dff_wires, RTLIL::Module *module)
+{
+ CellTypes ct;
+ ct.setup_internals_mem();
+ ct.setup_stdcells_mem();
+
+ SigMap sigmap(module);
+ SigPool dffsignals;
+
+ for (auto &it : module->cells_) {
+ if (ct.cell_known(it.second->type) && it.second->hasPort("\\Q"))
+ dffsignals.add(sigmap(it.second->getPort("\\Q")));
+ }
+
+ for (auto &it : module->wires_) {
+ if (dffsignals.check_any(it.second))
+ dff_wires.insert(it.first);
+ }
+}
+
+void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::Design *design, RTLIL::Module *module)
+{
+ std::map<RTLIL::SigBit, dff_map_bit_info_t> bit_info;
+ SigMap sigmap(module);
+
+ for (auto &it : module->cells_)
+ {
+ if (!design->selected(module, it.second))
+ continue;
+
+ dff_map_bit_info_t info;
+ info.bit_d = RTLIL::State::Sm;
+ info.bit_clk = RTLIL::State::Sm;
+ info.bit_arst = RTLIL::State::Sm;
+ info.clk_polarity = false;
+ info.arst_polarity = false;
+ info.arst_value = RTLIL::State::Sm;
+ info.cell = it.second;
+
+ if (info.cell->type == "$dff") {
+ info.bit_clk = sigmap(info.cell->getPort("\\CLK")).as_bit();
+ info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool();
+ std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector();
+ std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->getPort("\\Q")).to_sigbit_vector();
+ for (size_t i = 0; i < sig_d.size(); i++) {
+ info.bit_d = sig_d.at(i);
+ bit_info[sig_q.at(i)] = info;
+ }
+ continue;
+ }
+
+ if (info.cell->type == "$adff") {
+ info.bit_clk = sigmap(info.cell->getPort("\\CLK")).as_bit();
+ info.bit_arst = sigmap(info.cell->getPort("\\ARST")).as_bit();
+ info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool();
+ info.arst_polarity = info.cell->parameters.at("\\ARST_POLARITY").as_bool();
+ std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector();
+ std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->getPort("\\Q")).to_sigbit_vector();
+ std::vector<RTLIL::State> arst_value = info.cell->parameters.at("\\ARST_VALUE").bits;
+ for (size_t i = 0; i < sig_d.size(); i++) {
+ info.bit_d = sig_d.at(i);
+ info.arst_value = arst_value.at(i);
+ bit_info[sig_q.at(i)] = info;
+ }
+ continue;
+ }
+
+ if (info.cell->type == "$_DFF_N_" || info.cell->type == "$_DFF_P_") {
+ info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit();
+ info.clk_polarity = info.cell->type == "$_DFF_P_";
+ info.bit_d = sigmap(info.cell->getPort("\\D")).as_bit();
+ bit_info[sigmap(info.cell->getPort("\\Q")).as_bit()] = info;
+ continue;
+ }
+
+ if (info.cell->type.size() == 10 && info.cell->type.substr(0, 6) == "$_DFF_") {
+ info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit();
+ info.bit_arst = sigmap(info.cell->getPort("\\R")).as_bit();
+ info.clk_polarity = info.cell->type[6] == 'P';
+ info.arst_polarity = info.cell->type[7] == 'P';
+ info.arst_value = info.cell->type[0] == '1' ? RTLIL::State::S1 : RTLIL::State::S0;
+ info.bit_d = sigmap(info.cell->getPort("\\D")).as_bit();
+ bit_info[sigmap(info.cell->getPort("\\Q")).as_bit()] = info;
+ continue;
+ }
+ }
+
+ std::map<RTLIL::IdString, dff_map_info_t> empty_dq_map;
+ for (auto &it : module->wires_)
+ {
+ if (!consider_wire(it.second, empty_dq_map))
+ continue;
+
+ std::vector<RTLIL::SigBit> bits_q = sigmap(it.second).to_sigbit_vector();
+ std::vector<RTLIL::SigBit> bits_d;
+ std::vector<RTLIL::State> arst_value;
+ std::set<RTLIL::Cell*> cells;
+
+ if (bits_q.empty() || !bit_info.count(bits_q.front()))
+ continue;
+
+ dff_map_bit_info_t ref_info = bit_info.at(bits_q.front());
+ for (auto &bit : bits_q) {
+ if (!bit_info.count(bit))
+ break;
+ dff_map_bit_info_t info = bit_info.at(bit);
+ if (info.bit_clk != ref_info.bit_clk)
+ break;
+ if (info.bit_arst != ref_info.bit_arst)
+ break;
+ if (info.clk_polarity != ref_info.clk_polarity)
+ break;
+ if (info.arst_polarity != ref_info.arst_polarity)
+ break;
+ bits_d.push_back(info.bit_d);
+ arst_value.push_back(info.arst_value);
+ cells.insert(info.cell);
+ }
+
+ if (bits_d.size() != bits_q.size())
+ continue;
+
+ dff_map_info_t info;
+ info.sig_d = bits_d;
+ info.sig_clk = ref_info.bit_clk;
+ info.sig_arst = ref_info.bit_arst;
+ info.clk_polarity = ref_info.clk_polarity;
+ info.arst_polarity = ref_info.arst_polarity;
+ info.arst_value = arst_value;
+ for (auto it : cells)
+ info.cells.push_back(it->name);
+ map[it.first] = info;
+ }
+}
+
+RTLIL::Wire *add_new_wire(RTLIL::Module *module, RTLIL::IdString name, int width = 1)
+{
+ if (module->count_id(name))
+ log_error("Attempting to create wire %s, but a wire of this name exists already! Hint: Try another value for -sep.\n", log_id(name));
+ return module->addWire(name, width);
+}
+
+struct ExposePass : public Pass {
+ ExposePass() : Pass("expose", "convert internal signals to module ports") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" expose [options] [selection]\n");
+ log("\n");
+ log("This command exposes all selected internal signals of a module as additional\n");
+ log("outputs.\n");
+ log("\n");
+ log(" -dff\n");
+ log(" only consider wires that are directly driven by register cell.\n");
+ log("\n");
+ log(" -cut\n");
+ log(" when exposing a wire, create an input/output pair and cut the internal\n");
+ log(" signal path at that wire.\n");
+ log("\n");
+ log(" -shared\n");
+ log(" only expose those signals that are shared among the selected modules.\n");
+ log(" this is useful for preparing modules for equivalence checking.\n");
+ log("\n");
+ log(" -evert\n");
+ log(" also turn connections to instances of other modules to additional\n");
+ log(" inputs and outputs and remove the module instances.\n");
+ log("\n");
+ log(" -evert-dff\n");
+ log(" turn flip-flops to sets of inputs and outputs.\n");
+ log("\n");
+ log(" -sep <separator>\n");
+ log(" when creating new wire/port names, the original object name is suffixed\n");
+ log(" with this separator (default: '.') and the port name or a type\n");
+ log(" designator for the exposed signal.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ bool flag_shared = false;
+ bool flag_evert = false;
+ bool flag_dff = false;
+ bool flag_cut = false;
+ bool flag_evert_dff = false;
+ std::string sep = ".";
+
+ log_header(design, "Executing EXPOSE pass (exposing internal signals as outputs).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-shared") {
+ flag_shared = true;
+ continue;
+ }
+ if (args[argidx] == "-evert") {
+ flag_evert = true;
+ continue;
+ }
+ if (args[argidx] == "-dff") {
+ flag_dff = true;
+ continue;
+ }
+ if (args[argidx] == "-cut") {
+ flag_cut = true;
+ continue;
+ }
+ if (args[argidx] == "-evert-dff") {
+ flag_evert_dff = true;
+ continue;
+ }
+ if (args[argidx] == "-sep" && argidx+1 < args.size()) {
+ sep = args[++argidx];
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ CellTypes ct(design);
+
+ std::map<RTLIL::Module*, std::map<RTLIL::IdString, dff_map_info_t>> dff_dq_maps;
+ std::map<RTLIL::Module*, std::set<RTLIL::IdString>> dff_cells;
+
+ if (flag_evert_dff)
+ {
+ RTLIL::Module *first_module = NULL;
+ std::set<RTLIL::IdString> shared_dff_wires;
+
+ for (auto &mod_it : design->modules_)
+ {
+ if (!design->selected(mod_it.second))
+ continue;
+
+ create_dff_dq_map(dff_dq_maps[mod_it.second], design, mod_it.second);
+
+ if (!flag_shared)
+ continue;
+
+ if (first_module == NULL) {
+ for (auto &it : dff_dq_maps[mod_it.second])
+ shared_dff_wires.insert(it.first);
+ first_module = mod_it.second;
+ } else {
+ std::set<RTLIL::IdString> new_shared_dff_wires;
+ for (auto &it : shared_dff_wires) {
+ if (!dff_dq_maps[mod_it.second].count(it))
+ continue;
+ if (!compare_wires(first_module->wires_.at(it), mod_it.second->wires_.at(it)))
+ continue;
+ new_shared_dff_wires.insert(it);
+ }
+ shared_dff_wires.swap(new_shared_dff_wires);
+ }
+ }
+
+ if (flag_shared)
+ for (auto &map_it : dff_dq_maps)
+ {
+ std::map<RTLIL::IdString, dff_map_info_t> new_map;
+ for (auto &it : map_it.second)
+ if (shared_dff_wires.count(it.first))
+ new_map[it.first] = it.second;
+ map_it.second.swap(new_map);
+ }
+
+ for (auto &it1 : dff_dq_maps)
+ for (auto &it2 : it1.second)
+ for (auto &it3 : it2.second.cells)
+ dff_cells[it1.first].insert(it3);
+ }
+
+ std::set<RTLIL::IdString> shared_wires, shared_cells;
+ std::set<RTLIL::IdString> used_names;
+
+ if (flag_shared)
+ {
+ RTLIL::Module *first_module = NULL;
+
+ for (auto &mod_it : design->modules_)
+ {
+ RTLIL::Module *module = mod_it.second;
+
+ if (!design->selected(module))
+ continue;
+
+ std::set<RTLIL::IdString> dff_wires;
+ if (flag_dff)
+ find_dff_wires(dff_wires, module);
+
+ if (first_module == NULL)
+ {
+ for (auto &it : module->wires_)
+ if (design->selected(module, it.second) && consider_wire(it.second, dff_dq_maps[module]))
+ if (!flag_dff || dff_wires.count(it.first))
+ shared_wires.insert(it.first);
+
+ if (flag_evert)
+ for (auto &it : module->cells_)
+ if (design->selected(module, it.second) && consider_cell(design, dff_cells[module], it.second))
+ shared_cells.insert(it.first);
+
+ first_module = module;
+ }
+ else
+ {
+ std::vector<RTLIL::IdString> delete_shared_wires, delete_shared_cells;
+
+ for (auto &it : shared_wires)
+ {
+ RTLIL::Wire *wire;
+
+ if (module->wires_.count(it) == 0)
+ goto delete_shared_wire;
+
+ wire = module->wires_.at(it);
+
+ if (!design->selected(module, wire))
+ goto delete_shared_wire;
+ if (!consider_wire(wire, dff_dq_maps[module]))
+ goto delete_shared_wire;
+ if (!compare_wires(first_module->wires_.at(it), wire))
+ goto delete_shared_wire;
+ if (flag_dff && !dff_wires.count(it))
+ goto delete_shared_wire;
+
+ if (0)
+ delete_shared_wire:
+ delete_shared_wires.push_back(it);
+ }
+
+ if (flag_evert)
+ for (auto &it : shared_cells)
+ {
+ RTLIL::Cell *cell;
+
+ if (module->cells_.count(it) == 0)
+ goto delete_shared_cell;
+
+ cell = module->cells_.at(it);
+
+ if (!design->selected(module, cell))
+ goto delete_shared_cell;
+ if (!consider_cell(design, dff_cells[module], cell))
+ goto delete_shared_cell;
+ if (!compare_cells(first_module->cells_.at(it), cell))
+ goto delete_shared_cell;
+
+ if (0)
+ delete_shared_cell:
+ delete_shared_cells.push_back(it);
+ }
+
+ for (auto &it : delete_shared_wires)
+ shared_wires.erase(it);
+ for (auto &it : delete_shared_cells)
+ shared_cells.erase(it);
+ }
+ }
+ }
+
+ for (auto &mod_it : design->modules_)
+ {
+ RTLIL::Module *module = mod_it.second;
+
+ if (!design->selected(module))
+ continue;
+
+ std::set<RTLIL::IdString> dff_wires;
+ if (flag_dff && !flag_shared)
+ find_dff_wires(dff_wires, module);
+
+ SigMap sigmap(module);
+
+ SigMap out_to_in_map;
+
+ for (auto &it : module->wires_)
+ {
+ if (flag_shared) {
+ if (shared_wires.count(it.first) == 0)
+ continue;
+ } else {
+ if (!design->selected(module, it.second) || !consider_wire(it.second, dff_dq_maps[module]))
+ continue;
+ if (flag_dff && !dff_wires.count(it.first))
+ continue;
+ }
+
+ if (!it.second->port_output) {
+ it.second->port_output = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(it.second->name));
+ }
+
+ if (flag_cut) {
+ RTLIL::Wire *in_wire = add_new_wire(module, it.second->name.str() + sep + "i", it.second->width);
+ in_wire->port_input = true;
+ out_to_in_map.add(sigmap(it.second), in_wire);
+ }
+ }
+
+ if (flag_cut)
+ {
+ for (auto &it : module->cells_) {
+ if (!ct.cell_known(it.second->type))
+ continue;
+ for (auto &conn : it.second->connections_)
+ if (ct.cell_input(it.second->type, conn.first))
+ conn.second = out_to_in_map(sigmap(conn.second));
+ }
+
+ for (auto &conn : module->connections_)
+ conn.second = out_to_in_map(sigmap(conn.second));
+ }
+
+ std::set<RTLIL::SigBit> set_q_bits;
+
+ for (auto &dq : dff_dq_maps[module])
+ {
+ if (!module->wires_.count(dq.first))
+ continue;
+
+ RTLIL::Wire *wire = module->wires_.at(dq.first);
+ std::set<RTLIL::SigBit> wire_bits_set = sigmap(wire).to_sigbit_set();
+ std::vector<RTLIL::SigBit> wire_bits_vec = sigmap(wire).to_sigbit_vector();
+
+ dff_map_info_t &info = dq.second;
+
+ RTLIL::Wire *wire_dummy_q = add_new_wire(module, NEW_ID, 0);
+
+ for (auto &cell_name : info.cells) {
+ RTLIL::Cell *cell = module->cells_.at(cell_name);
+ std::vector<RTLIL::SigBit> cell_q_bits = sigmap(cell->getPort("\\Q")).to_sigbit_vector();
+ for (auto &bit : cell_q_bits)
+ if (wire_bits_set.count(bit))
+ bit = RTLIL::SigBit(wire_dummy_q, wire_dummy_q->width++);
+ cell->setPort("\\Q", cell_q_bits);
+ }
+
+ RTLIL::Wire *wire_q = add_new_wire(module, wire->name.str() + sep + "q", wire->width);
+ wire_q->port_input = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_q->name));
+
+ RTLIL::SigSig connect_q;
+ for (size_t i = 0; i < wire_bits_vec.size(); i++) {
+ if (set_q_bits.count(wire_bits_vec[i]))
+ continue;
+ connect_q.first.append(wire_bits_vec[i]);
+ connect_q.second.append(RTLIL::SigBit(wire_q, i));
+ set_q_bits.insert(wire_bits_vec[i]);
+ }
+ module->connect(connect_q);
+
+ RTLIL::Wire *wire_d = add_new_wire(module, wire->name.str() + sep + "d", wire->width);
+ wire_d->port_output = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_d->name));
+ module->connect(RTLIL::SigSig(wire_d, info.sig_d));
+
+ RTLIL::Wire *wire_c = add_new_wire(module, wire->name.str() + sep + "c");
+ wire_c->port_output = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_c->name));
+ if (info.clk_polarity) {
+ module->connect(RTLIL::SigSig(wire_c, info.sig_clk));
+ } else {
+ RTLIL::Cell *c = module->addCell(NEW_ID, "$not");
+ c->parameters["\\A_SIGNED"] = 0;
+ c->parameters["\\A_WIDTH"] = 1;
+ c->parameters["\\Y_WIDTH"] = 1;
+ c->setPort("\\A", info.sig_clk);
+ c->setPort("\\Y", wire_c);
+ }
+
+ if (info.sig_arst != RTLIL::State::Sm)
+ {
+ RTLIL::Wire *wire_r = add_new_wire(module, wire->name.str() + sep + "r");
+ wire_r->port_output = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_r->name));
+ if (info.arst_polarity) {
+ module->connect(RTLIL::SigSig(wire_r, info.sig_arst));
+ } else {
+ RTLIL::Cell *c = module->addCell(NEW_ID, "$not");
+ c->parameters["\\A_SIGNED"] = 0;
+ c->parameters["\\A_WIDTH"] = 1;
+ c->parameters["\\Y_WIDTH"] = 1;
+ c->setPort("\\A", info.sig_arst);
+ c->setPort("\\Y", wire_r);
+ }
+
+ RTLIL::Wire *wire_v = add_new_wire(module, wire->name.str() + sep + "v", wire->width);
+ wire_v->port_output = true;
+ log("New module port: %s/%s\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire_v->name));
+ module->connect(RTLIL::SigSig(wire_v, info.arst_value));
+ }
+ }
+
+ if (flag_evert)
+ {
+ std::vector<RTLIL::Cell*> delete_cells;
+
+ for (auto &it : module->cells_)
+ {
+ if (flag_shared) {
+ if (shared_cells.count(it.first) == 0)
+ continue;
+ } else {
+ if (!design->selected(module, it.second) || !consider_cell(design, dff_cells[module], it.second))
+ continue;
+ }
+
+ RTLIL::Cell *cell = it.second;
+
+ if (design->modules_.count(cell->type))
+ {
+ RTLIL::Module *mod = design->modules_.at(cell->type);
+
+ for (auto &it : mod->wires_)
+ {
+ RTLIL::Wire *p = it.second;
+ if (!p->port_input && !p->port_output)
+ continue;
+
+ RTLIL::Wire *w = add_new_wire(module, cell->name.str() + sep + RTLIL::unescape_id(p->name), p->width);
+ if (p->port_input)
+ w->port_output = true;
+ if (p->port_output)
+ w->port_input = true;
+
+ log("New module port: %s/%s (%s)\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name), RTLIL::id2cstr(cell->type));
+
+ RTLIL::SigSpec sig;
+ if (cell->hasPort(p->name))
+ sig = cell->getPort(p->name);
+ sig.extend_u0(w->width);
+ if (w->port_input)
+ module->connect(RTLIL::SigSig(sig, w));
+ else
+ module->connect(RTLIL::SigSig(w, sig));
+ }
+ }
+ else
+ {
+ for (auto &it : cell->connections())
+ {
+ RTLIL::Wire *w = add_new_wire(module, cell->name.str() + sep + RTLIL::unescape_id(it.first), it.second.size());
+ if (ct.cell_input(cell->type, it.first))
+ w->port_output = true;
+ if (ct.cell_output(cell->type, it.first))
+ w->port_input = true;
+
+ log("New module port: %s/%s (%s)\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(w->name), RTLIL::id2cstr(cell->type));
+
+ if (w->port_input)
+ module->connect(RTLIL::SigSig(it.second, w));
+ else
+ module->connect(RTLIL::SigSig(w, it.second));
+ }
+ }
+
+ delete_cells.push_back(cell);
+ }
+
+ for (auto cell : delete_cells) {
+ log("Removing cell: %s/%s (%s)\n", log_id(module), log_id(cell), log_id(cell->type));
+ module->remove(cell);
+ }
+ }
+
+ module->fixup_ports();
+ }
+ }
+} ExposePass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
new file mode 100644
index 00000000..77263f6a
--- /dev/null
+++ b/passes/sat/freduce.cc
@@ -0,0 +1,840 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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"
+#include "kernel/celltypes.h"
+#include "kernel/consteval.h"
+#include "kernel/sigtools.h"
+#include "kernel/log.h"
+#include "kernel/satgen.h"
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <algorithm>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+bool inv_mode;
+int verbose_level, reduce_counter, reduce_stop_at;
+typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
+std::string dump_prefix;
+
+struct equiv_bit_t
+{
+ int depth;
+ bool inverted;
+ RTLIL::Cell *drv;
+ RTLIL::SigBit bit;
+
+ bool operator<(const equiv_bit_t &other) const {
+ if (depth != other.depth)
+ return depth < other.depth;
+ if (inverted != other.inverted)
+ return inverted < other.inverted;
+ if (drv != other.drv)
+ return drv < other.drv;
+ return bit < other.bit;
+ }
+};
+
+struct CountBitUsage
+{
+ SigMap &sigmap;
+ std::map<RTLIL::SigBit, int> &cache;
+
+ CountBitUsage(SigMap &sigmap, std::map<RTLIL::SigBit, int> &cache) : sigmap(sigmap), cache(cache) { }
+
+ void operator()(RTLIL::SigSpec &sig) {
+ std::vector<RTLIL::SigBit> vec = sigmap(sig).to_sigbit_vector();
+ for (auto &bit : vec)
+ cache[bit]++;
+ }
+};
+
+struct FindReducedInputs
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
+
+ ezSatPtr ez;
+ std::set<RTLIL::Cell*> ez_cells;
+ SatGen satgen;
+
+ std::map<RTLIL::SigBit, int> sat_pi;
+ std::vector<int> sat_pi_uniq_bitvec;
+
+ FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
+ sigmap(sigmap), drivers(drivers), satgen(ez.get(), &sigmap)
+ {
+ satgen.model_undef = true;
+ }
+
+ int get_bits(int val)
+ {
+ int bits = 0;
+ for (int i = 8*sizeof(int); val; i = i >> 1)
+ if (val >> (i-1)) {
+ bits += i;
+ val = val >> i;
+ }
+ return bits;
+ }
+
+ void register_pi_bit(RTLIL::SigBit bit)
+ {
+ if (sat_pi.count(bit) != 0)
+ return;
+
+ satgen.setContext(&sigmap, "A");
+ int sat_a = satgen.importSigSpec(bit).front();
+ ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front()));
+
+ satgen.setContext(&sigmap, "B");
+ int sat_b = satgen.importSigSpec(bit).front();
+ ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front()));
+
+ int idx = sat_pi.size();
+ size_t idx_bits = get_bits(idx);
+
+ if (sat_pi_uniq_bitvec.size() != idx_bits) {
+ sat_pi_uniq_bitvec.push_back(ez->frozen_literal(stringf("uniq_%d", int(idx_bits)-1)));
+ for (auto &it : sat_pi)
+ ez->assume(ez->OR(ez->NOT(it.second), ez->NOT(sat_pi_uniq_bitvec.back())));
+ }
+ log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
+
+ sat_pi[bit] = ez->frozen_literal(stringf("p, falsei_%s", log_signal(bit)));
+ ez->assume(ez->IFF(ez->XOR(sat_a, sat_b), sat_pi[bit]));
+
+ for (size_t i = 0; i < idx_bits; i++)
+ if ((idx & (1 << i)) == 0)
+ ez->assume(ez->OR(ez->NOT(sat_pi[bit]), ez->NOT(sat_pi_uniq_bitvec[i])));
+ else
+ ez->assume(ez->OR(ez->NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
+ }
+
+ void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
+ {
+ if (out.wire == NULL)
+ return;
+ if (sigdone.count(out) != 0)
+ return;
+ sigdone.insert(out);
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (ez_cells.count(drv.first) == 0) {
+ satgen.setContext(&sigmap, "A");
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ satgen.setContext(&sigmap, "B");
+ if (!satgen.importCell(drv.first))
+ log_abort();
+ ez_cells.insert(drv.first);
+ }
+ for (auto &bit : drv.second)
+ register_cone_worker(pi, sigdone, bit);
+ } else {
+ register_pi_bit(out);
+ pi.insert(out);
+ }
+ }
+
+ void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
+ {
+ std::set<RTLIL::SigBit> pi_set, sigdone;
+ register_cone_worker(pi_set, sigdone, out);
+ pi.clear();
+ pi.insert(pi.end(), pi_set.begin(), pi_set.end());
+ }
+
+ void analyze(std::vector<RTLIL::SigBit> &reduced_inputs, RTLIL::SigBit output, int prec)
+ {
+ if (verbose_level >= 1)
+ log("[%2d%%] Analyzing input cone for signal %s:\n", prec, log_signal(output));
+
+ std::vector<RTLIL::SigBit> pi;
+ register_cone(pi, output);
+
+ if (verbose_level >= 1)
+ log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size()));
+
+ satgen.setContext(&sigmap, "A");
+ int output_a = satgen.importSigSpec(output).front();
+ int output_undef_a = satgen.importUndefSigSpec(output).front();
+
+ satgen.setContext(&sigmap, "B");
+ int output_b = satgen.importSigSpec(output).front();
+ int output_undef_b = satgen.importUndefSigSpec(output).front();
+
+ std::set<int> unused_pi_idx;
+
+ for (size_t i = 0; i < pi.size(); i++)
+ unused_pi_idx.insert(i);
+
+ while (1)
+ {
+ std::vector<int> model_pi_idx;
+ std::vector<int> model_expr;
+ std::vector<bool> model;
+
+ for (size_t i = 0; i < pi.size(); i++)
+ if (unused_pi_idx.count(i) != 0) {
+ model_pi_idx.push_back(i);
+ model_expr.push_back(sat_pi.at(pi[i]));
+ }
+
+ if (!ez->solve(model_expr, model, ez->expression(ezSAT::OpOr, model_expr), ez->XOR(output_a, output_b), ez->NOT(output_undef_a), ez->NOT(output_undef_b)))
+ break;
+
+ int found_count = 0;
+ for (size_t i = 0; i < model_pi_idx.size(); i++)
+ if (model[i]) {
+ if (verbose_level >= 2)
+ log(" Found relevant input: %s\n", log_signal(pi[model_pi_idx[i]]));
+ unused_pi_idx.erase(model_pi_idx[i]);
+ found_count++;
+ }
+ log_assert(found_count == 1);
+ }
+
+ for (size_t i = 0; i < pi.size(); i++)
+ if (unused_pi_idx.count(i) == 0)
+ reduced_inputs.push_back(pi[i]);
+
+ if (verbose_level >= 1)
+ log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
+ }
+};
+
+struct PerformReduction
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
+ pool<SigBit> recursion_guard;
+
+ ezSatPtr ez;
+ SatGen satgen;
+
+ std::vector<int> sat_pi, sat_out, sat_def;
+ std::vector<RTLIL::SigBit> out_bits, pi_bits;
+ std::vector<bool> out_inverted;
+ std::vector<int> out_depth;
+ int cone_size;
+
+ int register_cone_worker(std::set<RTLIL::Cell*> &celldone, std::map<RTLIL::SigBit, int> &sigdepth, RTLIL::SigBit out)
+ {
+ if (out.wire == NULL)
+ return 0;
+ if (sigdepth.count(out) != 0)
+ return sigdepth.at(out);
+
+ if (recursion_guard.count(out)) {
+ string loop_signals;
+ for (auto loop_bit : recursion_guard)
+ loop_signals += string(" ") + log_signal(loop_bit);
+ log_error("Found logic loop:%s\n", loop_signals.c_str());
+ }
+
+ recursion_guard.insert(out);
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (celldone.count(drv.first) == 0) {
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ celldone.insert(drv.first);
+ }
+ int max_child_depth = 0;
+ for (auto &bit : drv.second)
+ max_child_depth = max(register_cone_worker(celldone, sigdepth, bit), max_child_depth);
+ sigdepth[out] = max_child_depth + 1;
+ } else {
+ pi_bits.push_back(out);
+ sat_pi.push_back(satgen.importSigSpec(out).front());
+ ez->assume(ez->NOT(satgen.importUndefSigSpec(out).front()));
+ sigdepth[out] = 0;
+ }
+
+ recursion_guard.erase(out);
+ return sigdepth.at(out);
+ }
+
+ PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits, int cone_size) :
+ sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(ez.get(), &sigmap), out_bits(bits), cone_size(cone_size)
+ {
+ satgen.model_undef = true;
+
+ std::set<RTLIL::Cell*> celldone;
+ std::map<RTLIL::SigBit, int> sigdepth;
+
+ for (auto &bit : bits) {
+ out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
+ sat_out.push_back(satgen.importSigSpec(bit).front());
+ sat_def.push_back(ez->NOT(satgen.importUndefSigSpec(bit).front()));
+ }
+
+ if (inv_mode && cone_size > 0) {
+ if (!ez->solve(sat_out, out_inverted, ez->expression(ezSAT::OpAnd, sat_def)))
+ log_error("Solving for initial model failed!\n");
+ for (size_t i = 0; i < sat_out.size(); i++)
+ if (out_inverted.at(i))
+ sat_out[i] = ez->NOT(sat_out[i]);
+ } else
+ out_inverted = std::vector<bool>(sat_out.size(), false);
+ }
+
+ void analyze_const(std::vector<std::vector<equiv_bit_t>> &results, int idx)
+ {
+ if (verbose_level == 1)
+ log(" Finding const value for %s.\n", log_signal(out_bits[idx]));
+
+ bool can_be_set = ez->solve(ez->AND(sat_out[idx], sat_def[idx]));
+ bool can_be_clr = ez->solve(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
+ log_assert(!can_be_set || !can_be_clr);
+
+ RTLIL::SigBit value(RTLIL::State::Sx);
+ if (can_be_set)
+ value = RTLIL::State::S1;
+ if (can_be_clr)
+ value = RTLIL::State::S0;
+ if (verbose_level == 1)
+ log(" Constant value for this signal: %s\n", log_signal(value));
+
+ int result_idx = -1;
+ for (size_t i = 0; i < results.size(); i++) {
+ if (results[i].front().bit == value) {
+ result_idx = i;
+ break;
+ }
+ }
+
+ if (result_idx == -1) {
+ result_idx = results.size();
+ results.push_back(std::vector<equiv_bit_t>());
+ equiv_bit_t bit;
+ bit.depth = 0;
+ bit.inverted = false;
+ bit.drv = NULL;
+ bit.bit = value;
+ results.back().push_back(bit);
+ }
+
+ equiv_bit_t bit;
+ bit.depth = 1;
+ bit.inverted = false;
+ bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
+ bit.bit = out_bits[idx];
+ results[result_idx].push_back(bit);
+ }
+
+ void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, std::string indent1, std::string indent2)
+ {
+ std::string indent = indent1 + indent2;
+ const char *indt = indent.c_str();
+
+ if (bucket.size() <= 1)
+ return;
+
+ if (verbose_level == 1)
+ log("%s Trying to shatter bucket with %d signals.\n", indt, int(bucket.size()));
+
+ if (verbose_level > 1) {
+ std::vector<RTLIL::SigBit> bucket_sigbits;
+ for (int idx : bucket)
+ bucket_sigbits.push_back(out_bits[idx]);
+ log("%s Trying to shatter bucket with %d signals: %s\n", indt, int(bucket.size()), log_signal(bucket_sigbits));
+ }
+
+ std::vector<int> sat_set_list, sat_clr_list;
+ for (int idx : bucket) {
+ sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+ sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
+ }
+
+ std::vector<int> modelVars = sat_out;
+ std::vector<bool> model;
+
+ modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+ if (verbose_level >= 2)
+ modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
+
+ if (ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list)))
+ {
+ int iter_count = 1;
+
+ while (1)
+ {
+ sat_set_list.clear();
+ sat_clr_list.clear();
+
+ std::vector<int> sat_def_list;
+
+ for (int idx : bucket)
+ if (!model[sat_out.size() + idx]) {
+ sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx]));
+ sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx]));
+ } else {
+ sat_def_list.push_back(sat_def[idx]);
+ }
+
+ if (!ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list), ez->expression(ezSAT::OpAnd, sat_def_list)))
+ break;
+ iter_count++;
+ }
+
+ if (verbose_level >= 1) {
+ int count_set = 0, count_clr = 0, count_undef = 0;
+ for (int idx : bucket)
+ if (!model[sat_out.size() + idx])
+ count_undef++;
+ else if (model[idx])
+ count_set++;
+ else
+ count_clr++;
+ log("%s After %d iterations: %d set vs. %d clr vs %d undef\n", indt, iter_count, count_set, count_clr, count_undef);
+ }
+
+ if (verbose_level >= 2) {
+ for (size_t i = 0; i < pi_bits.size(); i++)
+ log("%s -> PI %c == %s\n", indt, model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i]));
+ for (int idx : bucket)
+ log("%s -> OUT %c == %s%s\n", indt, model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x',
+ out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
+ }
+
+ std::vector<int> buckets_a;
+ std::vector<int> buckets_b;
+
+ for (int idx : bucket) {
+ if (!model[sat_out.size() + idx] || model[idx])
+ buckets_a.push_back(idx);
+ if (!model[sat_out.size() + idx] || !model[idx])
+ buckets_b.push_back(idx);
+ }
+ analyze(results, results_map, buckets_a, indent1 + ".", indent2 + " ");
+ analyze(results, results_map, buckets_b, indent1 + "x", indent2 + " ");
+ }
+ else
+ {
+ std::vector<int> undef_slaves;
+
+ for (int idx : bucket) {
+ std::vector<int> sat_def_list;
+ for (int idx2 : bucket)
+ if (idx != idx2)
+ sat_def_list.push_back(sat_def[idx2]);
+ if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
+ undef_slaves.push_back(idx);
+ }
+
+ if (undef_slaves.size() == bucket.size()) {
+ if (verbose_level >= 1)
+ log("%s Complex undef overlap. None of the signals covers the others.\n", indt);
+ // FIXME: We could try to further shatter a group with complex undef overlaps
+ return;
+ }
+
+ for (int idx : undef_slaves)
+ out_depth[idx] = std::numeric_limits<int>::max();
+
+ if (verbose_level >= 1) {
+ log("%s Found %d equivalent signals:", indt, int(bucket.size()));
+ for (int idx : bucket)
+ log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
+ log("\n");
+ }
+
+ int result_idx = -1;
+ for (int idx : bucket) {
+ if (results_map.count(idx) == 0)
+ continue;
+ if (result_idx == -1) {
+ result_idx = results_map.at(idx);
+ continue;
+ }
+ int result_idx2 = results_map.at(idx);
+ results[result_idx].insert(results[result_idx2].begin(), results[result_idx2].end());
+ for (int idx2 : results[result_idx2])
+ results_map[idx2] = result_idx;
+ results[result_idx2].clear();
+ }
+
+ if (result_idx == -1) {
+ result_idx = results.size();
+ results.push_back(std::set<int>());
+ }
+
+ results[result_idx].insert(bucket.begin(), bucket.end());
+ }
+ }
+
+ void analyze(std::vector<std::vector<equiv_bit_t>> &results, int perc)
+ {
+ std::vector<int> bucket;
+ for (size_t i = 0; i < sat_out.size(); i++)
+ bucket.push_back(i);
+
+ std::vector<std::set<int>> results_buf;
+ std::map<int, int> results_map;
+ analyze(results_buf, results_map, bucket, stringf("[%2d%%] %d ", perc, cone_size), "");
+
+ for (auto &r : results_buf)
+ {
+ if (r.size() <= 1)
+ continue;
+
+ if (verbose_level >= 1) {
+ std::vector<RTLIL::SigBit> r_sigbits;
+ for (int idx : r)
+ r_sigbits.push_back(out_bits[idx]);
+ log(" Found group of %d equivalent signals: %s\n", int(r.size()), log_signal(r_sigbits));
+ }
+
+ std::vector<int> undef_slaves;
+
+ for (int idx : r) {
+ std::vector<int> sat_def_list;
+ for (int idx2 : r)
+ if (idx != idx2)
+ sat_def_list.push_back(sat_def[idx2]);
+ if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list)))
+ undef_slaves.push_back(idx);
+ }
+
+ if (undef_slaves.size() == bucket.size()) {
+ if (verbose_level >= 1)
+ log(" Complex undef overlap. None of the signals covers the others.\n");
+ // FIXME: We could try to further shatter a group with complex undef overlaps
+ return;
+ }
+
+ for (int idx : undef_slaves)
+ out_depth[idx] = std::numeric_limits<int>::max();
+
+ std::vector<equiv_bit_t> result;
+
+ for (int idx : r) {
+ equiv_bit_t bit;
+ bit.depth = out_depth[idx];
+ bit.inverted = out_inverted[idx];
+ bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
+ bit.bit = out_bits[idx];
+ result.push_back(bit);
+ }
+
+ std::sort(result.begin(), result.end());
+
+ if (result.front().inverted)
+ for (auto &bit : result)
+ bit.inverted = !bit.inverted;
+
+ for (size_t i = 1; i < result.size(); i++) {
+ std::pair<RTLIL::SigBit, RTLIL::SigBit> p(result[0].bit, result[i].bit);
+ if (inv_pairs.count(p) != 0)
+ result.erase(result.begin() + i);
+ }
+
+ if (result.size() > 1)
+ results.push_back(result);
+ }
+ }
+};
+
+struct FreduceWorker
+{
+ RTLIL::Design *design;
+ RTLIL::Module *module;
+
+ SigMap sigmap;
+ drivers_t drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
+
+ FreduceWorker(RTLIL::Design *design, RTLIL::Module *module) : design(design), module(module), sigmap(module)
+ {
+ }
+
+ bool find_bit_in_cone(std::set<RTLIL::Cell*> &celldone, RTLIL::SigBit needle, RTLIL::SigBit haystack)
+ {
+ if (needle == haystack)
+ return true;
+ if (haystack.wire == NULL || needle.wire == NULL || drivers.count(haystack) == 0)
+ return false;
+
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(haystack);
+
+ if (celldone.count(drv.first))
+ return false;
+ celldone.insert(drv.first);
+
+ for (auto &bit : drv.second)
+ if (find_bit_in_cone(celldone, needle, bit))
+ return true;
+ return false;
+ }
+
+ bool find_bit_in_cone(RTLIL::SigBit needle, RTLIL::SigBit haystack)
+ {
+ std::set<RTLIL::Cell*> celldone;
+ return find_bit_in_cone(celldone, needle, haystack);
+ }
+
+ void dump()
+ {
+ std::string filename = stringf("%s_%s_%05d.il", dump_prefix.c_str(), RTLIL::id2cstr(module->name), reduce_counter);
+ log("%s Writing dump file `%s'.\n", reduce_counter ? " " : "", filename.c_str());
+ Pass::call(design, stringf("dump -outfile %s %s", filename.c_str(), design->selected_active_module.empty() ? module->name.c_str() : ""));
+ }
+
+ int run()
+ {
+ log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
+
+ CellTypes ct;
+ ct.setup_internals();
+ ct.setup_stdcells();
+
+ int bits_full_total = 0;
+ std::vector<std::set<RTLIL::SigBit>> batches;
+ for (auto &it : module->wires_)
+ if (it.second->port_input) {
+ batches.push_back(sigmap(it.second).to_sigbit_set());
+ bits_full_total += it.second->width;
+ }
+ for (auto &it : module->cells_) {
+ if (ct.cell_known(it.second->type)) {
+ std::set<RTLIL::SigBit> inputs, outputs;
+ for (auto &port : it.second->connections()) {
+ std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
+ if (ct.cell_output(it.second->type, port.first))
+ outputs.insert(bits.begin(), bits.end());
+ else
+ inputs.insert(bits.begin(), bits.end());
+ }
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> drv(it.second, inputs);
+ for (auto &bit : outputs)
+ drivers[bit] = drv;
+ batches.push_back(outputs);
+ bits_full_total += outputs.size();
+ }
+ if (inv_mode && it.second->type == "$_NOT_")
+ inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->getPort("\\A")), sigmap(it.second->getPort("\\Y"))));
+ }
+
+ int bits_count = 0;
+ int bits_full_count = 0;
+ std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
+ for (auto &batch : batches)
+ {
+ for (auto &bit : batch)
+ if (bit.wire != NULL && design->selected(module, bit.wire))
+ goto found_selected_wire;
+ bits_full_count += batch.size();
+ continue;
+
+ found_selected_wire:
+ log(" Finding reduced input cone for signal batch %s%c\n",
+ log_signal(batch), verbose_level ? ':' : '.');
+
+ FindReducedInputs infinder(sigmap, drivers);
+ for (auto &bit : batch) {
+ std::vector<RTLIL::SigBit> inputs;
+ infinder.analyze(inputs, bit, 100 * bits_full_count / bits_full_total);
+ buckets[inputs].push_back(bit);
+ bits_full_count++;
+ bits_count++;
+ }
+ }
+ log(" Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
+
+ int bucket_count = 0;
+ std::vector<std::vector<equiv_bit_t>> equiv;
+ for (auto &bucket : buckets)
+ {
+ bucket_count++;
+
+ if (bucket.second.size() == 1)
+ continue;
+
+ if (bucket.first.size() == 0) {
+ log(" Finding const values for bucket %s%c\n", log_signal(bucket.second), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
+ for (size_t idx = 0; idx < bucket.second.size(); idx++)
+ worker.analyze_const(equiv, idx);
+ } else {
+ log(" Trying to shatter bucket %s%c\n", log_signal(bucket.second), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second, bucket.first.size());
+ worker.analyze(equiv, 100 * bucket_count / (buckets.size() + 1));
+ }
+ }
+
+ std::map<RTLIL::SigBit, int> bitusage;
+ module->rewrite_sigspecs(CountBitUsage(sigmap, bitusage));
+
+ if (!dump_prefix.empty())
+ dump();
+
+ log(" Rewiring %d equivalent groups:\n", int(equiv.size()));
+ int rewired_sigbits = 0;
+ for (auto &grp : equiv)
+ {
+ log(" [%05d] Using as master for group: %s\n", ++reduce_counter, log_signal(grp.front().bit));
+
+ RTLIL::SigSpec inv_sig;
+ for (size_t i = 1; i < grp.size(); i++)
+ {
+ if (!design->selected(module, grp[i].bit.wire)) {
+ log(" Skipping not-selected slave: %s\n", log_signal(grp[i].bit));
+ continue;
+ }
+
+ if (grp[i].bit.wire->port_id == 0 && bitusage[grp[i].bit] <= 1) {
+ log(" Skipping unused slave: %s\n", log_signal(grp[i].bit));
+ continue;
+ }
+
+ if (find_bit_in_cone(grp[i].bit, grp.front().bit)) {
+ log(" Skipping dependency of master: %s\n", log_signal(grp[i].bit));
+ continue;
+ }
+
+ log(" Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
+
+ RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
+ RTLIL::Wire *dummy_wire = module->addWire(NEW_ID);
+ for (auto &port : drv->connections_)
+ if (ct.cell_output(drv->type, port.first))
+ sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
+
+ if (grp[i].inverted)
+ {
+ if (inv_sig.size() == 0)
+ {
+ inv_sig = module->addWire(NEW_ID);
+
+ RTLIL::Cell *inv_cell = module->addCell(NEW_ID, "$_NOT_");
+ inv_cell->setPort("\\A", grp[0].bit);
+ inv_cell->setPort("\\Y", inv_sig);
+ }
+
+ module->connect(RTLIL::SigSig(grp[i].bit, inv_sig));
+ }
+ else
+ module->connect(RTLIL::SigSig(grp[i].bit, grp[0].bit));
+
+ rewired_sigbits++;
+ }
+
+ if (!dump_prefix.empty())
+ dump();
+
+ if (reduce_counter == reduce_stop_at) {
+ log(" Reached limit passed using -stop option. Skipping all further reductions.\n");
+ break;
+ }
+ }
+
+ log(" Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
+ return rewired_sigbits;
+ }
+};
+
+struct FreducePass : public Pass {
+ FreducePass() : Pass("freduce", "perform functional reduction") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" freduce [options] [selection]\n");
+ log("\n");
+ log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
+ log("equivalent, they are merged to one node and one of the redundant drivers is\n");
+ log("disconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
+ log("\n");
+ log(" -v, -vv\n");
+ log(" enable verbose or very verbose output\n");
+ log("\n");
+ log(" -inv\n");
+ log(" enable explicit handling of inverted signals\n");
+ log("\n");
+ log(" -stop <n>\n");
+ log(" stop after <n> reduction operations. this is mostly used for\n");
+ log(" debugging the freduce command itself.\n");
+ log("\n");
+ log(" -dump <prefix>\n");
+ log(" dump the design to <prefix>_<module>_<num>.il after each reduction\n");
+ log(" operation. this is mostly used for debugging the freduce command.\n");
+ log("\n");
+ log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
+ log("equivalent nodes.\n");
+ log("\n");
+ log("All selected wires are considered for rewiring. The selected cells cover the\n");
+ log("circuit that is analyzed.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ reduce_counter = 0;
+ reduce_stop_at = 0;
+ verbose_level = 0;
+ inv_mode = false;
+ dump_prefix = std::string();
+
+ log_header(design, "Executing FREDUCE pass (perform functional reduction).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-v") {
+ verbose_level = 1;
+ continue;
+ }
+ if (args[argidx] == "-vv") {
+ verbose_level = 2;
+ continue;
+ }
+ if (args[argidx] == "-inv") {
+ inv_mode = true;
+ continue;
+ }
+ if (args[argidx] == "-stop" && argidx+1 < args.size()) {
+ reduce_stop_at = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-dump" && argidx+1 < args.size()) {
+ dump_prefix = args[++argidx];
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ int bitcount = 0;
+ for (auto &mod_it : design->modules_) {
+ RTLIL::Module *module = mod_it.second;
+ if (design->selected(module))
+ bitcount += FreduceWorker(design, module).run();
+ }
+
+ log("Rewired a total of %d signal bits.\n", bitcount);
+ }
+} FreducePass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
new file mode 100644
index 00000000..9e150b60
--- /dev/null
+++ b/passes/sat/miter.cc
@@ -0,0 +1,421 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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"
+#include "kernel/rtlil.h"
+#include "kernel/log.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
+{
+ bool flag_ignore_gold_x = false;
+ bool flag_make_outputs = false;
+ bool flag_make_outcmp = false;
+ bool flag_make_assert = false;
+ bool flag_flatten = false;
+
+ log_header(design, "Executing MITER pass (creating miter circuit).\n");
+
+ size_t argidx;
+ for (argidx = 2; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-ignore_gold_x") {
+ flag_ignore_gold_x = true;
+ continue;
+ }
+ if (args[argidx] == "-make_outputs") {
+ flag_make_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-make_outcmp") {
+ flag_make_outcmp = true;
+ continue;
+ }
+ if (args[argidx] == "-make_assert") {
+ flag_make_assert = true;
+ continue;
+ }
+ if (args[argidx] == "-flatten") {
+ flag_flatten = true;
+ continue;
+ }
+ break;
+ }
+ if (argidx+3 != args.size() || args[argidx].substr(0, 1) == "-")
+ that->cmd_error(args, argidx, "command argument error");
+
+ RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
+ RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]);
+ RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]);
+
+ if (design->modules_.count(gold_name) == 0)
+ log_cmd_error("Can't find gold module %s!\n", gold_name.c_str());
+ if (design->modules_.count(gate_name) == 0)
+ log_cmd_error("Can't find gate module %s!\n", gate_name.c_str());
+ if (design->modules_.count(miter_name) != 0)
+ log_cmd_error("There is already a module %s!\n", miter_name.c_str());
+
+ RTLIL::Module *gold_module = design->modules_.at(gold_name);
+ RTLIL::Module *gate_module = design->modules_.at(gate_name);
+
+ for (auto &it : gold_module->wires_) {
+ RTLIL::Wire *w1 = it.second, *w2;
+ if (w1->port_id == 0)
+ continue;
+ if (gate_module->wires_.count(it.second->name) == 0)
+ goto match_gold_port_error;
+ w2 = gate_module->wires_.at(it.second->name);
+ if (w1->port_input != w2->port_input)
+ goto match_gold_port_error;
+ if (w1->port_output != w2->port_output)
+ goto match_gold_port_error;
+ if (w1->width != w2->width)
+ goto match_gold_port_error;
+ continue;
+ match_gold_port_error:
+ log_cmd_error("No matching port in gate module was found for %s!\n", it.second->name.c_str());
+ }
+
+ for (auto &it : gate_module->wires_) {
+ RTLIL::Wire *w1 = it.second, *w2;
+ if (w1->port_id == 0)
+ continue;
+ if (gold_module->wires_.count(it.second->name) == 0)
+ goto match_gate_port_error;
+ w2 = gold_module->wires_.at(it.second->name);
+ if (w1->port_input != w2->port_input)
+ goto match_gate_port_error;
+ if (w1->port_output != w2->port_output)
+ goto match_gate_port_error;
+ if (w1->width != w2->width)
+ goto match_gate_port_error;
+ continue;
+ match_gate_port_error:
+ log_cmd_error("No matching port in gold module was found for %s!\n", it.second->name.c_str());
+ }
+
+ log("Creating miter cell \"%s\" with gold cell \"%s\" and gate cell \"%s\".\n", RTLIL::id2cstr(miter_name), RTLIL::id2cstr(gold_name), RTLIL::id2cstr(gate_name));
+
+ RTLIL::Module *miter_module = new RTLIL::Module;
+ miter_module->name = miter_name;
+ design->add(miter_module);
+
+ RTLIL::Cell *gold_cell = miter_module->addCell("\\gold", gold_name);
+ RTLIL::Cell *gate_cell = miter_module->addCell("\\gate", gate_name);
+
+ RTLIL::SigSpec all_conditions;
+
+ for (auto &it : gold_module->wires_)
+ {
+ RTLIL::Wire *w1 = it.second;
+
+ if (w1->port_input)
+ {
+ RTLIL::Wire *w2 = miter_module->addWire("\\in_" + RTLIL::unescape_id(w1->name), w1->width);
+ w2->port_input = true;
+
+ gold_cell->setPort(w1->name, w2);
+ gate_cell->setPort(w1->name, w2);
+ }
+
+ if (w1->port_output)
+ {
+ RTLIL::Wire *w2_gold = miter_module->addWire("\\gold_" + RTLIL::unescape_id(w1->name), w1->width);
+ w2_gold->port_output = flag_make_outputs;
+
+ RTLIL::Wire *w2_gate = miter_module->addWire("\\gate_" + RTLIL::unescape_id(w1->name), w1->width);
+ w2_gate->port_output = flag_make_outputs;
+
+ gold_cell->setPort(w1->name, w2_gold);
+ gate_cell->setPort(w1->name, w2_gate);
+
+ RTLIL::SigSpec this_condition;
+
+ if (flag_ignore_gold_x)
+ {
+ RTLIL::SigSpec gold_x = miter_module->addWire(NEW_ID, w2_gold->width);
+ for (int i = 0; i < w2_gold->width; i++) {
+ RTLIL::Cell *eqx_cell = miter_module->addCell(NEW_ID, "$eqx");
+ eqx_cell->parameters["\\A_WIDTH"] = 1;
+ eqx_cell->parameters["\\B_WIDTH"] = 1;
+ eqx_cell->parameters["\\Y_WIDTH"] = 1;
+ eqx_cell->parameters["\\A_SIGNED"] = 0;
+ eqx_cell->parameters["\\B_SIGNED"] = 0;
+ eqx_cell->setPort("\\A", RTLIL::SigSpec(w2_gold, i));
+ eqx_cell->setPort("\\B", RTLIL::State::Sx);
+ eqx_cell->setPort("\\Y", gold_x.extract(i, 1));
+ }
+
+ RTLIL::SigSpec gold_masked = miter_module->addWire(NEW_ID, w2_gold->width);
+ RTLIL::SigSpec gate_masked = miter_module->addWire(NEW_ID, w2_gate->width);
+
+ RTLIL::Cell *or_gold_cell = miter_module->addCell(NEW_ID, "$or");
+ or_gold_cell->parameters["\\A_WIDTH"] = w2_gold->width;
+ or_gold_cell->parameters["\\B_WIDTH"] = w2_gold->width;
+ or_gold_cell->parameters["\\Y_WIDTH"] = w2_gold->width;
+ or_gold_cell->parameters["\\A_SIGNED"] = 0;
+ or_gold_cell->parameters["\\B_SIGNED"] = 0;
+ or_gold_cell->setPort("\\A", w2_gold);
+ or_gold_cell->setPort("\\B", gold_x);
+ or_gold_cell->setPort("\\Y", gold_masked);
+
+ RTLIL::Cell *or_gate_cell = miter_module->addCell(NEW_ID, "$or");
+ or_gate_cell->parameters["\\A_WIDTH"] = w2_gate->width;
+ or_gate_cell->parameters["\\B_WIDTH"] = w2_gate->width;
+ or_gate_cell->parameters["\\Y_WIDTH"] = w2_gate->width;
+ or_gate_cell->parameters["\\A_SIGNED"] = 0;
+ or_gate_cell->parameters["\\B_SIGNED"] = 0;
+ or_gate_cell->setPort("\\A", w2_gate);
+ or_gate_cell->setPort("\\B", gold_x);
+ or_gate_cell->setPort("\\Y", gate_masked);
+
+ RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
+ eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
+ eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
+ eq_cell->parameters["\\Y_WIDTH"] = 1;
+ eq_cell->parameters["\\A_SIGNED"] = 0;
+ eq_cell->parameters["\\B_SIGNED"] = 0;
+ eq_cell->setPort("\\A", gold_masked);
+ eq_cell->setPort("\\B", gate_masked);
+ eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+ this_condition = eq_cell->getPort("\\Y");
+ }
+ else
+ {
+ RTLIL::Cell *eq_cell = miter_module->addCell(NEW_ID, "$eqx");
+ eq_cell->parameters["\\A_WIDTH"] = w2_gold->width;
+ eq_cell->parameters["\\B_WIDTH"] = w2_gate->width;
+ eq_cell->parameters["\\Y_WIDTH"] = 1;
+ eq_cell->parameters["\\A_SIGNED"] = 0;
+ eq_cell->parameters["\\B_SIGNED"] = 0;
+ eq_cell->setPort("\\A", w2_gold);
+ eq_cell->setPort("\\B", w2_gate);
+ eq_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+ this_condition = eq_cell->getPort("\\Y");
+ }
+
+ if (flag_make_outcmp)
+ {
+ RTLIL::Wire *w_cmp = miter_module->addWire("\\cmp_" + RTLIL::unescape_id(w1->name));
+ w_cmp->port_output = true;
+ miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
+ }
+
+ all_conditions.append(this_condition);
+ }
+ }
+
+ if (all_conditions.size() != 1) {
+ RTLIL::Cell *reduce_cell = miter_module->addCell(NEW_ID, "$reduce_and");
+ reduce_cell->parameters["\\A_WIDTH"] = all_conditions.size();
+ reduce_cell->parameters["\\Y_WIDTH"] = 1;
+ reduce_cell->parameters["\\A_SIGNED"] = 0;
+ reduce_cell->setPort("\\A", all_conditions);
+ reduce_cell->setPort("\\Y", miter_module->addWire(NEW_ID));
+ all_conditions = reduce_cell->getPort("\\Y");
+ }
+
+ if (flag_make_assert) {
+ RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, "$assert");
+ assert_cell->setPort("\\A", all_conditions);
+ assert_cell->setPort("\\EN", RTLIL::SigSpec(1, 1));
+ }
+
+ RTLIL::Wire *w_trigger = miter_module->addWire("\\trigger");
+ w_trigger->port_output = true;
+
+ RTLIL::Cell *not_cell = miter_module->addCell(NEW_ID, "$not");
+ not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
+ not_cell->parameters["\\A_WIDTH"] = all_conditions.size();
+ not_cell->parameters["\\Y_WIDTH"] = w_trigger->width;
+ not_cell->parameters["\\A_SIGNED"] = 0;
+ not_cell->setPort("\\A", all_conditions);
+ not_cell->setPort("\\Y", w_trigger);
+
+ miter_module->fixup_ports();
+
+ if (flag_flatten) {
+ log_push();
+ Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;");
+ log_pop();
+ }
+}
+
+void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design)
+{
+ bool flag_make_outputs = false;
+ bool flag_flatten = false;
+
+ log_header(design, "Executing MITER pass (creating miter circuit).\n");
+
+ size_t argidx;
+ for (argidx = 2; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-make_outputs") {
+ flag_make_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-flatten") {
+ flag_flatten = true;
+ continue;
+ }
+ break;
+ }
+ if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].substr(0, 1) == "-")
+ that->cmd_error(args, argidx, "command argument error");
+
+ IdString module_name = RTLIL::escape_id(args[argidx++]);
+ IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : "";
+
+ if (design->modules_.count(module_name) == 0)
+ log_cmd_error("Can't find module %s!\n", module_name.c_str());
+ if (!miter_name.empty() && design->modules_.count(miter_name) != 0)
+ log_cmd_error("There is already a module %s!\n", miter_name.c_str());
+
+ Module *module = design->module(module_name);
+
+ if (!miter_name.empty()) {
+ module = module->clone();
+ module->name = miter_name;
+ design->add(module);
+ }
+
+ if (!flag_make_outputs)
+ for (auto wire : module->wires())
+ wire->port_output = false;
+
+ Wire *trigger = module->addWire("\\trigger");
+ trigger->port_output = true;
+ module->fixup_ports();
+
+ if (flag_flatten) {
+ log_push();
+ Pass::call_on_module(design, module, "flatten;;");
+ log_pop();
+ }
+
+ SigSpec assert_signals, assume_signals;
+ vector<Cell*> cell_list = module->cells();
+ for (auto cell : cell_list)
+ {
+ if (!cell->type.in("$assert", "$assume"))
+ continue;
+
+ SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1);
+ SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1);
+
+ if (cell->type == "$assert") {
+ assert_signals.append(module->And(NEW_ID, is_active, is_enabled));
+ } else {
+ assume_signals.append(module->And(NEW_ID, is_active, is_enabled));
+ }
+
+ module->remove(cell);
+ }
+
+ if (assume_signals.empty())
+ {
+ module->addReduceOr(NEW_ID, assert_signals, trigger);
+ }
+ else
+ {
+ Wire *assume_q = module->addWire(NEW_ID);
+ assume_q->attributes["\\init"] = State::S0;
+ assume_signals.append(assume_q);
+
+ SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals);
+ SigSpec assume_ok = module->Not(NEW_ID, assume_nok);
+ module->addFf(NEW_ID, assume_nok, assume_q);
+
+ SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals);
+ module->addAnd(NEW_ID, assert_fail, assume_ok, trigger);
+ }
+
+ if (flag_flatten) {
+ log_push();
+ Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;");
+ log_pop();
+ }
+}
+
+struct MiterPass : public Pass {
+ MiterPass() : Pass("miter", "automatically create a miter circuit") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" miter -equiv [options] gold_name gate_name miter_name\n");
+ log("\n");
+ log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n");
+ log("must have the same interfaces. The miter circuit will have all inputs of the\n");
+ log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n");
+ log("output that goes high if an output mismatch between the two source modules is\n");
+ log("detected.\n");
+ log("\n");
+ log(" -ignore_gold_x\n");
+ log(" a undef (x) bit in the gold module output will match any value in\n");
+ log(" the gate module output.\n");
+ log("\n");
+ log(" -make_outputs\n");
+ log(" also route the gold- and gate-outputs to 'gold_*' and 'gate_*' outputs\n");
+ log(" on the miter circuit.\n");
+ log("\n");
+ log(" -make_outcmp\n");
+ log(" also create a cmp_* output for each gold/gate output pair.\n");
+ log("\n");
+ log(" -make_assert\n");
+ log(" also create an 'assert' cell that checks if trigger is always low.\n");
+ log("\n");
+ log(" -flatten\n");
+ log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+ log("\n");
+ log("\n");
+ log(" miter -assert [options] module [miter_name]\n");
+ log("\n");
+ log("Creates a miter circuit for property checking. All input ports are kept,\n");
+ log("output ports are discarded. An additional output 'trigger' is created that\n");
+ log("goes high when an assert is violated. Without a miter_name, the existing\n");
+ log("module is modified.\n");
+ log("\n");
+ log(" -make_outputs\n");
+ log(" keep module output ports.\n");
+ log("\n");
+ log(" -flatten\n");
+ log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ if (args.size() > 1 && args[1] == "-equiv") {
+ create_miter_equiv(this, args, design);
+ return;
+ }
+
+ if (args.size() > 1 && args[1] == "-assert") {
+ create_miter_assert(this, args, design);
+ return;
+ }
+
+ log_cmd_error("Missing mode parameter!\n");
+ }
+} MiterPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
new file mode 100644
index 00000000..a6ac7afd
--- /dev/null
+++ b/passes/sat/sat.cc
@@ -0,0 +1,1713 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * 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.
+ *
+ */
+
+// [[CITE]] Temporal Induction by Incremental SAT Solving
+// Niklas Een and Niklas Sörensson (2003)
+// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161
+
+#include "kernel/register.h"
+#include "kernel/celltypes.h"
+#include "kernel/consteval.h"
+#include "kernel/sigtools.h"
+#include "kernel/log.h"
+#include "kernel/satgen.h"
+#include <stdlib.h>
+#include <stdio.h>
+#include <algorithm>
+#include <errno.h>
+#include <string.h>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct SatHelper
+{
+ RTLIL::Design *design;
+ RTLIL::Module *module;
+
+ SigMap sigmap;
+ CellTypes ct;
+
+ ezSatPtr ez;
+ SatGen satgen;
+
+ // additional constraints
+ std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
+ std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
+ std::map<int, std::vector<std::string>> unsets_at;
+ bool prove_asserts, set_assumes;
+
+ // undef constraints
+ bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells;
+ std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
+
+ // model variables
+ std::vector<std::string> shows;
+ SigPool show_signal_pool;
+ SigSet<RTLIL::Cell*> show_drivers;
+ int max_timestep, timeout;
+ bool gotTimeout;
+
+ SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
+ design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
+ {
+ this->enable_undef = enable_undef;
+ satgen.model_undef = enable_undef;
+ set_init_def = false;
+ set_init_undef = false;
+ set_init_zero = false;
+ ignore_unknown_cells = false;
+ max_timestep = -1;
+ timeout = 0;
+ gotTimeout = false;
+ }
+
+ void check_undef_enabled(const RTLIL::SigSpec &sig)
+ {
+ if (enable_undef)
+ return;
+
+ std::vector<RTLIL::SigBit> sigbits = sig.to_sigbit_vector();
+ for (size_t i = 0; i < sigbits.size(); i++)
+ if (sigbits[i].wire == NULL && sigbits[i].data == RTLIL::State::Sx)
+ log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig));
+ }
+
+ void setup(int timestep = -1, bool initstate = false)
+ {
+ if (timestep > 0)
+ log ("\nSetting up time step %d:\n", timestep);
+ else
+ log ("\nSetting up SAT problem:\n");
+
+ if (initstate)
+ satgen.setInitState(timestep);
+
+ if (timestep > max_timestep)
+ max_timestep = timestep;
+
+ RTLIL::SigSpec big_lhs, big_rhs;
+
+ for (auto &s : sets)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
+ log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+
+ for (auto &s : sets_at[timestep])
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
+ log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+
+ for (auto &s : unsets_at[timestep])
+ {
+ RTLIL::SigSpec lhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s))
+ log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
+ show_signal_pool.add(sigmap(lhs));
+
+ log("Import unset-constraint for this timestep: %s\n", log_signal(lhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ }
+
+ log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+
+ // 0 = sets_def
+ // 1 = sets_any_undef
+ // 2 = sets_all_undef
+ std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+ for (auto &s : sets_def) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ }
+
+ for (auto &s : sets_any_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[1].insert(sig);
+ }
+
+ for (auto &s : sets_all_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (auto &s : sets_def_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_any_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].insert(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_all_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (int t = 0; t < 3; t++)
+ for (auto &sig : sets_def_undef[t]) {
+ log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+ std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+ if (t == 0)
+ ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_sig)));
+ if (t == 1)
+ ez->assume(ez->expression(ezSAT::OpOr, undef_sig));
+ if (t == 2)
+ ez->assume(ez->expression(ezSAT::OpAnd, undef_sig));
+ }
+
+ int import_cell_counter = 0;
+ for (auto cell : module->cells())
+ if (design->selected(module, cell)) {
+ // log("Import cell: %s\n", RTLIL::id2cstr(cell->name));
+ if (satgen.importCell(cell, timestep)) {
+ for (auto &p : cell->connections())
+ if (ct.cell_output(cell->type, p.first))
+ show_drivers.insert(sigmap(p.second), cell);
+ import_cell_counter++;
+ } else if (ignore_unknown_cells)
+ log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
+ else
+ log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
+ }
+ log("Imported %d cells to SAT database.\n", import_cell_counter);
+
+ if (set_assumes) {
+ RTLIL::SigSpec assumes_a, assumes_en;
+ satgen.getAssumes(assumes_a, assumes_en, timestep);
+ for (int i = 0; i < GetSize(assumes_a); i++)
+ log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
+ ez->assume(satgen.importAssumes(timestep));
+ }
+
+ if (initstate)
+ {
+ RTLIL::SigSpec big_lhs, big_rhs;
+
+ for (auto &it : module->wires_)
+ {
+ if (it.second->attributes.count("\\init") == 0)
+ continue;
+
+ RTLIL::SigSpec lhs = sigmap(it.second);
+ RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
+ log_assert(lhs.size() == rhs.size());
+
+ RTLIL::SigSpec removed_bits;
+ for (int i = 0; i < lhs.size(); i++) {
+ RTLIL::SigSpec bit = lhs.extract(i, 1);
+ if (!satgen.initial_state.check_all(bit)) {
+ removed_bits.append(bit);
+ lhs.remove(i, 1);
+ rhs.remove(i, 1);
+ i--;
+ }
+ }
+
+ if (removed_bits.size())
+ log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits));
+
+ if (lhs.size()) {
+ log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+ }
+
+ for (auto &s : sets_init)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
+ log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import init set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+
+ if (!satgen.initial_state.check_all(big_lhs)) {
+ RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs);
+ log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
+ }
+
+ if (set_init_def) {
+ RTLIL::SigSpec rem = satgen.initial_state.export_all();
+ std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
+ ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem)));
+ }
+
+ if (set_init_undef) {
+ RTLIL::SigSpec rem = satgen.initial_state.export_all();
+ rem.remove(big_lhs);
+ big_lhs.append(rem);
+ big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
+ }
+
+ if (set_init_zero) {
+ RTLIL::SigSpec rem = satgen.initial_state.export_all();
+ rem.remove(big_lhs);
+ big_lhs.append(rem);
+ big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
+ }
+
+ if (big_lhs.size() == 0) {
+ log("No constraints for initial state found.\n\n");
+ return;
+ }
+
+ log("Final init constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ }
+ }
+
+ int setup_proof(int timestep = -1)
+ {
+ log_assert(prove.size() || prove_x.size() || prove_asserts);
+
+ RTLIL::SigSpec big_lhs, big_rhs;
+ std::vector<int> prove_bits;
+
+ if (prove.size() > 0)
+ {
+ for (auto &s : prove)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
+ log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+
+ log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ }
+
+ if (prove_x.size() > 0)
+ {
+ for (auto &s : prove_x)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
+ log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.size() != rhs.size())
+ log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
+
+ log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
+
+ log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+
+ std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
+ std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
+
+ std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
+ std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
+
+ for (size_t i = 0; i < value_lhs.size(); i++)
+ prove_bits.push_back(ez->OR(undef_lhs.at(i), ez->AND(ez->NOT(undef_rhs.at(i)), ez->NOT(ez->XOR(value_lhs.at(i), value_rhs.at(i))))));
+ }
+
+ if (prove_asserts) {
+ RTLIL::SigSpec asserts_a, asserts_en;
+ satgen.getAsserts(asserts_a, asserts_en, timestep);
+ for (int i = 0; i < GetSize(asserts_a); i++)
+ log("Import proof for assert: %s when %s.\n", log_signal(asserts_a[i]), log_signal(asserts_en[i]));
+ prove_bits.push_back(satgen.importAsserts(timestep));
+ }
+
+ return ez->expression(ezSAT::OpAnd, prove_bits);
+ }
+
+ void force_unique_state(int timestep_from, int timestep_to)
+ {
+ RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
+ for (int i = timestep_from; i < timestep_to; i++)
+ ez->assume(ez->NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
+ }
+
+ bool solve(const std::vector<int> &assumptions)
+ {
+ log_assert(gotTimeout == false);
+ ez->setSolverTimeout(timeout);
+ bool success = ez->solve(modelExpressions, modelValues, assumptions);
+ if (ez->getSolverTimoutStatus())
+ gotTimeout = true;
+ return success;
+ }
+
+ bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
+ {
+ log_assert(gotTimeout == false);
+ ez->setSolverTimeout(timeout);
+ bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
+ if (ez->getSolverTimoutStatus())
+ gotTimeout = true;
+ return success;
+ }
+
+ struct ModelBlockInfo {
+ int timestep, offset, width;
+ std::string description;
+ bool operator < (const ModelBlockInfo &other) const {
+ if (timestep != other.timestep)
+ return timestep < other.timestep;
+ if (description != other.description)
+ return description < other.description;
+ if (offset != other.offset)
+ return offset < other.offset;
+ if (width != other.width)
+ return width < other.width;
+ return false;
+ }
+ };
+
+ std::vector<int> modelExpressions;
+ std::vector<bool> modelValues;
+ std::set<ModelBlockInfo> modelInfo;
+
+ void maximize_undefs()
+ {
+ log_assert(enable_undef);
+ std::vector<bool> backupValues;
+
+ while (1)
+ {
+ std::vector<int> must_undef, maybe_undef;
+
+ for (size_t i = 0; i < modelExpressions.size()/2; i++)
+ if (modelValues.at(modelExpressions.size()/2 + i))
+ must_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
+ else
+ maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
+
+ backupValues.swap(modelValues);
+ if (!solve(ez->expression(ezSAT::OpAnd, must_undef), ez->expression(ezSAT::OpOr, maybe_undef)))
+ break;
+ }
+
+ backupValues.swap(modelValues);
+ }
+
+ void generate_model()
+ {
+ RTLIL::SigSpec modelSig;
+ modelExpressions.clear();
+ modelInfo.clear();
+
+ // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
+
+ if (shows.size() == 0)
+ {
+ SigPool queued_signals, handled_signals, final_signals;
+ queued_signals = show_signal_pool;
+ while (queued_signals.size() > 0) {
+ RTLIL::SigSpec sig = queued_signals.export_one();
+ queued_signals.del(sig);
+ handled_signals.add(sig);
+ std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
+ if (drivers.size() == 0) {
+ final_signals.add(sig);
+ } else {
+ for (auto &d : drivers)
+ for (auto &p : d->connections()) {
+ if (d->type == "$dff" && p.first == "\\CLK")
+ continue;
+ if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
+ continue;
+ queued_signals.add(handled_signals.remove(sigmap(p.second)));
+ }
+ }
+ }
+ modelSig = final_signals.export_all();
+
+ // additionally add all set and prove signals directly
+ // (it improves user confidence if we write the constraints back ;-)
+ modelSig.append(show_signal_pool.export_all());
+ }
+ else
+ {
+ for (auto &s : shows) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
+ log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
+ log("Import show expression: %s\n", log_signal(sig));
+ modelSig.append(sig);
+ }
+ }
+
+ modelSig.sort_and_unify();
+ // log("Model signals: %s\n", log_signal(modelSig));
+
+ std::vector<int> modelUndefExpressions;
+
+ for (auto &c : modelSig.chunks())
+ if (c.wire != NULL)
+ {
+ ModelBlockInfo info;
+ RTLIL::SigSpec chunksig = c;
+ info.width = chunksig.size();
+ info.description = log_signal(chunksig);
+
+ for (int timestep = -1; timestep <= max_timestep; timestep++)
+ {
+ if ((timestep == -1 && max_timestep > 0) || timestep == 0)
+ continue;
+
+ info.timestep = timestep;
+ info.offset = modelExpressions.size();
+ modelInfo.insert(info);
+
+ std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
+ modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
+
+ if (enable_undef) {
+ std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, timestep);
+ modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
+ }
+ }
+ }
+
+ // Add initial state signals as collected by satgen
+ //
+ modelSig = satgen.initial_state.export_all();
+ for (auto &c : modelSig.chunks())
+ if (c.wire != NULL)
+ {
+ ModelBlockInfo info;
+ RTLIL::SigSpec chunksig = c;
+
+ info.timestep = 0;
+ info.offset = modelExpressions.size();
+ info.width = chunksig.size();
+ info.description = log_signal(chunksig);
+ modelInfo.insert(info);
+
+ std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
+ modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
+
+ if (enable_undef) {
+ std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, 1);
+ modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
+ }
+ }
+
+ modelExpressions.insert(modelExpressions.end(), modelUndefExpressions.begin(), modelUndefExpressions.end());
+ }
+
+ void print_model()
+ {
+ int maxModelName = 10;
+ int maxModelWidth = 10;
+
+ for (auto &info : modelInfo) {
+ maxModelName = max(maxModelName, int(info.description.size()));
+ maxModelWidth = max(maxModelWidth, info.width);
+ }
+
+ log("\n");
+
+ int last_timestep = -2;
+ for (auto &info : modelInfo)
+ {
+ RTLIL::Const value;
+ bool found_undef = false;
+
+ for (int i = 0; i < info.width; i++) {
+ value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+ if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+ value.bits.back() = RTLIL::State::Sx, found_undef = true;
+ }
+
+ if (info.timestep != last_timestep) {
+ const char *hline = "---------------------------------------------------------------------------------------------------"
+ "---------------------------------------------------------------------------------------------------"
+ "---------------------------------------------------------------------------------------------------";
+ if (last_timestep == -2) {
+ log(max_timestep > 0 ? " Time " : " ");
+ log("%-*s %11s %9s %*s\n", maxModelName+5, "Signal Name", "Dec", "Hex", maxModelWidth+3, "Bin");
+ }
+ log(max_timestep > 0 ? " ---- " : " ");
+ log("%*.*s %11.11s %9.9s %*.*s\n", maxModelName+5, maxModelName+5,
+ hline, hline, hline, maxModelWidth+3, maxModelWidth+3, hline);
+ last_timestep = info.timestep;
+ }
+
+ if (max_timestep > 0) {
+ if (info.timestep > 0)
+ log(" %4d ", info.timestep);
+ else
+ log(" init ");
+ } else
+ log(" ");
+
+ if (info.width <= 32 && !found_undef)
+ log("%-*s %11d %9x %*s\n", maxModelName+5, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+3, value.as_string().c_str());
+ else
+ log("%-*s %11s %9s %*s\n", maxModelName+5, info.description.c_str(), "--", "--", maxModelWidth+3, value.as_string().c_str());
+ }
+
+ if (last_timestep == -2)
+ log(" no model variables selected for display.\n");
+ }
+
+ void dump_model_to_vcd(std::string vcd_file_name)
+ {
+ FILE *f = fopen(vcd_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
+
+ log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
+
+ time_t timestamp;
+ struct tm* now;
+ char stime[128] = {};
+ time(&timestamp);
+ now = localtime(&timestamp);
+ strftime(stime, sizeof(stime), "%c", now);
+
+ std::string module_fname = "unknown";
+ auto apos = module->attributes.find("\\src");
+ if(apos != module->attributes.end())
+ module_fname = module->attributes["\\src"].decode_string();
+
+ fprintf(f, "$date\n");
+ fprintf(f, " %s\n", stime);
+ fprintf(f, "$end\n");
+ fprintf(f, "$version\n");
+ fprintf(f, " Generated by %s\n", yosys_version_str);
+ fprintf(f, "$end\n");
+ fprintf(f, "$comment\n");
+ fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n",
+ module->name.c_str(), module_fname.c_str());
+ fprintf(f, "$end\n");
+
+ // VCD has some limits on internal (non-display) identifier names, so make legal ones
+ std::map<std::string, std::string> vcdnames;
+
+ fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
+ fprintf(f, "$scope module %s $end\n", module->name.c_str());
+ for (auto &info : modelInfo)
+ {
+ if (vcdnames.find(info.description) != vcdnames.end())
+ continue;
+
+ char namebuf[16];
+ snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
+ vcdnames[info.description] = namebuf;
+
+ // Even display identifiers can't use some special characters
+ std::string legal_desc = info.description.c_str();
+ for (auto &c : legal_desc) {
+ if(c == '$')
+ c = '_';
+ if(c == ':')
+ c = '_';
+ }
+
+ fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
+
+ // Need to look at first *two* cycles!
+ // We need to put a name on all variables but those without an initialization clause
+ // have no value at timestep 0
+ if(info.timestep > 1)
+ break;
+ }
+ fprintf(f, "$upscope $end\n");
+ fprintf(f, "$enddefinitions $end\n");
+ fprintf(f, "$dumpvars\n");
+
+ static const char bitvals[] = "01xzxx";
+
+ int last_timestep = -2;
+ for (auto &info : modelInfo)
+ {
+ RTLIL::Const value;
+
+ for (int i = 0; i < info.width; i++) {
+ value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+ if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+ value.bits.back() = RTLIL::State::Sx;
+ }
+
+ if (info.timestep != last_timestep) {
+ if(last_timestep == 0)
+ fprintf(f, "$end\n");
+ else
+ fprintf(f, "#%d\n", info.timestep);
+ last_timestep = info.timestep;
+ }
+
+ if(info.width == 1) {
+ fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
+ } else {
+ fprintf(f, "b");
+ for(int k=info.width-1; k >= 0; k --) //need to flip bit ordering for VCD
+ fprintf(f, "%c", bitvals[value.bits[k]]);
+ fprintf(f, " %s\n", vcdnames[info.description].c_str());
+ }
+ }
+
+ if (last_timestep == -2)
+ log(" no model variables selected for display.\n");
+
+ fclose(f);
+ }
+
+ void dump_model_to_json(std::string json_file_name)
+ {
+ FILE *f = fopen(json_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
+
+ log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str());
+
+ int mintime = 1, maxtime = 0, maxwidth = 0;;
+ dict<string, pair<int, dict<int, Const>>> wavedata;
+
+ for (auto &info : modelInfo)
+ {
+ Const value;
+ for (int i = 0; i < info.width; i++) {
+ value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
+ if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
+ value.bits.back() = RTLIL::State::Sx;
+ }
+
+ wavedata[info.description].first = info.width;
+ wavedata[info.description].second[info.timestep] = value;
+ mintime = min(mintime, info.timestep);
+ maxtime = max(maxtime, info.timestep);
+ maxwidth = max(maxwidth, info.width);
+ }
+
+ fprintf(f, "{ \"signal\": [");
+ bool fist_wavedata = true;
+ for (auto &wd : wavedata)
+ {
+ fprintf(f, "%s", fist_wavedata ? "\n" : ",\n");
+ fist_wavedata = false;
+
+ vector<string> data;
+ string name = wd.first.c_str();
+ while (name.substr(0, 1) == "\\")
+ name = name.substr(1);
+
+ fprintf(f, " { \"name\": \"%s\", \"wave\": \"", name.c_str());
+ for (int i = mintime; i <= maxtime; i++) {
+ if (wd.second.second.count(i)) {
+ string this_data = wd.second.second[i].as_string();
+ char ch = '=';
+ if (wd.second.first == 1)
+ ch = this_data[0];
+ if (!data.empty() && data.back() == this_data) {
+ fprintf(f, ".");
+ } else {
+ data.push_back(this_data);
+ fprintf(f, "%c", ch);
+ }
+ } else {
+ data.push_back("");
+ fprintf(f, "4");
+ }
+ }
+ if (wd.second.first != 1) {
+ fprintf(f, "\", \"data\": [");
+ for (int i = 0; i < GetSize(data); i++)
+ fprintf(f, "%s\"%s\"", i ? ", " : "", data[i].c_str());
+ fprintf(f, "] }");
+ } else {
+ fprintf(f, "\" }");
+ }
+ }
+ fprintf(f, "\n ],\n");
+ fprintf(f, " \"config\": {\n");
+ fprintf(f, " \"hscale\": %.2f\n", maxwidth / 4.0);
+ fprintf(f, " }\n");
+ fprintf(f, "}\n");
+ fclose(f);
+ }
+
+ void invalidate_model(bool max_undef)
+ {
+ std::vector<int> clause;
+ if (enable_undef) {
+ for (size_t i = 0; i < modelExpressions.size()/2; i++) {
+ int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i);
+ bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i);
+ if (!max_undef || !val_undef)
+ clause.push_back(val_undef ? ez->NOT(bit_undef) : val ? ez->NOT(bit) : bit);
+ }
+ } else
+ for (size_t i = 0; i < modelExpressions.size(); i++)
+ clause.push_back(modelValues.at(i) ? ez->NOT(modelExpressions.at(i)) : modelExpressions.at(i));
+ ez->assume(ez->expression(ezSAT::OpOr, clause));
+ }
+};
+
+void print_proof_failed()
+{
+ log("\n");
+ log(" ______ ___ ___ _ _ _ _ \n");
+ log(" (_____ \\ / __) / __) (_) | | | |\n");
+ log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
+ log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
+ log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
+ log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
+ log("\n");
+}
+
+void print_timeout()
+{
+ log("\n");
+ log(" _____ _ _ _____ ____ _ _____\n");
+ log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n");
+ log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n");
+ log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n");
+ log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n");
+ log("\n");
+}
+
+void print_qed()
+{
+ log("\n");
+ log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
+ log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
+ log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
+ log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
+ log(" | $$ | $$ | $$__/ | $$ | $$ \n");
+ log(" | $$/$$ $$ | $$ | $$ | $$ \n");
+ log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
+ log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
+ log(" \\__/ \n");
+ log("\n");
+}
+
+struct SatPass : public Pass {
+ SatPass() : Pass("sat", "solve a SAT problem in the circuit") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" sat [options] [selection]\n");
+ log("\n");
+ log("This command solves a SAT problem defined over the currently selected circuit\n");
+ log("and additional constraints passed as parameters.\n");
+ log("\n");
+ log(" -all\n");
+ log(" show all solutions to the problem (this can grow exponentially, use\n");
+ log(" -max <N> instead to get <N> solutions)\n");
+ log("\n");
+ log(" -max <N>\n");
+ log(" like -all, but limit number of solutions to <N>\n");
+ log("\n");
+ log(" -enable_undef\n");
+ log(" enable modeling of undef value (aka 'x-bits')\n");
+ log(" this option is implied by -set-def, -set-undef et. cetera\n");
+ log("\n");
+ log(" -max_undef\n");
+ log(" maximize the number of undef bits in solutions, giving a better\n");
+ log(" picture of which input bits are actually vital to the solution.\n");
+ log("\n");
+ log(" -set <signal> <value>\n");
+ log(" set the specified signal to the specified value.\n");
+ log("\n");
+ log(" -set-def <signal>\n");
+ log(" add a constraint that all bits of the given signal must be defined\n");
+ log("\n");
+ log(" -set-any-undef <signal>\n");
+ log(" add a constraint that at least one bit of the given signal is undefined\n");
+ log("\n");
+ log(" -set-all-undef <signal>\n");
+ log(" add a constraint that all bits of the given signal are undefined\n");
+ log("\n");
+ log(" -set-def-inputs\n");
+ log(" add -set-def constraints for all module inputs\n");
+ log("\n");
+ log(" -show <signal>\n");
+ log(" show the model for the specified signal. if no -show option is\n");
+ log(" passed then a set of signals to be shown is automatically selected.\n");
+ log("\n");
+ log(" -show-inputs, -show-outputs, -show-ports\n");
+ log(" add all module (input/output) ports to the list of shown signals\n");
+ log("\n");
+ log(" -show-regs, -show-public, -show-all\n");
+ log(" show all registers, show signals with 'public' names, show all signals\n");
+ log("\n");
+ log(" -ignore_div_by_zero\n");
+ log(" ignore all solutions that involve a division by zero\n");
+ log("\n");
+ log(" -ignore_unknown_cells\n");
+ log(" ignore all cells that can not be matched to a SAT model\n");
+ log("\n");
+ log("The following options can be used to set up a sequential problem:\n");
+ log("\n");
+ log(" -seq <N>\n");
+ log(" set up a sequential problem with <N> time steps. The steps will\n");
+ log(" be numbered from 1 to N.\n");
+ log("\n");
+ log(" note: for large <N> it can be significantly faster to use\n");
+ log(" -tempinduct-baseonly -maxsteps <N> instead of -seq <N>.\n");
+ log("\n");
+ log(" -set-at <N> <signal> <value>\n");
+ log(" -unset-at <N> <signal>\n");
+ log(" set or unset the specified signal to the specified value in the\n");
+ log(" given timestep. this has priority over a -set for the same signal.\n");
+ log("\n");
+ log(" -set-assumes\n");
+ log(" set all assumptions provided via $assume cells\n");
+ log("\n");
+ log(" -set-def-at <N> <signal>\n");
+ log(" -set-any-undef-at <N> <signal>\n");
+ log(" -set-all-undef-at <N> <signal>\n");
+ log(" add undef constraints in the given timestep.\n");
+ log("\n");
+ log(" -set-init <signal> <value>\n");
+ log(" set the initial value for the register driving the signal to the value\n");
+ log("\n");
+ log(" -set-init-undef\n");
+ log(" set all initial states (not set using -set-init) to undef\n");
+ log("\n");
+ log(" -set-init-def\n");
+ log(" do not force a value for the initial state but do not allow undef\n");
+ log("\n");
+ log(" -set-init-zero\n");
+ log(" set all initial states (not set using -set-init) to zero\n");
+ log("\n");
+ log(" -dump_vcd <vcd-file-name>\n");
+ log(" dump SAT model (counter example in proof) to VCD file\n");
+ log("\n");
+ log(" -dump_json <json-file-name>\n");
+ log(" dump SAT model (counter example in proof) to a WaveJSON file.\n");
+ log("\n");
+ log(" -dump_cnf <cnf-file-name>\n");
+ log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
+ log(" proofs this is the CNF of the first induction step.\n");
+ log("\n");
+ log("The following additional options can be used to set up a proof. If also -seq\n");
+ log("is passed, a temporal induction proof is performed.\n");
+ log("\n");
+ log(" -tempinduct\n");
+ log(" Perform a temporal induction proof. In a temporal induction proof it is\n");
+ log(" proven that the condition holds forever after the number of time steps\n");
+ log(" specified using -seq.\n");
+ log("\n");
+ log(" -tempinduct-def\n");
+ log(" Perform a temporal induction proof. Assume an initial state with all\n");
+ log(" registers set to defined values for the induction step.\n");
+ log("\n");
+ log(" -tempinduct-baseonly\n");
+ log(" Run only the basecase half of temporal induction (requires -maxsteps)\n");
+ log("\n");
+ log(" -tempinduct-inductonly\n");
+ log(" Run only the induction half of temporal induction\n");
+ log("\n");
+ log(" -tempinduct-skip <N>\n");
+ log(" Skip the first <N> steps of the induction proof.\n");
+ log("\n");
+ log(" note: this will assume that the base case holds for <N> steps.\n");
+ log(" this must be proven independently with \"-tempinduct-baseonly\n");
+ log(" -maxsteps <N>\". Use -initsteps if you just want to set a\n");
+ log(" minimal induction length.\n");
+ log("\n");
+ log(" -prove <signal> <value>\n");
+ log(" Attempt to proof that <signal> is always <value>.\n");
+ log("\n");
+ log(" -prove-x <signal> <value>\n");
+ log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
+ log(" the right hand side. Useful for equivalence checking.\n");
+ log("\n");
+ log(" -prove-asserts\n");
+ log(" Prove that all asserts in the design hold.\n");
+ log("\n");
+ log(" -prove-skip <N>\n");
+ log(" Do not enforce the prove-condition for the first <N> time steps.\n");
+ log("\n");
+ log(" -maxsteps <N>\n");
+ log(" Set a maximum length for the induction.\n");
+ log("\n");
+ log(" -initsteps <N>\n");
+ log(" Set initial length for the induction.\n");
+ log(" This will speed up the search of the right induction length\n");
+ log(" for deep induction proofs.\n");
+ log("\n");
+ log(" -stepsize <N>\n");
+ log(" Increase the size of the induction proof in steps of <N>.\n");
+ log(" This will speed up the search of the right induction length\n");
+ log(" for deep induction proofs.\n");
+ log("\n");
+ log(" -timeout <N>\n");
+ log(" Maximum number of seconds a single SAT instance may take.\n");
+ log("\n");
+ log(" -verify\n");
+ log(" Return an error and stop the synthesis script if the proof fails.\n");
+ log("\n");
+ log(" -verify-no-timeout\n");
+ log(" Like -verify but do not return an error for timeouts.\n");
+ log("\n");
+ log(" -falsify\n");
+ log(" Return an error and stop the synthesis script if the proof succeeds.\n");
+ log("\n");
+ log(" -falsify-no-timeout\n");
+ log(" Like -falsify but do not return an error for timeouts.\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
+ std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
+ std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
+ std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
+ int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
+ bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
+ bool show_regs = false, show_public = false, show_all = false;
+ bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
+ bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false;
+ int tempinduct_skip = 0, stepsize = 1;
+ std::string vcd_file_name, json_file_name, cnf_file_name;
+
+ log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-all") {
+ loopcount = -1;
+ continue;
+ }
+ if (args[argidx] == "-verify") {
+ fail_on_timeout = true;
+ verify = true;
+ continue;
+ }
+ if (args[argidx] == "-verify-no-timeout") {
+ verify = true;
+ continue;
+ }
+ if (args[argidx] == "-falsify") {
+ fail_on_timeout = true;
+ falsify = true;
+ continue;
+ }
+ if (args[argidx] == "-falsify-no-timeout") {
+ falsify = true;
+ continue;
+ }
+ if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
+ timeout = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-max" && argidx+1 < args.size()) {
+ loopcount = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
+ maxsteps = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
+ initsteps = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-stepsize" && argidx+1 < args.size()) {
+ stepsize = max(1, atoi(args[++argidx].c_str()));
+ continue;
+ }
+ if (args[argidx] == "-ignore_div_by_zero") {
+ ignore_div_by_zero = true;
+ continue;
+ }
+ if (args[argidx] == "-enable_undef") {
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-max_undef") {
+ enable_undef = true;
+ max_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-def-inputs") {
+ enable_undef = true;
+ set_def_inputs = true;
+ continue;
+ }
+ if (args[argidx] == "-set" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ continue;
+ }
+ if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
+ sets_def.push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
+ sets_any_undef.push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
+ sets_all_undef.push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-assumes") {
+ set_assumes = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct") {
+ tempinduct = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-def") {
+ tempinduct = true;
+ tempinduct_def = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-baseonly") {
+ tempinduct = true;
+ tempinduct_baseonly = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-inductonly") {
+ tempinduct = true;
+ tempinduct_inductonly = true;
+ continue;
+ }
+ if (args[argidx] == "-tempinduct-skip" && argidx+1 < args.size()) {
+ tempinduct_skip = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-prove" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ continue;
+ }
+ if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-prove-asserts") {
+ prove_asserts = true;
+ continue;
+ }
+ if (args[argidx] == "-prove-skip" && argidx+1 < args.size()) {
+ prove_skip = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-seq" && argidx+1 < args.size()) {
+ seq_len = atoi(args[++argidx].c_str());
+ continue;
+ }
+ if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
+ int timestep = atoi(args[++argidx].c_str());
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
+ continue;
+ }
+ if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
+ int timestep = atoi(args[++argidx].c_str());
+ unsets_at[timestep].push_back(args[++argidx]);
+ continue;
+ }
+ if (args[argidx] == "-set-def-at" && argidx+2 < args.size()) {
+ int timestep = atoi(args[++argidx].c_str());
+ sets_def_at[timestep].push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
+ int timestep = atoi(args[++argidx].c_str());
+ sets_any_undef_at[timestep].push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-all-undef-at" && argidx+2 < args.size()) {
+ int timestep = atoi(args[++argidx].c_str());
+ sets_all_undef_at[timestep].push_back(args[++argidx]);
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-init" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ sets_init.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ continue;
+ }
+ if (args[argidx] == "-set-init-undef") {
+ set_init_undef = true;
+ enable_undef = true;
+ continue;
+ }
+ if (args[argidx] == "-set-init-def") {
+ set_init_def = true;
+ continue;
+ }
+ if (args[argidx] == "-set-init-zero") {
+ set_init_zero = true;
+ continue;
+ }
+ if (args[argidx] == "-show" && argidx+1 < args.size()) {
+ shows.push_back(args[++argidx]);
+ continue;
+ }
+ if (args[argidx] == "-show-inputs") {
+ show_inputs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-outputs") {
+ show_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-ports") {
+ show_inputs = true;
+ show_outputs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-regs") {
+ show_regs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-public") {
+ show_public = true;
+ continue;
+ }
+ if (args[argidx] == "-show-all") {
+ show_all = true;
+ continue;
+ }
+ if (args[argidx] == "-ignore_unknown_cells") {
+ ignore_unknown_cells = true;
+ continue;
+ }
+ if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
+ vcd_file_name = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-dump_json" && argidx+1 < args.size()) {
+ json_file_name = args[++argidx];
+ continue;
+ }
+ if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
+ cnf_file_name = args[++argidx];
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ RTLIL::Module *module = NULL;
+ for (auto mod : design->selected_modules()) {
+ if (module)
+ log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod));
+ module = mod;
+ }
+ if (module == NULL)
+ log_cmd_error("Can't perform SAT on an empty selection!\n");
+
+ if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
+ log_cmd_error("Got -tempinduct but nothing to prove!\n");
+
+ if (prove_skip && tempinduct)
+ log_cmd_error("Options -prove-skip and -tempinduct don't work with each other. Use -seq instead of -prove-skip.\n");
+
+ if (prove_skip >= seq_len && prove_skip > 0)
+ log_cmd_error("The value of -prove-skip must be smaller than the one of -seq.\n");
+
+ if (set_init_undef + set_init_zero + set_init_def > 1)
+ log_cmd_error("The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!\n");
+
+ if (set_def_inputs) {
+ for (auto &it : module->wires_)
+ if (it.second->port_input)
+ sets_def.push_back(it.second->name.str());
+ }
+
+ if (show_inputs) {
+ for (auto &it : module->wires_)
+ if (it.second->port_input)
+ shows.push_back(it.second->name.str());
+ }
+
+ if (show_outputs) {
+ for (auto &it : module->wires_)
+ if (it.second->port_output)
+ shows.push_back(it.second->name.str());
+ }
+
+ if (show_regs) {
+ pool<Wire*> reg_wires;
+ for (auto cell : module->cells()) {
+ if (cell->type == "$dff" || cell->type.substr(0, 6) == "$_DFF_")
+ for (auto bit : cell->getPort("\\Q"))
+ if (bit.wire)
+ reg_wires.insert(bit.wire);
+ }
+ for (auto wire : reg_wires)
+ shows.push_back(wire->name.str());
+ }
+
+ if (show_public) {
+ for (auto wire : module->wires())
+ if (wire->name[0] == '\\')
+ shows.push_back(wire->name.str());
+ }
+
+ if (show_all) {
+ for (auto wire : module->wires())
+ shows.push_back(wire->name.str());
+ }
+
+ if (tempinduct)
+ {
+ if (loopcount > 0 || max_undef)
+ log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
+
+ SatHelper basecase(design, module, enable_undef);
+ SatHelper inductstep(design, module, enable_undef);
+
+ basecase.sets = sets;
+ basecase.set_assumes = set_assumes;
+ basecase.prove = prove;
+ basecase.prove_x = prove_x;
+ basecase.prove_asserts = prove_asserts;
+ basecase.sets_at = sets_at;
+ basecase.unsets_at = unsets_at;
+ basecase.shows = shows;
+ basecase.timeout = timeout;
+ basecase.sets_def = sets_def;
+ basecase.sets_any_undef = sets_any_undef;
+ basecase.sets_all_undef = sets_all_undef;
+ basecase.sets_def_at = sets_def_at;
+ basecase.sets_any_undef_at = sets_any_undef_at;
+ basecase.sets_all_undef_at = sets_all_undef_at;
+ basecase.sets_init = sets_init;
+ basecase.set_init_def = set_init_def;
+ basecase.set_init_undef = set_init_undef;
+ basecase.set_init_zero = set_init_zero;
+ basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
+ basecase.ignore_unknown_cells = ignore_unknown_cells;
+
+ for (int timestep = 1; timestep <= seq_len; timestep++)
+ if (!tempinduct_inductonly)
+ basecase.setup(timestep, timestep == 1);
+
+ inductstep.sets = sets;
+ inductstep.set_assumes = set_assumes;
+ inductstep.prove = prove;
+ inductstep.prove_x = prove_x;
+ inductstep.prove_asserts = prove_asserts;
+ inductstep.shows = shows;
+ inductstep.timeout = timeout;
+ inductstep.sets_def = sets_def;
+ inductstep.sets_any_undef = sets_any_undef;
+ inductstep.sets_all_undef = sets_all_undef;
+ inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
+ inductstep.ignore_unknown_cells = ignore_unknown_cells;
+
+ if (!tempinduct_baseonly) {
+ inductstep.setup(1);
+ inductstep.ez->assume(inductstep.setup_proof(1));
+ }
+
+ if (tempinduct_def) {
+ std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
+ inductstep.ez->assume(inductstep.ez->NOT(inductstep.ez->expression(ezSAT::OpOr, undef_state)));
+ }
+
+ for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
+ {
+ log("\n** Trying induction with length %d **\n", inductlen);
+
+ // phase 1: proving base case
+
+ if (!tempinduct_inductonly)
+ {
+ basecase.setup(seq_len + inductlen, seq_len + inductlen == 1);
+ int property = basecase.setup_proof(seq_len + inductlen);
+ basecase.generate_model();
+
+ if (inductlen > 1)
+ basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
+
+ if (tempinduct_skip < inductlen)
+ {
+ log("\n[base case %d] Solving problem with %d variables and %d clauses..\n",
+ inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+ log_flush();
+
+ if (basecase.solve(basecase.ez->NOT(property))) {
+ log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
+ print_proof_failed();
+ basecase.print_model();
+ if(!vcd_file_name.empty())
+ basecase.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ basecase.dump_model_to_json(json_file_name);
+ goto tip_failed;
+ }
+
+ if (basecase.gotTimeout)
+ goto timeout;
+
+ log("Base case for induction length %d proven.\n", inductlen);
+ }
+ else
+ {
+ log("\n[base case %d] Skipping prove for this step (-tempinduct-skip %d).",
+ inductlen, tempinduct_skip);
+ log("\n[base case %d] Problem size so far: %d variables and %d clauses.\n",
+ inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses());
+ }
+ basecase.ez->assume(property);
+ }
+
+ // phase 2: proving induction step
+
+ if (!tempinduct_baseonly)
+ {
+ inductstep.setup(inductlen + 1);
+ int property = inductstep.setup_proof(inductlen + 1);
+ inductstep.generate_model();
+
+ if (inductlen > 1)
+ inductstep.force_unique_state(1, inductlen + 1);
+
+ if (inductlen <= tempinduct_skip || inductlen <= initsteps || inductlen % stepsize != 0)
+ {
+ if (inductlen < tempinduct_skip)
+ log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).",
+ inductlen, tempinduct_skip);
+ if (inductlen < initsteps)
+ log("\n[induction step %d] Skipping prove for this step (-initsteps %d).",
+ inductlen, tempinduct_skip);
+ if (inductlen % stepsize != 0)
+ log("\n[induction step %d] Skipping prove for this step (-stepsize %d).",
+ inductlen, stepsize);
+ log("\n[induction step %d] Problem size so far: %d variables and %d clauses.\n",
+ inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+ inductstep.ez->assume(property);
+ }
+ else
+ {
+ if (!cnf_file_name.empty())
+ {
+ FILE *f = fopen(cnf_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
+
+ log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ inductstep.ez->printDIMACS(f, false);
+ fclose(f);
+ }
+
+ log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n",
+ inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
+ log_flush();
+
+ if (!inductstep.solve(inductstep.ez->NOT(property))) {
+ if (inductstep.gotTimeout)
+ goto timeout;
+ log("Induction step proven: SUCCESS!\n");
+ print_qed();
+ goto tip_success;
+ }
+
+ log("Induction step failed. Incrementing induction length.\n");
+ inductstep.ez->assume(property);
+ inductstep.print_model();
+ }
+ }
+ }
+
+ if (tempinduct_baseonly) {
+ log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps);
+ goto tip_success;
+ }
+
+ log("\nReached maximum number of time steps -> proof failed.\n");
+ if(!vcd_file_name.empty())
+ inductstep.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ inductstep.dump_model_to_json(json_file_name);
+ print_proof_failed();
+
+ tip_failed:
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
+
+ if (0)
+ tip_success:
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and proof did succeed!\n");
+ }
+ }
+ else
+ {
+ if (maxsteps > 0)
+ log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
+
+ SatHelper sathelper(design, module, enable_undef);
+
+ sathelper.sets = sets;
+ sathelper.set_assumes = set_assumes;
+ sathelper.prove = prove;
+ sathelper.prove_x = prove_x;
+ sathelper.prove_asserts = prove_asserts;
+ sathelper.sets_at = sets_at;
+ sathelper.unsets_at = unsets_at;
+ sathelper.shows = shows;
+ sathelper.timeout = timeout;
+ sathelper.sets_def = sets_def;
+ sathelper.sets_any_undef = sets_any_undef;
+ sathelper.sets_all_undef = sets_all_undef;
+ sathelper.sets_def_at = sets_def_at;
+ sathelper.sets_any_undef_at = sets_any_undef_at;
+ sathelper.sets_all_undef_at = sets_all_undef_at;
+ sathelper.sets_init = sets_init;
+ sathelper.set_init_def = set_init_def;
+ sathelper.set_init_undef = set_init_undef;
+ sathelper.set_init_zero = set_init_zero;
+ sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
+ sathelper.ignore_unknown_cells = ignore_unknown_cells;
+
+ if (seq_len == 0) {
+ sathelper.setup();
+ if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+ sathelper.ez->assume(sathelper.ez->NOT(sathelper.setup_proof()));
+ } else {
+ std::vector<int> prove_bits;
+ for (int timestep = 1; timestep <= seq_len; timestep++) {
+ sathelper.setup(timestep, timestep == 1);
+ if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+ if (timestep > prove_skip)
+ prove_bits.push_back(sathelper.setup_proof(timestep));
+ }
+ if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+ sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits)));
+ }
+ sathelper.generate_model();
+
+ if (!cnf_file_name.empty())
+ {
+ FILE *f = fopen(cnf_file_name.c_str(), "w");
+ if (!f)
+ log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
+
+ log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
+ cnf_file_name.clear();
+
+ sathelper.ez->printDIMACS(f, false);
+ fclose(f);
+ }
+
+ int rerun_counter = 0;
+
+ rerun_solver:
+ log("\nSolving problem with %d variables and %d clauses..\n",
+ sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
+ log_flush();
+
+ if (sathelper.solve())
+ {
+ if (max_undef) {
+ log("SAT model found. maximizing number of undefs.\n");
+ sathelper.maximize_undefs();
+ }
+
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ log("SAT solving finished - model found:\n");
+ } else {
+ log("SAT proof finished - model found: FAIL!\n");
+ print_proof_failed();
+ }
+
+ sathelper.print_model();
+
+ if(!vcd_file_name.empty())
+ sathelper.dump_model_to_vcd(vcd_file_name);
+ if(!json_file_name.empty())
+ sathelper.dump_model_to_json(json_file_name);
+
+ if (loopcount != 0) {
+ loopcount--, rerun_counter++;
+ sathelper.invalidate_model(max_undef);
+ goto rerun_solver;
+ }
+
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
+ }
+ }
+ else
+ {
+ if (sathelper.gotTimeout)
+ goto timeout;
+ if (rerun_counter)
+ log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
+ else if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ log("SAT solving finished - no model found.\n");
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and found no model!\n");
+ }
+ } else {
+ log("SAT proof finished - no model found: SUCCESS!\n");
+ print_qed();
+ if (falsify) {
+ log("\n");
+ log_error("Called with -falsify and proof did succeed!\n");
+ }
+ }
+ }
+
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
+ if (falsify && rerun_counter) {
+ log("\n");
+ log_error("Called with -falsify and found a model!\n");
+ }
+ } else {
+ if (verify && rerun_counter) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
+ }
+ }
+
+ if (0) {
+ timeout:
+ log("Interrupted SAT solver: TIMEOUT!\n");
+ print_timeout();
+ if (fail_on_timeout)
+ log_error("Called with -verify and proof did time out!\n");
+ }
+ }
+} SatPass;
+
+PRIVATE_NAMESPACE_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-29 09:45:46 +0000