aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/Makefile.inc1
-rw-r--r--passes/cmds/printattrs.cc90
-rw-r--r--passes/cmds/stat.cc2
-rw-r--r--passes/hierarchy/hierarchy.cc4
-rw-r--r--passes/memory/memory_share.cc2
-rw-r--r--passes/opt/opt_expr.cc58
-rw-r--r--passes/opt/opt_share.cc4
-rw-r--r--passes/opt/share.cc6
-rw-r--r--passes/opt/wreduce.cc4
-rw-r--r--passes/sat/qbfsat.cc133
-rw-r--r--passes/tests/test_cell.cc4
11 files changed, 260 insertions, 48 deletions
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index a88980eaf..53bfd40c6 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -39,3 +39,4 @@ OBJS += passes/cmds/bugpoint.o
endif
OBJS += passes/cmds/scratchpad.o
OBJS += passes/cmds/logger.o
+OBJS += passes/cmds/printattrs.o
diff --git a/passes/cmds/printattrs.cc b/passes/cmds/printattrs.cc
new file mode 100644
index 000000000..80dbfa259
--- /dev/null
+++ b/passes/cmds/printattrs.cc
@@ -0,0 +1,90 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
+ *
+ * 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"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct PrintAttrsPass : public Pass {
+ PrintAttrsPass() : Pass("printattrs", "print attributes of selected objects") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" printattrs [selection]\n");
+ log("\n");
+ log("Print all attributes of the selected objects.\n");
+ log("\n");
+ log("\n");
+ }
+
+ static std::string get_indent_str(const unsigned int indent) {
+ return stringf("%*s", indent, "");
+ }
+
+ static void log_const(const RTLIL::IdString &s, const RTLIL::Const &x, const unsigned int indent) {
+ if (x.flags == RTLIL::CONST_FLAG_STRING)
+ log("%s(* %s=\"%s\" *)\n", get_indent_str(indent).c_str(), log_id(s), x.decode_string().c_str());
+ else if (x.flags == RTLIL::CONST_FLAG_NONE)
+ log("%s(* %s=%s *)\n", get_indent_str(indent).c_str(), log_id(s), x.as_string().c_str());
+ else
+ log_assert(x.flags == RTLIL::CONST_FLAG_STRING || x.flags == RTLIL::CONST_FLAG_NONE); //intended to fail
+ }
+
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ size_t argidx = 1;
+ extra_args(args, argidx, design);
+
+ unsigned int indent = 0;
+ for (auto mod : design->selected_modules())
+ {
+ if (design->selected_whole_module(mod)) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(mod->name));
+ indent += 2;
+ for (auto &it : mod->attributes)
+ log_const(it.first, it.second, indent);
+ }
+
+ for (auto cell : mod->selected_cells()) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(cell->name));
+ indent += 2;
+ for (auto &it : cell->attributes)
+ log_const(it.first, it.second, indent);
+ indent -= 2;
+ }
+
+ for (auto wire : mod->selected_wires()) {
+ log("%s%s\n", get_indent_str(indent).c_str(), log_id(wire->name));
+ indent += 2;
+ for (auto &it : wire->attributes)
+ log_const(it.first, it.second, indent);
+ indent -= 2;
+ }
+
+ if (design->selected_whole_module(mod))
+ indent -= 2;
+ }
+
+ log("\n");
+ }
+} PrintAttrsPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index 6c4bc0e5b..30436d829 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -109,7 +109,7 @@ struct statdata_t
ID($lut), ID($and), ID($or), ID($xor), ID($xnor),
ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx),
ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt),
- ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($pow), ID($alu))) {
+ ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow), ID($alu))) {
int width_a = cell->hasPort(ID::A) ? GetSize(cell->getPort(ID::A)) : 0;
int width_b = cell->hasPort(ID::B) ? GetSize(cell->getPort(ID::B)) : 0;
int width_y = cell->hasPort(ID::Y) ? GetSize(cell->getPort(ID::Y)) : 0;
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 95d74d1eb..f99d1509d 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -574,9 +574,9 @@ struct HierarchyPass : public Pass {
log("\n");
log("In parametric designs, a module might exists in several variations with\n");
log("different parameter values. This pass looks at all modules in the current\n");
- log("design an re-runs the language frontends for the parametric modules as\n");
+ log("design and re-runs the language frontends for the parametric modules as\n");
log("needed. It also resolves assignments to wired logic data types (wand/wor),\n");
- log("resolves positional module parameters, unroll array instances, and more.\n");
+ log("resolves positional module parameters, unrolls array instances, and more.\n");
log("\n");
log(" -check\n");
log(" also check the design hierarchy. this generates an error when\n");
diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc
index 477246687..e11958bd6 100644
--- a/passes/memory/memory_share.cc
+++ b/passes/memory/memory_share.cc
@@ -715,6 +715,8 @@ struct MemoryShareWorker
cone_ct.cell_types.erase(ID($mul));
cone_ct.cell_types.erase(ID($mod));
cone_ct.cell_types.erase(ID($div));
+ cone_ct.cell_types.erase(ID($modfloor));
+ cone_ct.cell_types.erase(ID($divfloor));
cone_ct.cell_types.erase(ID($pow));
cone_ct.cell_types.erase(ID($shl));
cone_ct.cell_types.erase(ID($shr));
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 777a24777..e5b8bda95 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -864,7 +864,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
skip_fine_alu:
if (cell->type.in(ID($reduce_xor), ID($reduce_xnor), ID($shift), ID($shiftx), ID($shl), ID($shr), ID($sshl), ID($sshr),
- ID($lt), ID($le), ID($ge), ID($gt), ID($neg), ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($pow)))
+ ID($lt), ID($le), ID($ge), ID($gt), ID($neg), ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow)))
{
RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
RTLIL::SigSpec sig_b = cell->hasPort(ID::B) ? assign_map(cell->getPort(ID::B)) : RTLIL::SigSpec();
@@ -883,7 +883,7 @@ skip_fine_alu:
if (0) {
found_the_x_bit:
cover_list("opt.opt_expr.xbit", "$reduce_xor", "$reduce_xnor", "$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx",
- "$lt", "$le", "$ge", "$gt", "$neg", "$add", "$sub", "$mul", "$div", "$mod", "$pow", cell->type.str());
+ "$lt", "$le", "$ge", "$gt", "$neg", "$add", "$sub", "$mul", "$div", "$mod", "$divfloor", "$modfloor", "$pow", cell->type.str());
if (cell->type.in(ID($reduce_xor), ID($reduce_xnor), ID($lt), ID($le), ID($ge), ID($gt)))
replace_cell(assign_map, module, cell, "x-bit in input", ID::Y, RTLIL::State::Sx);
else
@@ -1469,6 +1469,8 @@ skip_identity:
FOLD_2ARG_CELL(mul)
FOLD_2ARG_CELL(div)
FOLD_2ARG_CELL(mod)
+ FOLD_2ARG_CELL(divfloor)
+ FOLD_2ARG_CELL(modfloor)
FOLD_2ARG_CELL(pow)
FOLD_1ARG_CELL(pos)
@@ -1583,9 +1585,11 @@ skip_identity:
}
}
- if (!keepdc && cell->type.in(ID($div), ID($mod)))
+ if (!keepdc && cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor)))
{
+ bool a_signed = cell->parameters[ID::A_SIGNED].as_bool();
bool b_signed = cell->parameters[ID::B_SIGNED].as_bool();
+ SigSpec sig_a = assign_map(cell->getPort(ID::A));
SigSpec sig_b = assign_map(cell->getPort(ID::B));
SigSpec sig_y = assign_map(cell->getPort(ID::Y));
@@ -1610,11 +1614,13 @@ skip_identity:
for (int i = 1; i < (b_signed ? sig_b.size()-1 : sig_b.size()); i++)
if (b_val == (1 << i))
{
- if (cell->type == ID($div))
+ if (cell->type.in(ID($div), ID($divfloor)))
{
cover("opt.opt_expr.div_shift");
- log_debug("Replacing divide-by-%d cell `%s' in module `%s' with shift-by-%d.\n",
+ bool is_truncating = cell->type == ID($div);
+ log_debug("Replacing %s-divide-by-%d cell `%s' in module `%s' with shift-by-%d.\n",
+ is_truncating ? "truncating" : "flooring",
b_val, cell->name.c_str(), module->name.c_str(), i);
std::vector<RTLIL::SigBit> new_b = RTLIL::SigSpec(i, 6);
@@ -1622,17 +1628,35 @@ skip_identity:
while (GetSize(new_b) > 1 && new_b.back() == RTLIL::State::S0)
new_b.pop_back();
- cell->type = ID($shr);
+ cell->type = ID($sshr);
cell->parameters[ID::B_WIDTH] = GetSize(new_b);
cell->parameters[ID::B_SIGNED] = false;
cell->setPort(ID::B, new_b);
+
+ // Truncating division is the same as flooring division, except when
+ // the result is negative and there is a remainder - then trunc = floor + 1
+ if (is_truncating && a_signed) {
+ Wire *flooring = module->addWire(NEW_ID, sig_y.size());
+ cell->setPort(ID::Y, flooring);
+
+ Wire *result_neg = module->addWire(NEW_ID);
+ module->addXor(NEW_ID, sig_a[sig_a.size()-1], sig_b[sig_b.size()-1], result_neg);
+ Wire *rem_nonzero = module->addWire(NEW_ID);
+ module->addReduceOr(NEW_ID, sig_a.extract(0, i), rem_nonzero);
+ Wire *should_add = module->addWire(NEW_ID);
+ module->addAnd(NEW_ID, result_neg, rem_nonzero, should_add);
+ module->addAdd(NEW_ID, flooring, should_add, sig_y);
+ }
+
cell->check();
}
- else
+ else if (cell->type.in(ID($mod), ID($modfloor)))
{
cover("opt.opt_expr.mod_mask");
- log_debug("Replacing modulo-by-%d cell `%s' in module `%s' with bitmask.\n",
+ bool is_truncating = cell->type == ID($mod);
+ log_debug("Replacing %s-modulo-by-%d cell `%s' in module `%s' with bitmask.\n",
+ is_truncating ? "truncating" : "flooring",
b_val, cell->name.c_str(), module->name.c_str());
std::vector<RTLIL::SigBit> new_b = RTLIL::SigSpec(State::S1, i);
@@ -1643,6 +1667,24 @@ skip_identity:
cell->type = ID($and);
cell->parameters[ID::B_WIDTH] = GetSize(new_b);
cell->setPort(ID::B, new_b);
+
+ // truncating modulo has the same masked bits as flooring modulo, but
+ // the sign bits are those of A (except when R=0)
+ if (is_truncating && a_signed) {
+ Wire *flooring = module->addWire(NEW_ID, sig_y.size());
+ cell->setPort(ID::Y, flooring);
+ SigSpec truncating = SigSpec(flooring).extract(0, i);
+
+ Wire *rem_nonzero = module->addWire(NEW_ID);
+ module->addReduceOr(NEW_ID, truncating, rem_nonzero);
+ SigSpec a_sign = sig_a[sig_a.size()-1];
+ Wire *extend_bit = module->addWire(NEW_ID);
+ module->addAnd(NEW_ID, a_sign, rem_nonzero, extend_bit);
+
+ truncating.append(extend_bit);
+ module->addPos(NEW_ID, truncating, sig_y, true);
+ }
+
cell->check();
}
diff --git a/passes/opt/opt_share.cc b/passes/opt/opt_share.cc
index 1f69c98f4..cbace7bac 100644
--- a/passes/opt/opt_share.cc
+++ b/passes/opt/opt_share.cc
@@ -103,7 +103,7 @@ bool cell_supported(RTLIL::Cell *cell)
if (sig_bi.is_fully_const() && sig_ci.is_fully_const() && sig_bi == sig_ci)
return true;
- } else if (cell->type.in(LOGICAL_OPS, SHIFT_OPS, BITWISE_OPS, RELATIONAL_OPS, ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($concat))) {
+ } else if (cell->type.in(LOGICAL_OPS, SHIFT_OPS, BITWISE_OPS, RELATIONAL_OPS, ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($concat))) {
return true;
}
@@ -130,7 +130,7 @@ bool mergeable(RTLIL::Cell *a, RTLIL::Cell *b)
RTLIL::IdString decode_port_semantics(RTLIL::Cell *cell, RTLIL::IdString port_name)
{
- if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt), ID($div), ID($mod), ID($concat), SHIFT_OPS) && port_name == ID::B)
+ if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($concat), SHIFT_OPS) && port_name == ID::B)
return port_name;
return "";
diff --git a/passes/opt/share.cc b/passes/opt/share.cc
index 2839507b0..988253edf 100644
--- a/passes/opt/share.cc
+++ b/passes/opt/share.cc
@@ -376,7 +376,7 @@ struct ShareWorker
continue;
}
- if (cell->type.in(ID($mul), ID($div), ID($mod))) {
+ if (cell->type.in(ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
if (config.opt_aggressive || cell->parameters.at(ID::Y_WIDTH).as_int() >= 4)
shareable_cells.insert(cell);
continue;
@@ -1133,6 +1133,8 @@ struct ShareWorker
cone_ct.cell_types.erase(ID($mul));
cone_ct.cell_types.erase(ID($mod));
cone_ct.cell_types.erase(ID($div));
+ cone_ct.cell_types.erase(ID($modfloor));
+ cone_ct.cell_types.erase(ID($divfloor));
cone_ct.cell_types.erase(ID($pow));
cone_ct.cell_types.erase(ID($shl));
cone_ct.cell_types.erase(ID($shr));
@@ -1512,6 +1514,8 @@ struct SharePass : public Pass {
config.generic_bin_ops.insert(ID($sub));
config.generic_bin_ops.insert(ID($div));
config.generic_bin_ops.insert(ID($mod));
+ config.generic_bin_ops.insert(ID($divfloor));
+ config.generic_bin_ops.insert(ID($modfloor));
// config.generic_bin_ops.insert(ID($pow));
config.generic_uni_ops.insert(ID($logic_not));
diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc
index 195400bf0..f60f2f8a8 100644
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@@ -37,7 +37,7 @@ struct WreduceConfig
ID($and), ID($or), ID($xor), ID($xnor),
ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx),
ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt),
- ID($add), ID($sub), ID($mul), // ID($div), ID($mod), ID($pow),
+ ID($add), ID($sub), ID($mul), // ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow),
ID($mux), ID($pmux),
ID($dff), ID($adff)
});
@@ -545,7 +545,7 @@ struct WreducePass : public Pass {
}
}
- if (c->type.in(ID($div), ID($mod), ID($pow)))
+ if (c->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow)))
{
SigSpec A = c->getPort(ID::A);
int original_a_width = GetSize(A);
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index c42760488..d6dbf8ef4 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -41,6 +41,8 @@ struct QbfSolveOptions {
bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
bool nooptimize, nobisection;
bool sat, unsat, show_smtbmc;
+ enum Solver{Z3, Yices, CVC4} solver;
+ int timeout;
std::string specialize_soln_file;
std::string write_soln_soln_file;
std::string dump_final_smt2_file;
@@ -48,12 +50,29 @@ struct QbfSolveOptions {
QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false),
- argidx(0) {};
+ solver(Yices), timeout(0), argidx(0) {};
};
+std::string get_solver_name(const QbfSolveOptions &opt) {
+ if (opt.solver == opt.Solver::Z3)
+ return "z3";
+ else if (opt.solver == opt.Solver::Yices)
+ return "yices";
+ else if (opt.solver == opt.Solver::CVC4)
+ return "cvc4";
+ else
+ log_cmd_error("unknown solver specified.\n");
+ return "";
+}
+
void recover_solution(QbfSolutionType &sol) {
YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+ YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
+ YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
+ YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
+ YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
+ YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
#ifndef NDEBUG
@@ -74,14 +93,40 @@ void recover_solution(QbfSolutionType &sol) {
#endif
sol.hole_to_value[loc] = val;
}
- else if (YS_REGEX_NS::regex_search(x, sat_regex))
+ else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
sat_regex_found = true;
- else if (YS_REGEX_NS::regex_search(x, unsat_regex))
+ sol.sat = true;
+ sol.unknown = false;
+ }
+ else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
unsat_regex_found = true;
+ sol.sat = false;
+ sol.unknown = false;
+ }
else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
sol.unknown = true;
log_warning("solver ran out of memory\n");
}
+ else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
+ sol.unknown = true;
+ log_warning("solver timed out\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
+ sol.unknown = true;
+ log_warning("solver timed out\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
+ sol.unknown = true;
+ log_warning("solver returned \"unknown\"\n");
+ }
+ else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
+ unsat_regex_found = true;
+ sol.sat = false;
+ sol.unknown = false;
+ }
+ else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
+ sol.unknown = true;
+ }
}
#ifndef NDEBUG
log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
@@ -315,31 +360,23 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt,
QbfSolutionType ret;
const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2";
- const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
const std::string smtbmc_warning = "z3: WARNING:";
- const bool show_smtbmc = opt.show_smtbmc;
+ const std::string smtbmc_cmd = yosys_smtbmc_exe + " -s " + (get_solver_name(opt)) + (opt.timeout != 0? stringf(" --timeout %d", opt.timeout) : "") + " -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem" + (iter_num != 0? stringf("%d", iter_num) : "") + ".smt2 2>&1";
Pass::call(mod->design, smt2_command);
- auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &quiet](const std::string &line) {
+ auto process_line = [&ret, &smtbmc_warning, &opt, &quiet](const std::string &line) {
ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
auto warning_pos = line.find(smtbmc_warning);
if (warning_pos != std::string::npos)
log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
else
- if (show_smtbmc && !quiet)
+ if (opt.show_smtbmc && !quiet)
log("smtbmc output: %s", line.c_str());
};
log_header(mod->design, "Solving QBF-SAT problem.\n");
if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str());
- int retval = run_command(smtbmc_cmd, process_line);
- if (retval == 0) {
- ret.sat = true;
- ret.unknown = false;
- } else if (retval == 1) {
- ret.sat = false;
- ret.unknown = false;
- }
+ run_command(smtbmc_cmd, process_line);
recover_solution(ret);
return ret;
@@ -486,6 +523,35 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
opt.nobisection = true;
continue;
}
+ else if (args[opt.argidx] == "-solver") {
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("solver not specified.\n");
+ else {
+ if (args[opt.argidx+1] == "z3")
+ opt.solver = opt.Solver::Z3;
+ else if (args[opt.argidx+1] == "yices")
+ opt.solver = opt.Solver::Yices;
+ else if (args[opt.argidx+1] == "cvc4")
+ opt.solver = opt.Solver::CVC4;
+ else
+ log_cmd_error("Unknown solver \"%s\".\n", args[opt.argidx+1].c_str());
+ opt.argidx++;
+ }
+ continue;
+ }
+ else if (args[opt.argidx] == "-timeout") {
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("timeout not specified.\n");
+ else {
+ int timeout = atoi(args[opt.argidx+1].c_str());
+ if (timeout > 0)
+ opt.timeout = timeout;
+ else
+ log_cmd_error("timeout must be greater than 0.\n");
+ opt.argidx++;
+ }
+ continue;
+ }
else if (args[opt.argidx] == "-sat") {
opt.sat = true;
continue;
@@ -563,21 +629,20 @@ struct QbfSatPass : public Pass {
log("\n");
log(" qbfsat [options] [selection]\n");
log("\n");
- log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
- log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
- log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
- log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
- log("by default.\n");
+ log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n");
+ log("selected module. Existentially-quantified variables are declared by assigning a wire\n");
+ log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n");
+ log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n");
+ log("variables by default.\n");
log("\n");
log(" -nocleanup\n");
- log(" Do not delete temporary files and directories. Useful for\n");
- log(" debugging.\n");
+ log(" Do not delete temporary files and directories. Useful for debugging.\n");
log("\n");
log(" -dump-final-smt2 <file>\n");
log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
log("\n");
log(" -assume-outputs\n");
- log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
+ log(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n");
log("\n");
log(" -assume-negative-polarity\n");
log(" When adding $assume cells for one-bit module output wires, assume they are\n");
@@ -586,15 +651,21 @@ struct QbfSatPass : public Pass {
log("\n");
log(" -nooptimize\n");
log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n");
- log(" \"(minimize)\" in the SMTLIBv2, and generally make no attempt to optimize anything.\n");
+ log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n");
log("\n");
log(" -nobisection\n");
log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n");
log(" attempt to optimize that value with the default iterated solving and threshold\n");
log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n");
- log(" command in the SMTLIBv2 output and hope that the solver supports optimizing\n");
+ log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n");
log(" quantified bitvector problems.\n");
log("\n");
+ log(" -solver <solver>\n");
+ log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n");
+ log("\n");
+ log(" -timeout <value>\n");
+ log(" Set the per-iteration timeout in seconds.\n");
+ log("\n");
log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n");
log("\n");
@@ -605,15 +676,16 @@ struct QbfSatPass : public Pass {
log(" Print the output from yosys-smtbmc.\n");
log("\n");
log(" -specialize\n");
- log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
+ log(" If the problem is satisfiable, replace each \"$anyconst\" cell with its\n");
+ log(" corresponding constant value from the model produced by the solver.\n");
log("\n");
log(" -specialize-from-file <solution file>\n");
- log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
- log(" cells in the current module with values provided by the specified file.\n");
+ log(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n");
+ log(" cell in the current module with a constant value provided by the specified file.\n");
log("\n");
log(" -write-solution <solution file>\n");
- log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
- log(" to the specified file.");
+ log(" If the problem is satisfiable, write the corresponding constant value for each\n");
+ log(" \"$anyconst\" cell from the model produced by the solver to the specified file.");
log("\n");
log("\n");
}
@@ -641,7 +713,6 @@ struct QbfSatPass : public Pass {
QbfSolutionType ret = qbf_solve(module, opt);
module = design->module(module_name);
if (ret.unknown) {
- log_warning("solver did not give an answer\n");
if (opt.sat || opt.unsat)
log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
}
diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc
index cdbe922b2..c6801007d 100644
--- a/passes/tests/test_cell.cc
+++ b/passes/tests/test_cell.cc
@@ -264,7 +264,7 @@ static void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type,
cell->setPort(ID::Y, wire);
}
- if (muxdiv && cell_type.in(ID($div), ID($mod))) {
+ if (muxdiv && cell_type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
auto b_not_zero = module->ReduceBool(NEW_ID, cell->getPort(ID::B));
auto div_out = module->addWire(NEW_ID, GetSize(cell->getPort(ID::Y)));
module->addMux(NEW_ID, RTLIL::SigSpec(0, GetSize(div_out)), div_out, b_not_zero, cell->getPort(ID::Y));
@@ -839,6 +839,8 @@ struct TestCellPass : public Pass {
cell_types[ID($mul)] = "ABSY";
cell_types[ID($div)] = "ABSY";
cell_types[ID($mod)] = "ABSY";
+ cell_types[ID($divfloor)] = "ABSY";
+ cell_types[ID($modfloor)] = "ABSY";
// cell_types[ID($pow)] = "ABsY";
cell_types[ID($logic_not)] = "ASY";
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 13:26:24 +0000