summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/assertpmux.cc240
-rw-r--r--passes/sat/eval.cc2
-rw-r--r--passes/sat/expose.cc2
-rw-r--r--passes/sat/freduce.cc2
-rw-r--r--passes/sat/miter.cc12
-rw-r--r--passes/sat/sat.cc217
7 files changed, 357 insertions, 119 deletions
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index 4fa6bf0d..0c5f6fc6 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -4,4 +4,5 @@ OBJS += passes/sat/freduce.o
OBJS += passes/sat/eval.o
OBJS += passes/sat/miter.o
OBJS += passes/sat/expose.o
+OBJS += passes/sat/assertpmux.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/eval.cc b/passes/sat/eval.cc
index 614a1bd3..09f69cc5 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -389,7 +389,7 @@ struct EvalPass : public Pass {
std::vector<std::string> shows, tables;
bool set_undef = false;
- log_header("Executing EVAL pass (evaluate the circuit given an input).\n");
+ log_header(design, "Executing EVAL pass (evaluate the circuit given an input).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
index ebdf2ed5..9427547f 100644
--- a/passes/sat/expose.cc
+++ b/passes/sat/expose.cc
@@ -262,7 +262,7 @@ struct ExposePass : public Pass {
bool flag_evert_dff = false;
std::string sep = ".";
- log_header("Executing EXPOSE pass (exposing internal signals as outputs).\n");
+ log_header(design, "Executing EXPOSE pass (exposing internal signals as outputs).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 373b8048..77263f6a 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -798,7 +798,7 @@ struct FreducePass : public Pass {
inv_mode = false;
dump_prefix = std::string();
- log_header("Executing FREDUCE pass (perform functional reduction).\n");
+ log_header(design, "Executing FREDUCE pass (perform functional reduction).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 682299ef..4854e19b 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -32,7 +32,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
bool flag_make_assert = false;
bool flag_flatten = false;
- log_header("Executing MITER pass (creating miter circuit).\n");
+ log_header(design, "Executing MITER pass (creating miter circuit).\n");
size_t argidx;
for (argidx = 2; argidx < args.size(); argidx++)
@@ -254,7 +254,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
if (flag_flatten) {
log_push();
- Pass::call_on_module(design, miter_module, "flatten; opt_const -keepdc -undriven;;");
+ Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;");
log_pop();
}
}
@@ -264,7 +264,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
bool flag_make_outputs = false;
bool flag_flatten = false;
- log_header("Executing MITER pass (creating miter circuit).\n");
+ log_header(design, "Executing MITER pass (creating miter circuit).\n");
size_t argidx;
for (argidx = 2; argidx < args.size(); argidx++)
@@ -327,7 +327,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
if (flag_flatten) {
log_push();
- Pass::call_on_module(design, module, "opt_const -keepdc -undriven;;");
+ Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;");
log_pop();
}
}
@@ -361,7 +361,7 @@ struct MiterPass : public Pass {
log(" also create an 'assert' cell that checks if trigger is always low.\n");
log("\n");
log(" -flatten\n");
- log(" call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\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");
@@ -375,7 +375,7 @@ struct MiterPass : public Pass {
log(" keep module output ports.\n");
log("\n");
log(" -flatten\n");
- log(" call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\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)
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 2e9c6d2f..a6ac7afd 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -90,106 +90,16 @@ struct SatHelper
log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig));
}
- void setup_init()
- {
- log ("\nSetting up initial state:\n");
-
- 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 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 constraint equation: %s = %s\n\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, 1));
- }
-
- void setup(int timestep = -1)
+ 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;
@@ -341,6 +251,97 @@ struct SatHelper
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)
@@ -630,11 +631,11 @@ struct SatHelper
"---------------------------------------------------------------------------------------------------";
if (last_timestep == -2) {
log(max_timestep > 0 ? " Time " : " ");
- log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
+ log("%-*s %11s %9s %*s\n", maxModelName+5, "Signal Name", "Dec", "Hex", maxModelWidth+3, "Bin");
}
log(max_timestep > 0 ? " ---- " : " ");
- log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
- hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
+ log("%*.*s %11.11s %9.9s %*.*s\n", maxModelName+5, maxModelName+5,
+ hline, hline, hline, maxModelWidth+3, maxModelWidth+3, hline);
last_timestep = info.timestep;
}
@@ -647,9 +648,9 @@ struct SatHelper
log(" ");
if (info.width <= 32 && !found_undef)
- log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str());
+ 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 %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
+ log("%-*s %11s %9s %*s\n", maxModelName+5, info.description.c_str(), "--", "--", maxModelWidth+3, value.as_string().c_str());
}
if (last_timestep == -2)
@@ -1073,7 +1074,7 @@ struct SatPass : public Pass {
int tempinduct_skip = 0, stepsize = 1;
std::string vcd_file_name, json_file_name, cnf_file_name;
- log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
+ log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -1377,7 +1378,6 @@ struct SatPass : public Pass {
SatHelper basecase(design, module, enable_undef);
SatHelper inductstep(design, module, enable_undef);
- bool basecase_setup_init = true;
basecase.sets = sets;
basecase.set_assumes = set_assumes;
@@ -1403,7 +1403,7 @@ struct SatPass : public Pass {
for (int timestep = 1; timestep <= seq_len; timestep++)
if (!tempinduct_inductonly)
- basecase.setup(timestep);
+ basecase.setup(timestep, timestep == 1);
inductstep.sets = sets;
inductstep.set_assumes = set_assumes;
@@ -1436,15 +1436,10 @@ struct SatPass : public Pass {
if (!tempinduct_inductonly)
{
- basecase.setup(seq_len + inductlen);
+ basecase.setup(seq_len + inductlen, seq_len + inductlen == 1);
int property = basecase.setup_proof(seq_len + inductlen);
basecase.generate_model();
- if (basecase_setup_init) {
- basecase.setup_init();
- basecase_setup_init = false;
- }
-
if (inductlen > 1)
basecase.force_unique_state(seq_len + 1, seq_len + inductlen);
@@ -1452,6 +1447,7 @@ struct SatPass : public Pass {
{
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");
@@ -1522,6 +1518,7 @@ struct SatPass : public Pass {
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)
@@ -1599,14 +1596,13 @@ struct SatPass : public Pass {
} else {
std::vector<int> prove_bits;
for (int timestep = 1; timestep <= seq_len; timestep++) {
- sathelper.setup(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.setup_init();
}
sathelper.generate_model();
@@ -1628,6 +1624,7 @@ struct SatPass : public Pass {
rerun_solver:
log("\nSolving problem with %d variables and %d clauses..\n",
sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses());
+ log_flush();
if (sathelper.solve())
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-19 17:08:28 +0000