aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/opt/opt_merge.cc4
-rw-r--r--passes/sat/fmcombine.cc3
-rw-r--r--passes/sat/qbfsat.cc89
-rw-r--r--passes/sat/sim.cc5
-rw-r--r--passes/tests/test_cell.cc4
5 files changed, 79 insertions, 26 deletions
diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc
index a95aa74c1..f03faa9cf 100644
--- a/passes/opt/opt_merge.cc
+++ b/passes/opt/opt_merge.cc
@@ -298,9 +298,7 @@ struct OptMergeWorker
module->connect(RTLIL::SigSig(it.second, other_sig));
assign_map.add(it.second, other_sig);
- if (it.first == ID::Q && (cell->type.begins_with("$dff") || cell->type.begins_with("$dlatch") ||
- cell->type.begins_with("$_DFF") || cell->type.begins_with("$_DLATCH") || cell->type.begins_with("$_SR_") ||
- cell->type.in(ID($adff), ID($sr), ID($ff), ID($_FF_)))) {
+ if (it.first == ID::Q && RTLIL::builtin_ff_cell_types().count(cell->type)) {
for (auto c : it.second.chunks()) {
auto jt = c.wire->attributes.find(ID::init);
if (jt == c.wire->attributes.end())
diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index 5694a7473..cb49edac3 100644
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@@ -114,8 +114,7 @@ struct FmcombineWorker
Cell *gold = import_prim_cell(cell, "_gold");
Cell *gate = import_prim_cell(cell, "_gate");
if (opts.initeq) {
- if (cell->type.in(ID($ff), ID($dff), ID($dffe),
- ID($dffsr), ID($adff), ID($dlatch), ID($dlatchsr))) {
+ if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
SigSpec gold_q = gold->getPort(ID::Q);
SigSpec gate_q = gate->getPort(ID::Q);
SigSpec en = module->Initstate(NEW_ID);
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index f4624ab3b..136259558 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -51,6 +51,7 @@ struct QbfSolveOptions {
bool nooptimize, nobisection;
bool sat, unsat, show_smtbmc;
enum Solver{Z3, Yices, CVC4} solver;
+ enum OptimizationLevel{O0, O1, O2} oflag;
int timeout;
std::string specialize_soln_file;
std::string write_soln_soln_file;
@@ -59,7 +60,7 @@ 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),
- solver(Yices), timeout(0), argidx(0) {};
+ solver(Yices), oflag(O0), timeout(0), argidx(0) {};
};
std::string get_solver_name(const QbfSolveOptions &opt) {
@@ -147,6 +148,9 @@ void recover_solution(QbfSolutionType &sol) {
dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_map(RTLIL::Module *module, const QbfSolutionType &sol) {
dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> hole_loc_idx_to_sigbit;
+ pool<RTLIL::SigBit> anyconst_sigbits;
+ dict<RTLIL::SigBit, RTLIL::SigBit> anyconst_sigbit_to_wire_sigbit;
+
for (auto cell : module->cells()) {
pool<std::string> cell_src = cell->get_strpool_attribute(ID::src);
auto pos = sol.hole_to_value.find(cell_src);
@@ -154,10 +158,30 @@ dict<std::pair<pool<std::string>, int>, RTLIL::SigBit> get_hole_loc_idx_sigbit_m
RTLIL::SigSpec port_y = cell->getPort(ID::Y);
for (int i = GetSize(port_y) - 1; i >= 0; --i) {
hole_loc_idx_to_sigbit[std::make_pair(pos->first, i)] = port_y[i];
+ anyconst_sigbits.insert(port_y[i]);
+ }
+ }
+ }
+
+ for (auto &conn : module->connections()) {
+ auto lhs = conn.first;
+ auto rhs = conn.second;
+ for (auto i = 0; i < GetSize(rhs); ++i) {
+ if (anyconst_sigbits[rhs[i]]) {
+ auto pos = anyconst_sigbit_to_wire_sigbit.find(rhs[i]);
+ if (pos != anyconst_sigbit_to_wire_sigbit.end())
+ log_cmd_error("conflicting names for hole $anyconst sigbit %s\n", log_signal(rhs[i]));
+ anyconst_sigbit_to_wire_sigbit[rhs[i]] = lhs[i];
}
}
}
+ for (auto &it : hole_loc_idx_to_sigbit) {
+ auto pos = anyconst_sigbit_to_wire_sigbit.find(it.second);
+ if (pos != anyconst_sigbit_to_wire_sigbit.end())
+ it.second = pos->second;
+ }
+
return hole_loc_idx_to_sigbit;
}
@@ -274,8 +298,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) {
pool<std::string> hole_loc_pool(locs.begin(), locs.end());
auto hole_cell_it = anyconst_loc_to_cell.find(hole_loc_pool);
if (hole_cell_it == anyconst_loc_to_cell.end())
- YS_DEBUGTRAP;
- //log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str());
+ log_cmd_error("cannot find matching wire name or $anyconst cell location for hole spec \"%s\"\n", buf.c_str());
RTLIL::Cell *hole_cell = hole_cell_it->second;
hole_sigbit = hole_cell->getPort(ID::Y)[hole_bit];
@@ -438,8 +461,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
RTLIL::Module *module = mod;
RTLIL::Design *design = module->design;
std::string module_name = module->name.str();
- RTLIL::Wire *wire_to_optimize = nullptr;
- RTLIL::IdString wire_to_optimize_name;
+ RTLIL::IdString wire_to_optimize_name = "";
bool maximize = false;
log_assert(module->design != nullptr);
@@ -452,19 +474,30 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
assume_miter_outputs(module, opt);
//Find the wire to be optimized, if any:
- for (auto wire : module->wires())
- if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize"))
- wire_to_optimize = wire;
- if (wire_to_optimize != nullptr) {
- wire_to_optimize_name = wire_to_optimize->name;
- maximize = wire_to_optimize->get_bool_attribute("\\maximize");
+ for (auto wire : module->wires()) {
+ if (wire->get_bool_attribute("\\maximize") || wire->get_bool_attribute("\\minimize")) {
+ wire_to_optimize_name = wire->name;
+ maximize = wire->get_bool_attribute("\\maximize");
+ if (opt.nooptimize) {
+ if (maximize)
+ wire->set_bool_attribute("\\maximize", false);
+ else
+ wire->set_bool_attribute("\\minimize", false);
+ }
+ }
}
- if (opt.nobisection || opt.nooptimize || wire_to_optimize == nullptr) {
- if (wire_to_optimize != nullptr && opt.nooptimize) {
- wire_to_optimize->set_bool_attribute("\\maximize", false);
- wire_to_optimize->set_bool_attribute("\\minimize", false);
- }
+ //If -O1 or -O2 was specified, use ABC to simplify the problem:
+ if (opt.oflag == opt.OptimizationLevel::O1)
+ Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor,-N,10,-lz;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str());
+ else if (opt.oflag == opt.OptimizationLevel::O2)
+ Pass::call(module->design, "abc -g AND,NAND,OR,NOR,XOR,XNOR,MUX,NMUX -script +print_stats;strash;print_stats;drwsat;print_stats;dch,-S,1000000,-C,100000,-p;print_stats;fraig;print_stats;refactor,-N,15,-lz;print_stats;dc2,-pbl;print_stats;drwsat;print_stats;&get,-n;&dch,-pem;&nf;&put " + mod->name.str());
+ if (opt.oflag != opt.OptimizationLevel::O0) {
+ Pass::call(module->design, "techmap");
+ Pass::call(module->design, "opt");
+ }
+
+ if (opt.nobisection || opt.nooptimize || wire_to_optimize_name == "") {
ret = call_qbf_solver(module, opt, tempdir_name, false, 0);
} else {
//Do the iterated bisection method:
@@ -473,8 +506,9 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
unsigned int failure = 0;
unsigned int cur_thresh = 0;
- log_assert(wire_to_optimize != nullptr);
- log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), log_signal(wire_to_optimize));
+ log_assert(wire_to_optimize_name != "");
+ log_assert(module->wire(wire_to_optimize_name) != nullptr);
+ log("%s wire \"%s\".\n", (maximize? "Maximizing" : "Minimizing"), wire_to_optimize_name.c_str());
//If maximizing, grow until we get a failure. Then bisect success and failure.
while (failure == 0 || difference(success, failure) > 1) {
@@ -607,6 +641,22 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
}
continue;
}
+ else if (args[opt.argidx].substr(0, 2) == "-O" && args[opt.argidx].size() == 3) {
+ switch (args[opt.argidx][2]) {
+ case '0':
+ opt.oflag = opt.OptimizationLevel::O0;
+ break;
+ case '1':
+ opt.oflag = opt.OptimizationLevel::O1;
+ break;
+ case '2':
+ opt.oflag = opt.OptimizationLevel::O2;
+ break;
+ default:
+ log_cmd_error("unknown argument %s\n", args[opt.argidx].c_str());
+ }
+ continue;
+ }
else if (args[opt.argidx] == "-sat") {
opt.sat = true;
continue;
@@ -721,6 +771,9 @@ struct QbfSatPass : public Pass {
log(" -timeout <value>\n");
log(" Set the per-iteration timeout in seconds.\n");
log("\n");
+ log(" -O0, -O1, -O2\n");
+ log(" Control the use of ABC to simplify the QBF-SAT problem before solving.\n");
+ log("\n");
log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n");
log("\n");
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1ab082b09..fb496ff87 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -163,7 +163,10 @@ struct SimInstance
mem_database[cell] = mem;
}
-
+ if (cell->type.in(ID($memwr),ID($memrd)))
+ {
+ log_error("$memrd and $memwr cells have to be merged to stand-alone $mem cells (execute memory_collect pass)\n");
+ }
if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
formal_database.insert(cell);
}
diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc
index 125efbaa3..bdb475d3b 100644
--- a/passes/tests/test_cell.cc
+++ b/passes/tests/test_cell.cc
@@ -909,7 +909,7 @@ struct TestCellPass : public Pass {
if (!ilang_file.empty()) {
if (!selected_cell_types.empty())
log_cmd_error("Do not specify any cell types when using -f.\n");
- selected_cell_types.push_back("ilang");
+ selected_cell_types.push_back(ID(ilang));
}
if (selected_cell_types.empty())
@@ -921,7 +921,7 @@ struct TestCellPass : public Pass {
for (int i = 0; i < num_iter; i++)
{
RTLIL::Design *design = new RTLIL::Design;
- if (cell_type == "ilang")
+ if (cell_type == ID(ilang))
Frontend::frontend_call(design, NULL, std::string(), "ilang " + ilang_file);
else
create_gold_module(design, cell_type, cell_types.at(cell_type), constmode, muxdiv);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-07 20:18:30 +0000