diff options
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/cmds/logger.cc | 16 | ||||
| -rw-r--r-- | passes/opt/opt_clean.cc | 31 | ||||
| -rw-r--r-- | passes/opt/opt_expr.cc | 136 | ||||
| -rw-r--r-- | passes/sat/qbfsat.cc | 305 | ||||
| -rw-r--r-- | passes/techmap/abc9.cc | 125 | ||||
| -rw-r--r-- | passes/techmap/abc9_ops.cc | 1144 |
6 files changed, 1242 insertions, 515 deletions
diff --git a/passes/cmds/logger.cc b/passes/cmds/logger.cc index 9a27952d4..c9532eced 100644 --- a/passes/cmds/logger.cc +++ b/passes/cmds/logger.cc @@ -58,7 +58,8 @@ struct LoggerPass : public Pass { log(" do not print warnings for the specified experimental feature\n"); log("\n"); log(" -expect <type> <regex> <expected_count>\n"); - log(" expect log,warning or error to appear. In case of error return code is 0.\n"); + log(" expect log, warning or error to appear. matched errors will terminate\n"); + log(" with exit code 0.\n"); log("\n"); log(" -expect-no-warnings\n"); log(" gives error in case there is at least one warning that is not expected.\n"); @@ -158,12 +159,13 @@ struct LoggerPass : public Pass { log_cmd_error("Expected error message occurrences must be 1 !\n"); log("Added regex '%s' for warnings to expected %s list.\n", pattern.c_str(), type.c_str()); try { - if (type=="error") - log_expect_error.push_back(std::make_pair(YS_REGEX_COMPILE(pattern), LogExpectedItem(pattern, count))); - else if (type=="warning") - log_expect_warning.push_back(std::make_pair(YS_REGEX_COMPILE(pattern), LogExpectedItem(pattern, count))); - else - log_expect_log.push_back(std::make_pair(YS_REGEX_COMPILE(pattern), LogExpectedItem(pattern, count))); + if (type == "error") + log_expect_error[pattern] = LogExpectedItem(YS_REGEX_COMPILE(pattern), count); + else if (type == "warning") + log_expect_warning[pattern] = LogExpectedItem(YS_REGEX_COMPILE(pattern), count); + else if (type == "log") + log_expect_log[pattern] = LogExpectedItem(YS_REGEX_COMPILE(pattern), count); + else log_abort(); } catch (const YS_REGEX_NS::regex_error& e) { log_cmd_error("Error in regex expression '%s' !\n", pattern.c_str()); diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index 6271376f1..f7de02164 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -412,7 +412,7 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos return !del_wires_queue.empty(); } -bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose) +bool rmunused_module_init(RTLIL::Module *module, bool verbose) { bool did_something = false; CellTypes fftypes; @@ -445,9 +445,6 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose) for (auto wire : module->wires()) { - if (!purge_mode && wire->name[0] == '\\') - continue; - if (wire->attributes.count(ID::init) == 0) continue; @@ -464,11 +461,22 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose) if (wire_bit == mapped_wire_bit) goto next_wire; - if (qbits.count(sigmap(SigBit(wire, i))) == 0) - goto next_wire; + if (mapped_wire_bit.wire) { + if (qbits.count(mapped_wire_bit) == 0) + goto next_wire; - if (qbits.at(sigmap(SigBit(wire, i))) != init[i]) - goto next_wire; + if (qbits.at(mapped_wire_bit) != init[i]) + goto next_wire; + } + else { + if (mapped_wire_bit == State::Sx || mapped_wire_bit == State::Sz) + goto next_wire; + + if (mapped_wire_bit != init[i]) { + log_warning("Initial value conflict for %s resolving to %s but with init %s.\n", log_signal(wire_bit), log_signal(mapped_wire_bit), log_signal(init[i])); + goto next_wire; + } + } } if (verbose) @@ -512,7 +520,7 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool verbose, bool rmunused_module_cells(module, verbose); while (rmunused_module_signals(module, purge_mode, verbose)) { } - if (rminit && rmunused_module_init(module, purge_mode, verbose)) + if (rminit && rmunused_module_init(module, verbose)) while (rmunused_module_signals(module, purge_mode, verbose)) { } } @@ -611,8 +619,7 @@ struct CleanPass : public Pass { } break; } - if (argidx < args.size()) - extra_args(args, argidx, design); + extra_args(args, argidx, design); keep_cache.reset(design); @@ -627,7 +634,7 @@ struct CleanPass : public Pass { for (auto module : design->selected_whole_modules()) { if (module->has_processes()) continue; - rmunused_module(module, purge_mode, ys_debug(), false); + rmunused_module(module, purge_mode, ys_debug(), true); } log_suppressed(); diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc index 0f5bff680..777a24777 100644 --- a/passes/opt/opt_expr.cc +++ b/passes/opt/opt_expr.cc @@ -132,7 +132,7 @@ void replace_cell(SigMap &assign_map, RTLIL::Module *module, RTLIL::Cell *cell, did_something = true; } -bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutative, SigMap &sigmap) +bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutative, SigMap &sigmap, bool keepdc) { IdString b_name = cell->hasPort(ID::B) ? ID::B : ID::A; @@ -156,20 +156,36 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ int group_idx = GRP_DYN; RTLIL::SigBit bit_a = bits_a[i], bit_b = bits_b[i]; - if (cell->type == ID($or) && (bit_a == RTLIL::State::S1 || bit_b == RTLIL::State::S1)) - bit_a = bit_b = RTLIL::State::S1; - - if (cell->type == ID($and) && (bit_a == RTLIL::State::S0 || bit_b == RTLIL::State::S0)) - bit_a = bit_b = RTLIL::State::S0; + if (cell->type == ID($or)) { + if (bit_a == RTLIL::State::S1 || bit_b == RTLIL::State::S1) + bit_a = bit_b = RTLIL::State::S1; + } + else if (cell->type == ID($and)) { + if (bit_a == RTLIL::State::S0 || bit_b == RTLIL::State::S0) + bit_a = bit_b = RTLIL::State::S0; + } + else if (!keepdc) { + if (cell->type == ID($xor)) { + if (bit_a == bit_b) + bit_a = bit_b = RTLIL::State::S0; + } + else if (cell->type == ID($xnor)) { + if (bit_a == bit_b) + bit_a = bit_b = RTLIL::State::S1; // For consistency with gate-level which does $xnor -> $_XOR_ + $_NOT_ + } + } - if (bit_a.wire == NULL && bit_b.wire == NULL) - group_idx = GRP_CONST_AB; - else if (bit_a.wire == NULL) - group_idx = GRP_CONST_A; - else if (bit_b.wire == NULL && commutative) - group_idx = GRP_CONST_A, std::swap(bit_a, bit_b); - else if (bit_b.wire == NULL) - group_idx = GRP_CONST_B; + bool def = (bit_a != State::Sx && bit_a != State::Sz && bit_b != State::Sx && bit_b != State::Sz); + if (def || !keepdc) { + if (bit_a.wire == NULL && bit_b.wire == NULL) + group_idx = GRP_CONST_AB; + else if (bit_a.wire == NULL) + group_idx = GRP_CONST_A; + else if (bit_b.wire == NULL && commutative) + group_idx = GRP_CONST_A, std::swap(bit_a, bit_b); + else if (bit_b.wire == NULL) + group_idx = GRP_CONST_B; + } grouped_bits[group_idx][std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit_a, bit_b)].insert(bits_y[i]); } @@ -186,26 +202,77 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ if (grouped_bits[i].empty()) continue; - RTLIL::Wire *new_y = module->addWire(NEW_ID, GetSize(grouped_bits[i])); + RTLIL::SigSpec new_y = module->addWire(NEW_ID, GetSize(grouped_bits[i])); RTLIL::SigSpec new_a, new_b; RTLIL::SigSig new_conn; for (auto &it : grouped_bits[i]) { for (auto &bit : it.second) { new_conn.first.append(bit); - new_conn.second.append(RTLIL::SigBit(new_y, new_a.size())); + new_conn.second.append(new_y[new_a.size()]); } new_a.append(it.first.first); new_b.append(it.first.second); } if (cell->type.in(ID($and), ID($or)) && i == GRP_CONST_A) { + if (!keepdc) { + if (cell->type == ID($and)) + new_a.replace(dict<SigBit,SigBit>{{State::Sx, State::S0}, {State::Sz, State::S0}}, &new_b); + else if (cell->type == ID($or)) + new_a.replace(dict<SigBit,SigBit>{{State::Sx, State::S1}, {State::Sz, State::S1}}, &new_b); + else log_abort(); + } log_debug(" Direct Connection: %s (%s with %s)\n", log_signal(new_b), log_id(cell->type), log_signal(new_a)); module->connect(new_y, new_b); module->connect(new_conn); continue; } + if (cell->type.in(ID($xor), ID($xnor)) && i == GRP_CONST_A) { + SigSpec undef_a, undef_y, undef_b; + SigSpec def_y, def_a, def_b; + for (int i = 0; i < GetSize(new_y); i++) { + bool undef = new_a[i] == State::Sx || new_a[i] == State::Sz; + if (!keepdc && (undef || new_a[i] == new_b[i])) { + undef_a.append(new_a[i]); + if (cell->type == ID($xor)) + undef_b.append(State::S0); + // For consistency since simplemap does $xnor -> $_XOR_ + $_NOT_ + else if (cell->type == ID($xnor)) + undef_b.append(State::S1); + else log_abort(); + undef_y.append(new_y[i]); + } + else if (new_a[i] == State::S0 || new_a[i] == State::S1) { + undef_a.append(new_a[i]); + if (cell->type == ID($xor)) + undef_b.append(new_a[i] == State::S1 ? module->Not(NEW_ID, new_b[i]).as_bit() : new_b[i]); + else if (cell->type == ID($xnor)) + undef_b.append(new_a[i] == State::S1 ? new_b[i] : module->Not(NEW_ID, new_b[i]).as_bit()); + else log_abort(); + undef_y.append(new_y[i]); + } + else { + def_a.append(new_a[i]); + def_b.append(new_b[i]); + def_y.append(new_y[i]); + } + } + if (!undef_y.empty()) { + log_debug(" Direct Connection: %s (%s with %s)\n", log_signal(undef_b), log_id(cell->type), log_signal(undef_a)); + module->connect(undef_y, undef_b); + if (def_y.empty()) { + module->connect(new_conn); + continue; + } + } + new_a = std::move(def_a); + new_b = std::move(def_b); + new_y = std::move(def_y); + } + + RTLIL::Cell *c = module->addCell(NEW_ID, cell->type); c->setPort(ID::A, new_a); @@ -219,7 +286,7 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ } c->setPort(ID::Y, new_y); - c->parameters[ID::Y_WIDTH] = new_y->width; + c->parameters[ID::Y_WIDTH] = GetSize(new_y); c->check(); module->connect(new_conn); @@ -476,13 +543,13 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons } } - if (detect_const_and && (found_zero || found_inv)) { + if (detect_const_and && (found_zero || found_inv || (found_undef && consume_x))) { cover("opt.opt_expr.const_and"); replace_cell(assign_map, module, cell, "const_and", ID::Y, RTLIL::State::S0); goto next_cell; } - if (detect_const_or && (found_one || found_inv)) { + if (detect_const_or && (found_one || found_inv || (found_undef && consume_x))) { cover("opt.opt_expr.const_or"); replace_cell(assign_map, module, cell, "const_or", ID::Y, RTLIL::State::S1); goto next_cell; @@ -499,6 +566,22 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons { SigBit sig_a = assign_map(cell->getPort(ID::A)); SigBit sig_b = assign_map(cell->getPort(ID::B)); + if (!keepdc && (sig_a == sig_b || sig_a == State::Sx || sig_a == State::Sz || sig_b == State::Sx || sig_b == State::Sz)) { + if (cell->type.in(ID($xor), ID($_XOR_))) { + cover("opt.opt_expr.const_xor"); + replace_cell(assign_map, module, cell, "const_xor", ID::Y, RTLIL::State::S0); + goto next_cell; + } + if (cell->type.in(ID($xnor), ID($_XNOR_))) { + cover("opt.opt_expr.const_xnor"); + // For consistency since simplemap does $xnor -> $_XOR_ + $_NOT_ + int width = cell->getParam(ID::Y_WIDTH).as_int(); + replace_cell(assign_map, module, cell, "const_xnor", ID::Y, SigSpec(RTLIL::State::S1, width)); + goto next_cell; + } + log_abort(); + } + if (!sig_a.wire) std::swap(sig_a, sig_b); if (sig_b == State::S0 || sig_b == State::S1) { @@ -550,7 +633,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons if (do_fine) { if (cell->type.in(ID($not), ID($pos), ID($and), ID($or), ID($xor), ID($xnor))) - if (group_cell_inputs(module, cell, true, assign_map)) + if (group_cell_inputs(module, cell, true, assign_map, keepdc)) goto next_cell; if (cell->type.in(ID($logic_not), ID($logic_and), ID($logic_or), ID($reduce_or), ID($reduce_and), ID($reduce_bool))) @@ -904,8 +987,10 @@ skip_fine_alu: if (input.match("01")) ACTION_DO_Y(1); if (input.match("10")) ACTION_DO_Y(1); if (input.match("11")) ACTION_DO_Y(0); - if (input.match(" *")) ACTION_DO_Y(x); - if (input.match("* ")) ACTION_DO_Y(x); + if (consume_x) { + if (input.match(" *")) ACTION_DO_Y(0); + if (input.match("* ")) ACTION_DO_Y(0); + } } if (cell->type == ID($_MUX_)) { @@ -1088,7 +1173,7 @@ skip_fine_alu: goto next_cell; } - if (!keepdc) + if (consume_x) { bool identity_wrt_a = false; bool identity_wrt_b = false; @@ -1980,11 +2065,12 @@ struct OptExprPass : public Pass { do { do { did_something = false; - replace_const_cells(design, module, false, mux_undef, mux_bool, do_fine, keepdc, clkinv); + replace_const_cells(design, module, false /* consume_x */, mux_undef, mux_bool, do_fine, keepdc, clkinv); if (did_something) design->scratchpad_set_bool("opt.did_something", true); } while (did_something); - replace_const_cells(design, module, true, mux_undef, mux_bool, do_fine, keepdc, clkinv); + if (!keepdc) + replace_const_cells(design, module, true /* consume_x */, mux_undef, mux_bool, do_fine, keepdc, clkinv); if (did_something) design->scratchpad_set_bool("opt.did_something", true); } while (did_something); diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index d99ca1b53..c42760488 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -19,22 +19,12 @@ #include "kernel/yosys.h" #include "kernel/celltypes.h" +#include "kernel/consteval.h" #include "kernel/log.h" #include "kernel/rtlil.h" #include "kernel/register.h" -#include <cstdio> #include <algorithm> -#if defined(_WIN32) -# define WIFEXITED(x) 1 -# define WIFSIGNALED(x) 0 -# define WIFSTOPPED(x) 0 -# define WEXITSTATUS(x) ((x) & 0xff) -# define WTERMSIG(x) SIGTERM -#else -# include <sys/wait.h> -#endif - USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -43,13 +33,13 @@ struct QbfSolutionType { dict<std::string, std::string> hole_to_value; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' - bool success; //true if exit code 0 - QbfSolutionType() : sat(false), unknown(true), success(false) {} + QbfSolutionType() : sat(false), unknown(true) {} }; 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; std::string specialize_soln_file; std::string write_soln_soln_file; @@ -57,12 +47,14 @@ struct QbfSolveOptions { size_t argidx; QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false), nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false), - sat(false), unsat(false), show_smtbmc(false), argidx(0) {}; + nooptimize(false), nobisection(false), sat(false), unsat(false), show_smtbmc(false), + argidx(0) {}; }; 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 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 YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+"); @@ -86,6 +78,10 @@ void recover_solution(QbfSolutionType &sol) { sat_regex_found = true; else if (YS_REGEX_NS::regex_search(x, unsat_regex)) unsat_regex_found = true; + else if (YS_REGEX_NS::regex_search(x, memout_regex)) { + sol.unknown = true; + log_warning("solver ran out of memory\n"); + } } #ifndef NDEBUG log_assert(!sol.unknown && sol.sat? sat_regex_found : true); @@ -107,6 +103,40 @@ dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, cons return hole_loc_to_name; } +pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { + bool found_input = false; + bool found_hole = false; + bool found_1bit_output = false; + bool found_assert_assume = false; + pool<std::string> input_wires; + for (auto wire : module->wires()) { + if (wire->port_input) { + found_input = true; + input_wires.insert(wire->name.str()); + } + if (wire->port_output && wire->width == 1) + found_1bit_output = true; + } + for (auto cell : module->cells()) { + if (cell->type == "$allconst") + found_input = true; + if (cell->type == "$anyconst") + found_hole = true; + if (cell->type.in("$assert", "$assume")) + found_assert_assume = true; + } + if (!found_input) + log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); + if (!found_hole) + log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); + if (!found_1bit_output && !found_assert_assume) + log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); + if (!found_assert_assume && !opt.assume_outputs) + log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); + + return input_wires; +} + void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) { std::ofstream fout(file.c_str()); if (!fout) @@ -164,7 +194,7 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { } } -void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { +void specialize(RTLIL::Module *module, const QbfSolutionType &sol, bool quiet = false) { dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol); pool<RTLIL::Cell *> anyconsts_to_remove; for (auto cell : module->cells()) @@ -189,7 +219,8 @@ void specialize(RTLIL::Module *module, const QbfSolutionType &sol) { log_assert(wire->width > 0 && GetSize(hole_value) == wire->width); #endif - log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); + if (!quiet) + log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str()); std::vector<RTLIL::SigBit> value_bv; value_bv.reserve(wire->width); for (char c : hole_value) @@ -219,7 +250,6 @@ void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) { value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0); std::reverse(value_bv.begin(), value_bv.end()); } - } void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) { @@ -280,84 +310,153 @@ void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) { module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1); } -QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { +QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, const std::string &tempdir_name, const bool quiet = false, const int iter_num = 0) { + //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` 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 tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); - const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2"; -#ifndef NDEBUG - log_assert(mod->design != nullptr); -#endif Pass::call(mod->design, smt2_command); - log_header(mod->design, "Solving QBF-SAT problem.\n"); - //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]` - { - const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1"; - auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](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) - log("smtbmc output: %s", line.c_str()); - }; - - log("Launching \"%s\".\n", cmd.c_str()); - int retval = run_command(cmd, process_line); - if (retval == 0) { - ret.sat = true; - ret.unknown = false; - } else if (retval == 1) { - ret.sat = false; - ret.unknown = false; - } + auto process_line = [&ret, &smtbmc_warning, &show_smtbmc, &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) + 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; } - if(!opt.nocleanup) - remove_directory(tempdir_name); - recover_solution(ret); - return ret; } -pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) { - bool found_input = false; - bool found_hole = false; - bool found_1bit_output = false; - bool found_assert_assume = false; - pool<std::string> input_wires; - for (auto wire : module->wires()) { - if (wire->port_input) { - found_input = true; - input_wires.insert(wire->name.str()); - } - if (wire->port_output && wire->width == 1) - found_1bit_output = true; +QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) { + QbfSolutionType ret, best_soln; + const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX"); + 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; + bool maximize = false; + log_assert(module->design != nullptr); + + Pass::call(design, "design -push-copy"); + + //Replace input wires with wires assigned $allconst cells: + pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); + allconstify_inputs(module, input_wires); + if (opt.assume_outputs) + 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 cell : module->cells()) { - if (cell->type == "$allconst") - found_input = true; - if (cell->type == "$anyconst") - found_hole = true; - if (cell->type.in("$assert", "$assume")) - found_assert_assume = true; + + if (opt.nobisection || opt.nooptimize) { + if (wire_to_optimize != nullptr && opt.nooptimize) { + wire_to_optimize->set_bool_attribute("\\maximize", false); + wire_to_optimize->set_bool_attribute("\\minimize", false); + } + ret = call_qbf_solver(module, opt, tempdir_name, false, 0); + } else { + //Do the iterated bisection method: + unsigned int iter_num = 1; + unsigned int success = 0; + 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)); + + //If maximizing, grow until we get a failure. Then bisect success and failure. + while (failure == 0 || success - failure > 1) { + Pass::call(design, "design -push-copy"); + log_header(design, "Preparing QBF-SAT problem.\n"); + + if (cur_thresh != 0) { + //Add thresholding logic (but not on the initial run when we don't have a sense of where to start): + RTLIL::SigSpec comparator = maximize? module->Ge(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false) + : module->Le(NEW_ID, module->wire(wire_to_optimize_name), RTLIL::Const(cur_thresh), false); + + module->addAssume(wire_to_optimize_name.str() + "__threshold", comparator, RTLIL::Const(1, 1)); + log("Trying to solve with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), cur_thresh); + } + + ret = call_qbf_solver(module, opt, tempdir_name, false, iter_num); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + if (!ret.unknown && ret.sat) { + Pass::call(design, "design -push-copy"); + specialize(module, ret, true); + + RTLIL::SigSpec wire, value, undef; + RTLIL::SigSpec::parse_sel(wire, design, module, wire_to_optimize_name.str()); + + ConstEval ce(module); + value = wire; + if (!ce.eval(value, undef)) + log_cmd_error("Failed to evaluate signal %s: Missing value for %s.\n", log_signal(wire), log_signal(undef)); + log_assert(value.is_fully_const()); + success = value.as_const().as_int(); + best_soln = ret; + log("Problem is satisfiable with %s = %d.\n", wire_to_optimize_name.c_str(), success); + Pass::call(design, "design -pop"); + module = design->module(module_name); + + //sometimes this happens if we get an 'unknown' or timeout + if (!maximize && success < failure) + break; + else if (maximize && success > failure) + break; + } else { + //Treat 'unknown' as UNSAT + failure = cur_thresh; + if (failure == 0) { + log("Problem is NOT satisfiable.\n"); + break; + } + else + log("Problem is NOT satisfiable with %s %s %d.\n", wire_to_optimize_name.c_str(), (maximize? ">=" : "<="), failure); + } + + iter_num++; + cur_thresh = (maximize && failure == 0)? 2 * success //growth + : (success + failure) / 2; //bisection + } + if (success != 0 || failure != 0) { + log("Wire %s is %s at %d.\n", wire_to_optimize_name.c_str(), (maximize? "maximized" : "minimized"), success); + ret = best_soln; + } } - if (!found_input) - log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); - if (!found_hole) - log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); - if (!found_1bit_output && !found_assert_assume) - log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n"); - if (!found_assert_assume && !opt.assume_outputs) - log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n"); - return input_wires; + if(!opt.nocleanup) + remove_directory(tempdir_name); + + Pass::call(design, "design -pop"); + + return ret; } QbfSolveOptions parse_args(const std::vector<std::string> &args) { @@ -379,6 +478,14 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) { opt.assume_neg = true; continue; } + else if (args[opt.argidx] == "-nooptimize") { + opt.nooptimize = true; + continue; + } + else if (args[opt.argidx] == "-nobisection") { + opt.nobisection = true; + continue; + } else if (args[opt.argidx] == "-sat") { opt.sat = true; continue; @@ -477,6 +584,17 @@ struct QbfSatPass : public Pass { log(" negative polarity signals and should always be low, for example like the\n"); log(" miters created with the `miter` command.\n"); 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("\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(" quantified bitvector problems.\n"); + log("\n"); log(" -sat\n"); log(" Generate an error if the solver does not return \"sat\".\n"); log("\n"); @@ -519,26 +637,16 @@ struct QbfSatPass : public Pass { if (!opt.specialize_from_file) { //Save the design to restore after modiyfing the current module. std::string module_name = module->name.str(); - Pass::call(design, "design -push-copy"); - - //Replace input wires with wires assigned $allconst cells. - pool<std::string> input_wires = validate_design_and_get_inputs(module, opt); - allconstify_inputs(module, input_wires); - if (opt.assume_outputs) - assume_miter_outputs(module, opt); QbfSolutionType ret = qbf_solve(module, opt); - Pass::call(design, "design -pop"); module = design->module(module_name); - - if (ret.unknown) + if (ret.unknown) { log_warning("solver did not give an answer\n"); - else if (ret.sat) + if (opt.sat || opt.unsat) + log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + } + else if (ret.sat) { print_qed(); - else - print_proof_failed(); - - if(!ret.unknown && ret.sat) { if (opt.write_solution) { write_solution(module, ret, opt.write_soln_soln_file); } @@ -550,10 +658,11 @@ struct QbfSatPass : public Pass { if (opt.unsat) log_cmd_error("expected problem to be UNSAT\n"); } - else if (!ret.unknown && !ret.sat && opt.sat) - log_cmd_error("expected problem to be SAT\n"); - else if (ret.unknown && (opt.sat || opt.unsat)) - log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); + else { + print_proof_failed(); + if (opt.sat) + log_cmd_error("expected problem to be SAT\n"); + } } else specialize_from_file(module, opt.specialize_soln_file); log_pop(); diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 1b3d5ff06..06097a6f7 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -151,8 +151,8 @@ struct Abc9Pass : public ScriptPass log(" specified).\n"); log("\n"); log(" -dff\n"); - log(" also pass $_ABC9_FF_ cells through to ABC. modules with many clock\n"); - log(" domains are marked as such and automatically partitioned by ABC.\n"); + log(" also pass $_DFF_[NP]_ cells through to ABC. modules with many clock\n"); + log(" domains are supported and automatically partitioned by ABC.\n"); log("\n"); log(" -nocleanup\n"); log(" when this option is used, the temporary files created by this pass\n"); @@ -274,40 +274,106 @@ struct Abc9Pass : public ScriptPass void script() YS_OVERRIDE { + if (check_label("check")) { + if (help_mode) + run("abc9_ops -check [-dff]", "(option if -dff)"); + else + run(stringf("abc9_ops -check %s", dff_mode ? "-dff" : "")); + } + + if (check_label("map")) { + if (help_mode) + run("abc9_ops -prep_hier -prep_bypass [-prep_dff -dff]", "(option if -dff)"); + else + run(stringf("abc9_ops -prep_hier -prep_bypass %s", dff_mode ? "-prep_dff -dff" : "")); + if (dff_mode) { + run("design -copy-to $abc9_map @$abc9_flops", "(only if -dff)"); + run("select -unset $abc9_flops", " (only if -dff)"); + } + run("design -stash $abc9"); + run("design -load $abc9_map"); + run("proc"); + run("wbflip"); + run("techmap"); + run("opt"); + if (dff_mode || help_mode) { + if (!help_mode) + active_design->scratchpad_unset("abc9_ops.prep_dff_submod.did_something"); + run("abc9_ops -prep_dff_submod", " (only if -dff)"); // rewrite specify + bool did_something = help_mode || active_design->scratchpad_get_bool("abc9_ops.prep_dff_submod.did_something"); + if (did_something) { + // select all $_DFF_[NP]_ + // then select all its fanins + // then select all fanouts of all that + // lastly remove $_DFF_[NP]_ cells + run("setattr -set submod \"$abc9_flop\" t:$_DFF_?_ %ci* %co* t:$_DFF_?_ %d", " (only if -dff)"); + run("submod", " (only if -dff)"); + run("setattr -mod -set whitebox 1 -set abc9_flop 1 -set abc9_box 1 *_$abc9_flop", "(only if -dff)"); + if (help_mode) { + run("foreach module in design"); + run(" rename <module-name>_$abc9_flop _TECHMAP_REPLACE_", " (only if -dff)"); + } + else { + // Rename all submod-s to _TECHMAP_REPLACE_ to inherit name + attrs + for (auto module : active_design->selected_modules()) { + active_design->selected_active_module = module->name.str(); + if (module->cell(stringf("%s_$abc9_flop", module->name.c_str()))) + run(stringf("rename %s_$abc9_flop _TECHMAP_REPLACE_", module->name.c_str())); + } + active_design->selected_active_module.clear(); + } + run("abc9_ops -prep_dff_unmap", " (only if -dff)"); + run("design -copy-to $abc9 =*_$abc9_flop", " (only if -dff)"); // copy submod out + run("delete =*_$abc9_flop", " (only if -dff)"); + } + } + run("design -stash $abc9_map"); + run("design -load $abc9"); + run("design -delete $abc9"); + if (help_mode) + run("techmap -wb -max_iter 1 -map %$abc9_map -map +/abc9_map.v [-D DFF]", "(option if -dff)"); + else + run(stringf("techmap -wb -max_iter 1 -map %%$abc9_map -map +/abc9_map.v %s", dff_mode ? "-D DFF" : "")); + run("design -delete $abc9_map"); + } + if (check_label("pre")) { - run("abc9_ops -check"); + run("read_verilog -icells -lib -specify +/abc9_model.v"); run("scc -set_attr abc9_scc_id {}"); if (help_mode) run("abc9_ops -mark_scc -prep_delays -prep_xaiger [-dff]", "(option for -dff)"); else - run("abc9_ops -mark_scc -prep_delays -prep_xaiger" + std::string(dff_mode ? " -dff" : ""), "(option for -dff)"); + run("abc9_ops -mark_scc -prep_delays -prep_xaiger" + std::string(dff_mode ? " -dff" : "")); if (help_mode) run("abc9_ops -prep_lut <maxlut>", "(skip if -lut or -luts)"); else if (!lut_mode) run(stringf("abc9_ops -prep_lut %d", maxlut)); if (help_mode) - run("abc9_ops -prep_box [-dff]", "(skip if -box)"); + run("abc9_ops -prep_box", "(skip if -box)"); else if (box_file.empty()) - run(stringf("abc9_ops -prep_box %s", dff_mode ? "-dff" : "")); - run("select -set abc9_holes A:abc9_holes"); - run("flatten -wb @abc9_holes"); - run("techmap @abc9_holes"); - if (dff_mode || help_mode) - run("abc9_ops -prep_dff", "(only if -dff)"); - run("opt -purge @abc9_holes"); - run("aigmap"); - run("wbflip @abc9_holes"); + run("abc9_ops -prep_box"); + if (saved_designs.count("$abc9_holes") || help_mode) { + run("design -stash $abc9"); + run("design -load $abc9_holes"); + run("techmap -wb -map %$abc9 -map +/techmap.v"); + run("opt -purge"); + run("aigmap"); + run("design -stash $abc9_holes"); + run("design -load $abc9"); + run("design -delete $abc9"); + } } - if (check_label("map")) { + if (check_label("exe")) { + run("aigmap"); if (help_mode) { run("foreach module in selection"); run(" abc9_ops -write_lut <abc-temp-dir>/input.lut", "(skip if '-lut' or '-luts')"); - run(" abc9_ops -write_box <abc-temp-dir>/input.box"); - run(" write_xaiger -map <abc-temp-dir>/input.sym <abc-temp-dir>/input.xaig"); - run(" abc9_exe [options] -cwd <abc-temp-dir> [-lut <abc-temp-dir>/input.lut] -box <abc-temp-dir>/input.box"); + run(" abc9_ops -write_box <abc-temp-dir>/input.box", "(skip if '-box')"); + run(" write_xaiger -map <abc-temp-dir>/input.sym [-dff] <abc-temp-dir>/input.xaig"); + run(" abc9_exe [options] -cwd <abc-temp-dir> -lut [<abc-temp-dir>/input.lut] -box [<abc-temp-dir>/input.box]"); run(" read_aiger -xaiger -wideports -module_name <module-name>$abc9 -map <abc-temp-dir>/input.sym <abc-temp-dir>/output.aig"); - run(" abc9_ops -reintegrate"); + run(" abc9_ops -reintegrate [-dff]"); } else { auto selected_modules = active_design->selected_modules(); @@ -318,7 +384,6 @@ struct Abc9Pass : public ScriptPass log("Skipping module %s as it contains processes.\n", log_id(mod)); continue; } - log_assert(!mod->attributes.count(ID::abc9_box_id)); log_push(); active_design->selection().select(mod); @@ -333,8 +398,9 @@ struct Abc9Pass : public ScriptPass if (!lut_mode) run_nocheck(stringf("abc9_ops -write_lut %s/input.lut", tempdir_name.c_str())); - run_nocheck(stringf("abc9_ops -write_box %s/input.box", tempdir_name.c_str())); - run_nocheck(stringf("write_xaiger -map %s/input.sym %s/input.xaig", tempdir_name.c_str(), tempdir_name.c_str())); + if (box_file.empty()) + run_nocheck(stringf("abc9_ops -write_box %s/input.box", tempdir_name.c_str())); + run_nocheck(stringf("write_xaiger -map %s/input.sym %s %s/input.xaig", tempdir_name.c_str(), dff_mode ? "-dff" : "", tempdir_name.c_str())); int num_outputs = active_design->scratchpad_get_int("write_xaiger.num_outputs"); @@ -349,10 +415,13 @@ struct Abc9Pass : public ScriptPass abc9_exe_cmd += stringf("%s -cwd %s", exe_cmd.str().c_str(), tempdir_name.c_str()); if (!lut_mode) abc9_exe_cmd += stringf(" -lut %s/input.lut", tempdir_name.c_str()); - abc9_exe_cmd += stringf(" -box %s/input.box", tempdir_name.c_str()); + if (box_file.empty()) + abc9_exe_cmd += stringf(" -box %s/input.box", tempdir_name.c_str()); + else + abc9_exe_cmd += stringf(" -box %s", box_file.c_str()); run_nocheck(abc9_exe_cmd); run_nocheck(stringf("read_aiger -xaiger -wideports -module_name %s$abc9 -map %s/input.sym %s/output.aig", log_id(mod), tempdir_name.c_str(), tempdir_name.c_str())); - run_nocheck("abc9_ops -reintegrate"); + run_nocheck(stringf("abc9_ops -reintegrate %s", dff_mode ? "-dff" : "")); } else log("Don't call ABC as there is nothing to map.\n"); @@ -369,6 +438,14 @@ struct Abc9Pass : public ScriptPass active_design->selection_stack.pop_back(); } } + + if (check_label("unmap")) { + run("techmap -wb -map %$abc9_unmap -map +/abc9_unmap.v"); // techmap user design from submod back to original cell + // ($_DFF_[NP]_ already shorted by -reintegrate) + run("design -delete $abc9_unmap"); + if (saved_designs.count("$abc9_holes") || help_mode) + run("design -delete $abc9_holes"); + } } } Abc9Pass; diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc index 1345188a4..8d55b18a0 100644 --- a/passes/techmap/abc9_ops.cc +++ b/passes/techmap/abc9_ops.cc @@ -34,13 +34,10 @@ inline std::string remap_name(RTLIL::IdString abc9_name) return stringf("$abc$%d$%s", map_autoidx, abc9_name.c_str()+1); } -void check(RTLIL::Design *design) +void check(RTLIL::Design *design, bool dff_mode) { dict<IdString,IdString> box_lookup; for (auto m : design->modules()) { - if (m->name.begins_with("$paramod")) - continue; - auto flop = m->get_bool_attribute(ID::abc9_flop); auto it = m->attributes.find(ID::abc9_box_id); if (!flop) { @@ -88,6 +85,461 @@ void check(RTLIL::Design *design) log_error("Module '%s' with (* abc9_flop *) has %d outputs (expect 1).\n", log_id(m), num_outputs); } } + + if (dff_mode) { + static pool<IdString> unsupported{ + ID($adff), ID($dlatch), ID($dlatchsr), ID($sr), + ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), + ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_), + ID($_DLATCH_N_), ID($_DLATCH_P_), + ID($_DLATCHSR_NNN_), ID($_DLATCHSR_NNP_), ID($_DLATCHSR_NPN_), ID($_DLATCHSR_NPP_), + ID($_DLATCHSR_PNN_), ID($_DLATCHSR_PNP_), ID($_DLATCHSR_PPN_), ID($_DLATCHSR_PPP_), + ID($_SR_NN_), ID($_SR_NP_), ID($_SR_PN_), ID($_SR_PP_) + }; + pool<IdString> processed; + for (auto module : design->selected_modules()) + for (auto cell : module->cells()) { + auto inst_module = design->module(cell->type); + if (!inst_module) + continue; + if (!inst_module->get_blackbox_attribute()) + continue; + IdString derived_type; + Module *derived_module; + if (cell->parameters.empty()) { + derived_type = cell->type; + derived_module = inst_module; + } + else { + derived_type = inst_module->derive(design, cell->parameters); + derived_module = design->module(derived_type); + log_assert(derived_module); + } + if (!derived_module->get_bool_attribute(ID::abc9_flop)) + continue; + if (derived_module->get_blackbox_attribute(true /* ignore_wb */)) + log_error("Module '%s' with (* abc9_flop *) is a blackbox.\n", log_id(derived_type)); + + if (derived_module->has_processes()) + Pass::call_on_module(design, derived_module, "proc"); + + bool found = false; + for (auto derived_cell : derived_module->cells()) { + if (derived_cell->type.in(ID($dff), ID($_DFF_N_), ID($_DFF_P_))) { + if (found) + log_error("Module '%s' with (* abc9_flop *) contains more than one $_DFF_[NP]_ cell.\n", log_id(derived_module)); + found = true; + + SigBit Q = derived_cell->getPort(ID::Q); + log_assert(GetSize(Q.wire) == 1); + + if (!Q.wire->port_output) + log_error("Module '%s' contains a %s cell where its 'Q' port does not drive a module output!\n", log_id(derived_module), log_id(derived_cell->type)); + + Const init = Q.wire->attributes.at(ID::init, State::Sx); + log_assert(GetSize(init) == 1); + } + else if (unsupported.count(derived_cell->type)) + log_error("Module '%s' with (* abc9_flop *) contains a %s cell, which is not supported for sequential synthesis.\n", log_id(derived_module), log_id(derived_cell->type)); + } + } + } +} + +void prep_hier(RTLIL::Design *design, bool dff_mode) +{ + auto r = saved_designs.emplace("$abc9_unmap", nullptr); + if (r.second) + r.first->second = new Design; + Design *unmap_design = r.first->second; + + static const pool<IdString> seq_types{ + ID($dff), ID($dffsr), ID($adff), + ID($dlatch), ID($dlatchsr), ID($sr), + ID($mem), + ID($_DFF_N_), ID($_DFF_P_), + ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_), + ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_), + ID($_DFF_N_), ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), + ID($_DFF_P_), ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_), + ID($_DLATCH_N_), ID($_DLATCH_P_), + ID($_DLATCHSR_NNN_), ID($_DLATCHSR_NNP_), ID($_DLATCHSR_NPN_), ID($_DLATCHSR_NPP_), + ID($_DLATCHSR_PNN_), ID($_DLATCHSR_PNP_), ID($_DLATCHSR_PPN_), ID($_DLATCHSR_PPP_), + ID($_SR_NN_), ID($_SR_NP_), ID($_SR_PN_), ID($_SR_PP_) + }; + + for (auto module : design->selected_modules()) + for (auto cell : module->cells()) { + auto inst_module = design->module(cell->type); + if (!inst_module) + continue; + if (!inst_module->get_blackbox_attribute()) + continue; + IdString derived_type; + Module *derived_module; + if (cell->parameters.empty()) { + derived_type = cell->type; + derived_module = inst_module; + } + else { + derived_type = inst_module->derive(design, cell->parameters); + derived_module = design->module(derived_type); + } + if (derived_module->get_blackbox_attribute(true /* ignore_wb */)) + continue; + + if (derived_module->get_bool_attribute(ID::abc9_flop)) { + if (!dff_mode) + continue; + } + else { + if (!derived_module->get_bool_attribute(ID::abc9_box) && !derived_module->get_bool_attribute(ID::abc9_bypass)) + continue; + } + + if (!unmap_design->module(derived_type)) { + if (derived_module->has_processes()) + Pass::call_on_module(design, derived_module, "proc"); + + if (derived_module->get_bool_attribute(ID::abc9_flop)) { + for (auto derived_cell : derived_module->cells()) + if (derived_cell->type.in(ID($dff), ID($_DFF_N_), ID($_DFF_P_))) { + SigBit Q = derived_cell->getPort(ID::Q); + Const init = Q.wire->attributes.at(ID::init, State::Sx); + log_assert(GetSize(init) == 1); + + // Block sequential synthesis on cells with (* init *) != 1'b0 + // because ABC9 doesn't support them + if (init != State::S0) { + log_warning("Module '%s' contains a %s cell with non-zero initial state -- this is not unsupported for ABC9 sequential synthesis. Treating as a blackbox.\n", log_id(derived_module), log_id(derived_cell->type)); + derived_module->set_bool_attribute(ID::abc9_flop, false); + } + break; + } + } + else if (derived_module->get_bool_attribute(ID::abc9_box)) { + for (auto derived_cell : derived_module->cells()) + if (seq_types.count(derived_cell->type)) { + derived_module->set_bool_attribute(ID::abc9_box, false); + derived_module->set_bool_attribute(ID::abc9_bypass); + break; + } + } + + if (derived_type != cell->type) { + auto unmap_module = unmap_design->addModule(derived_type); + for (auto port : derived_module->ports) { + auto w = unmap_module->addWire(port, derived_module->wire(port)); + // Do not propagate (* init *) values into the box, + // in fact, remove it from outside too + if (w->port_output && w->attributes.erase(ID::init)) { + auto r = unmap_module->addWire(stringf("\\_TECHMAP_REMOVEINIT_%s_", log_id(port))); + unmap_module->connect(r, State::S1); + } + } + unmap_module->ports = derived_module->ports; + unmap_module->check(); + + auto replace_cell = unmap_module->addCell(ID::_TECHMAP_REPLACE_, cell->type); + for (const auto &conn : cell->connections()) { + auto w = unmap_module->wire(conn.first); + log_assert(w); + replace_cell->setPort(conn.first, w); + } + replace_cell->parameters = cell->parameters; + } + } + + cell->type = derived_type; + cell->parameters.clear(); + } +} + +void prep_bypass(RTLIL::Design *design) +{ + auto r = saved_designs.emplace("$abc9_map", nullptr); + if (r.second) + r.first->second = new Design; + Design *map_design = r.first->second; + + r = saved_designs.emplace("$abc9_unmap", nullptr); + if (r.second) + r.first->second = new Design; + Design *unmap_design = r.first->second; + + pool<IdString> processed; + for (auto module : design->selected_modules()) + for (auto cell : module->cells()) { + if (!processed.insert(cell->type).second) + continue; + auto inst_module = design->module(cell->type); + if (!inst_module) + continue; + if (!inst_module->get_bool_attribute(ID::abc9_bypass)) + continue; + log_assert(!inst_module->get_blackbox_attribute(true /* ignore_wb */)); + log_assert(cell->parameters.empty()); + + + // The idea is to create two techmap designs, one which maps: + // + // box u0 (.i(i), .o(o)); + // + // to + // + // wire $abc9$o; + // box u0 (.i(i), .o($abc9_byp$o)); + // box_$abc9_byp (.i(i), .$abc9_byp$o($abc9_byp$o), .o(o)); + // + // the purpose being to move the (* abc9_box *) status from 'box' + // (which is stateful) to 'box_$abc9_byp' (which becomes a new + // combinatorial black- (not white-) box with all state elements + // removed). This has the effect of preserving any combinatorial + // paths through an otherwise sequential primitive -- e.g. LUTRAMs. + // + // The unmap design performs the reverse: + // + // wire $abc9$o; + // box u0 (.i(i), .o($abc9_byp$o)); + // box_$abc9_byp (.i(i), .$abc9_byp$o($abc9_byp$o), .o(o)); + // + // to: + // + // wire $abc9$o; + // box u0 (.i(i), .o($abc9_byp$o)); + // assign o = $abc9_byp$o; + + + // Copy inst_module into map_design, with the same interface + // and duplicate $abc9$* wires for its output ports + auto map_module = map_design->addModule(cell->type); + for (auto port_name : inst_module->ports) { + auto w = map_module->addWire(port_name, inst_module->wire(port_name)); + if (w->port_output) + w->attributes.erase(ID::init); + } + map_module->ports = inst_module->ports; + map_module->check(); + map_module->set_bool_attribute(ID::whitebox); + + // Create the bypass module in the user design, which has the same + // interface as the derived module but with additional input + // ports driven by the outputs of the replaced cell + auto bypass_module = design->addModule(cell->type.str() + "_$abc9_byp"); + for (auto port_name : inst_module->ports) { + auto port = inst_module->wire(port_name); + if (!port->port_output) + continue; + auto dst = bypass_module->addWire(port_name, port); + auto src = bypass_module->addWire("$abc9byp$" + port_name.str(), GetSize(port)); + src->port_input = true; + // For these new input ports driven by the replaced + // cell, then create a new simple-path specify entry: + // (input => output) = 0 + auto specify = bypass_module->addCell(NEW_ID, ID($specify2)); + specify->setPort(ID::EN, State::S1); + specify->setPort(ID::SRC, src); + specify->setPort(ID::DST, dst); + specify->setParam(ID::FULL, 0); + specify->setParam(ID::SRC_WIDTH, GetSize(src)); + specify->setParam(ID::DST_WIDTH, GetSize(dst)); + specify->setParam(ID::SRC_DST_PEN, 0); + specify->setParam(ID::SRC_DST_POL, 0); + specify->setParam(ID::T_RISE_MIN, 0); + specify->setParam(ID::T_RISE_TYP, 0); + specify->setParam(ID::T_RISE_MAX, 0); + specify->setParam(ID::T_FALL_MIN, 0); + specify->setParam(ID::T_FALL_TYP, 0); + specify->setParam(ID::T_FALL_MAX, 0); + } + bypass_module->set_bool_attribute(ID::blackbox); + bypass_module->set_bool_attribute(ID::abc9_box); + + // Copy any 'simple' (combinatorial) specify paths from + // the derived module into the bypass module, if EN + // is not false and SRC/DST are driven only by + // module ports; create new input port if one doesn't + // already exist + for (auto cell : inst_module->cells()) { + if (cell->type != ID($specify2)) + continue; + auto EN = cell->getPort(ID::EN).as_bit(); + SigBit newEN; + if (!EN.wire && EN != State::S1) + continue; + auto SRC = cell->getPort(ID::SRC); + for (const auto &c : SRC.chunks()) + if (c.wire && !c.wire->port_input) { + SRC = SigSpec(); + break; + } + if (SRC.empty()) + continue; + auto DST = cell->getPort(ID::DST); + for (const auto &c : DST.chunks()) + if (c.wire && !c.wire->port_output) { + DST = SigSpec(); + break; + } + if (DST.empty()) + continue; + auto rw = [bypass_module](RTLIL::SigSpec &sig) + { + SigSpec new_sig; + for (auto c : sig.chunks()) { + if (c.wire) { + auto port = bypass_module->wire(c.wire->name); + if (!port) + port = bypass_module->addWire(c.wire->name, c.wire); + c.wire = port; + } + new_sig.append(std::move(c)); + } + sig = std::move(new_sig); + }; + auto specify = bypass_module->addCell(NEW_ID, cell); + specify->rewrite_sigspecs(rw); + } + bypass_module->fixup_ports(); + + // Create an _TECHMAP_REPLACE_ cell identical to the original cell, + // and a bypass cell that has the same inputs/outputs as the + // original cell, but with additional inputs taken from the + // replaced cell + auto replace_cell = map_module->addCell(ID::_TECHMAP_REPLACE_, cell->type); + auto bypass_cell = map_module->addCell(NEW_ID, cell->type.str() + "_$abc9_byp"); + for (const auto &conn : cell->connections()) { + auto port = map_module->wire(conn.first); + if (cell->input(conn.first)) { + replace_cell->setPort(conn.first, port); + if (bypass_module->wire(conn.first)) + bypass_cell->setPort(conn.first, port); + } + if (cell->output(conn.first)) { + bypass_cell->setPort(conn.first, port); + auto n = "$abc9byp$" + conn.first.str(); + auto w = map_module->addWire(n, GetSize(conn.second)); + replace_cell->setPort(conn.first, w); + bypass_cell->setPort(n, w); + } + } + + + // Lastly, create a new module in the unmap_design that shorts + // out the bypass cell back to leave the replace cell behind + // driving the outputs + auto unmap_module = unmap_design->addModule(cell->type.str() + "_$abc9_byp"); + for (auto port_name : inst_module->ports) { + auto w = unmap_module->addWire(port_name, inst_module->wire(port_name)); + if (w->port_output) { + w->attributes.erase(ID::init); + auto w2 = unmap_module->addWire("$abc9byp$" + port_name.str(), GetSize(w)); + w2->port_input = true; + unmap_module->connect(w, w2); + } + } + unmap_module->fixup_ports(); + } +} + +void prep_dff(RTLIL::Design *design) +{ + auto r = design->selection_vars.insert(std::make_pair(ID($abc9_flops), RTLIL::Selection(false))); + auto &modules_sel = r.first->second; + + for (auto module : design->selected_modules()) + for (auto cell : module->cells()) { + if (modules_sel.selected_whole_module(cell->type)) + continue; + auto inst_module = design->module(cell->type); + if (!inst_module) + continue; + if (!inst_module->get_bool_attribute(ID::abc9_flop)) + continue; + log_assert(!inst_module->get_blackbox_attribute(true /* ignore_wb */)); + log_assert(cell->parameters.empty()); + modules_sel.select(inst_module); + } +} + +void prep_dff_submod(RTLIL::Design *design) +{ + for (auto module : design->modules()) { + vector<Cell*> specify_cells; + SigBit Q; + Cell* dff_cell = nullptr; + + if (!module->get_bool_attribute(ID::abc9_flop)) + continue; + + for (auto cell : module->cells()) + if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_))) { + log_assert(!dff_cell); + dff_cell = cell; + Q = cell->getPort(ID::Q); + log_assert(GetSize(Q.wire) == 1); + } + else if (cell->type.in(ID($specify3), ID($specrule))) + specify_cells.emplace_back(cell); + log_assert(dff_cell); + + // Add an always-enabled CE mux that drives $_DFF_[NP]_.D so that: + // (a) flop box will have an output + // (b) $_DFF_[NP]_.Q will be present as an input + SigBit D = module->addWire(NEW_ID); + module->addMuxGate(NEW_ID, dff_cell->getPort(ID::D), Q, State::S0, D); + dff_cell->setPort(ID::D, D); + + // Rewrite $specify cells that end with $_DFF_[NP]_.Q + // to $_DFF_[NP]_.D since it will be moved into + // the submodule + for (auto cell : specify_cells) { + auto DST = cell->getPort(ID::DST); + DST.replace(Q, D); + cell->setPort(ID::DST, DST); + } + + design->scratchpad_set_bool("abc9_ops.prep_dff_submod.did_something", true); + } +} + +void prep_dff_unmap(RTLIL::Design *design) +{ + Design *unmap_design = saved_designs.at("$abc9_unmap"); + + for (auto module : design->modules()) { + if (!module->get_bool_attribute(ID::abc9_flop) || module->get_bool_attribute(ID::abc9_box)) + continue; + + // Make sure the box module has all the same ports present on flop cell + auto replace_cell = module->cell(ID::_TECHMAP_REPLACE_); + log_assert(replace_cell); + auto box_module = design->module(module->name.str() + "_$abc9_flop"); + log_assert(box_module); + for (auto port_name : module->ports) { + auto port = module->wire(port_name); + auto box_port = box_module->wire(port_name); + if (box_port) { + // Do not propagate init -- already captured by box + box_port->attributes.erase(ID::init); + continue; + } + log_assert(port->port_input); + box_module->addWire(port_name, port); + replace_cell->setPort(port_name, port); + } + box_module->fixup_ports(); + + auto unmap_module = unmap_design->addModule(box_module->name); + replace_cell = unmap_module->addCell(ID::_TECHMAP_REPLACE_, module->name); + for (auto port_name : box_module->ports) { + auto w = unmap_module->addWire(port_name, box_module->wire(port_name)); + if (module->wire(port_name)) + replace_cell->setPort(port_name, w); + } + unmap_module->ports = box_module->ports; + unmap_module->check(); + } } void mark_scc(RTLIL::Module *module) @@ -95,7 +547,7 @@ void mark_scc(RTLIL::Module *module) // For every unique SCC found, (arbitrarily) find the first // cell in the component, and replace its output connections // with a new wire driven by the old connection but with a - // special (* abc9_scc *) attribute set (which is used by + // special (* abc9_keep *) attribute set (which is used by // write_xaiger to break this wire into PI and POs) pool<RTLIL::Const> ids_seen; for (auto cell : module->cells()) { @@ -111,7 +563,7 @@ void mark_scc(RTLIL::Module *module) if (c.second.is_fully_const()) continue; if (cell->output(c.first)) { Wire *w = module->addWire(NEW_ID, GetSize(c.second)); - w->set_bool_attribute(ID::abc9_scc); + w->set_bool_attribute(ID::abc9_keep); module->connect(w, c.second); c.second = w; } @@ -119,80 +571,94 @@ void mark_scc(RTLIL::Module *module) } } -void prep_dff(RTLIL::Module *module) +void prep_delays(RTLIL::Design *design, bool dff_mode) { - auto design = module->design; - log_assert(design); + TimingInfo timing; - SigMap assign_map(module); + // Derive all Yosys blackbox modules that are not combinatorial abc9 boxes + // (e.g. DSPs, RAMs, etc.) nor abc9 flops and collect all such instantiations + std::vector<Cell*> cells; + for (auto module : design->selected_modules()) { + if (module->processes.size() > 0) { + log("Skipping module %s as it contains processes.\n", log_id(module)); + continue; + } - typedef SigSpec clkdomain_t; - dict<clkdomain_t, int> clk_to_mergeability; + for (auto cell : module->cells()) { + if (cell->type.in(ID($_AND_), ID($_NOT_), ID($_DFF_N_), ID($_DFF_P_))) + continue; + log_assert(!cell->type.begins_with("$paramod$__ABC9_DELAY\\DELAY=")); - for (auto cell : module->cells()) { - if (cell->type != ID($__ABC9_FF_)) - continue; + RTLIL::Module* inst_module = design->module(cell->type); + if (!inst_module) + continue; + if (!inst_module->get_blackbox_attribute()) + continue; + if (!cell->parameters.empty()) + continue; - Wire *abc9_clock_wire = module->wire(stringf("%s.clock", cell->name.c_str())); - if (abc9_clock_wire == NULL) - log_error("'%s.clock' is not a wire present in module '%s'.\n", cell->name.c_str(), log_id(module)); - SigSpec abc9_clock = assign_map(abc9_clock_wire); + if (inst_module->get_bool_attribute(ID::abc9_box)) + continue; + if (inst_module->get_bool_attribute(ID::abc9_bypass)) + continue; + + if (dff_mode && inst_module->get_bool_attribute(ID::abc9_flop)) { + continue; // do not add $__ABC9_DELAY boxes to flops + // as delays will be captured in the flop box + } - clkdomain_t key(abc9_clock); + if (!timing.count(cell->type)) + timing.setup_module(inst_module); - auto r = clk_to_mergeability.insert(std::make_pair(abc9_clock, clk_to_mergeability.size() + 1)); - auto r2 = cell->attributes.insert(ID::abc9_mergeability); - log_assert(r2.second); - r2.first->second = r.first->second; + cells.emplace_back(cell); + } } - RTLIL::Module *holes_module = design->module(stringf("%s$holes", module->name.c_str())); - if (holes_module) { - SigMap sigmap(holes_module); + // Insert $__ABC9_DELAY cells on all cells that instantiate blackboxes + // (or bypassed white-boxes with required times) + dict<int, IdString> box_cache; + Module *delay_module = design->module(ID($__ABC9_DELAY)); + log_assert(delay_module); + for (auto cell : cells) { + auto module = cell->module; + auto inst_module = design->module(cell->type); + log_assert(inst_module); - dict<SigSpec, SigSpec> replace; - for (auto cell : holes_module->cells().to_vector()) { - if (!cell->type.in(ID($_DFF_N_), ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_), - ID($_DFF_P_), ID($_DFF_PN0_), ID($_DFF_PN1), ID($_DFF_PP0_), ID($_DFF_PP1_))) + auto &t = timing.at(cell->type).required; + for (auto &conn : cell->connections_) { + auto port_wire = inst_module->wire(conn.first); + if (!port_wire) + log_error("Port %s in cell %s (type %s) from module %s does not actually exist", + log_id(conn.first), log_id(cell), log_id(cell->type), log_id(module)); + if (!port_wire->port_input) continue; - SigBit D = cell->getPort(ID::D); - SigBit Q = cell->getPort(ID::Q); - // Emulate async control embedded inside $_DFF_* cell with mux in front of D - if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_PN0_))) - D = holes_module->MuxGate(NEW_ID, State::S0, D, cell->getPort(ID::R)); - else if (cell->type.in(ID($_DFF_NN1_), ID($_DFF_PN1_))) - D = holes_module->MuxGate(NEW_ID, State::S1, D, cell->getPort(ID::R)); - else if (cell->type.in(ID($_DFF_NP0_), ID($_DFF_PP0_))) - D = holes_module->MuxGate(NEW_ID, D, State::S0, cell->getPort(ID::R)); - else if (cell->type.in(ID($_DFF_NP1_), ID($_DFF_PP1_))) - D = holes_module->MuxGate(NEW_ID, D, State::S1, cell->getPort(ID::R)); - // Remove the $_DFF_* cell from what needs to be a combinatorial box - holes_module->remove(cell); - Wire *port; - if (GetSize(Q.wire) == 1) - port = holes_module->wire(stringf("$abc%s", Q.wire->name.c_str())); - else - port = holes_module->wire(stringf("$abc%s[%d]", Q.wire->name.c_str(), Q.offset)); - log_assert(port); - // Prepare to replace "assign <port> = $_DFF_*.Q;" with "assign <port> = $_DFF_*.D;" - // in order to extract just the combinatorial control logic that feeds the box - // (i.e. clock enable, synchronous reset, etc.) - replace.insert(std::make_pair(Q,D)); - // Since `flatten` above would have created wires named "<cell>.Q", - // extract the pre-techmap cell name - auto pos = Q.wire->name.str().rfind("."); - log_assert(pos != std::string::npos); - IdString driver = Q.wire->name.substr(0, pos); - // And drive the signal that was previously driven by "DFF.Q" (typically - // used to implement clock-enable functionality) with the "<cell>.$abc9_currQ" - // wire (which itself is driven an by input port) we inserted above - Wire *currQ = holes_module->wire(stringf("%s.abc9_ff.Q", driver.c_str())); - log_assert(currQ); - holes_module->connect(Q, currQ); - } + if (conn.second.is_fully_const()) + continue; + + SigSpec O = module->addWire(NEW_ID, GetSize(conn.second)); + for (int i = 0; i < GetSize(conn.second); i++) { + auto d = t.at(TimingInfo::NameBit(conn.first,i), 0); + if (d == 0) + continue; - for (auto &conn : holes_module->connections_) - conn.second = replace.at(sigmap(conn.second), conn.second); +#ifndef NDEBUG + if (ys_debug(1)) { + static std::set<std::tuple<IdString,IdString,int>> seen; + if (seen.emplace(cell->type, conn.first, i).second) log("%s.%s[%d] abc9_required = %d\n", + log_id(cell->type), log_id(conn.first), i, d); + } +#endif + auto r = box_cache.insert(d); + if (r.second) { + r.first->second = delay_module->derive(design, {{ID::DELAY, d}}); + log_assert(r.first->second.begins_with("$paramod$__ABC9_DELAY\\DELAY=")); + } + auto box = module->addCell(NEW_ID, r.first->second); + box->setPort(ID::I, conn.second[i]); + box->setPort(ID::O, O[i]); + conn.second[i] = O[i]; + } + } } } @@ -208,17 +674,17 @@ void prep_xaiger(RTLIL::Module *module, bool dff) dict<IdString, std::vector<IdString>> box_ports; for (auto cell : module->cells()) { - if (cell->type == ID($__ABC9_FF_)) + if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_))) continue; if (cell->has_keep_attr()) continue; - auto inst_module = module->design->module(cell->type); + auto inst_module = design->module(cell->type); bool abc9_flop = inst_module && inst_module->get_bool_attribute(ID::abc9_flop); if (abc9_flop && !dff) continue; - if ((inst_module && inst_module->get_bool_attribute(ID::abc9_box)) || abc9_flop) { + if (inst_module && inst_module->get_bool_attribute(ID::abc9_box)) { auto r = box_ports.insert(cell->type); if (r.second) { // Make carry in the last PI, and carry out the last PO @@ -287,9 +753,13 @@ void prep_xaiger(RTLIL::Module *module, bool dff) log_assert(no_loops); - RTLIL::Module *holes_module = design->addModule(stringf("%s$holes", module->name.c_str())); + auto r = saved_designs.emplace("$abc9_holes", nullptr); + if (r.second) + r.first->second = new Design; + RTLIL::Design *holes_design = r.first->second; + log_assert(holes_design); + RTLIL::Module *holes_module = holes_design->addModule(module->name); log_assert(holes_module); - holes_module->set_bool_attribute(ID::abc9_holes); dict<IdString, Cell*> cell_cache; TimingInfo timing; @@ -300,22 +770,20 @@ void prep_xaiger(RTLIL::Module *module, bool dff) log_assert(cell); RTLIL::Module* box_module = design->module(cell->type); - if (!box_module || (!box_module->get_bool_attribute(ID::abc9_box) && !box_module->get_bool_attribute(ID::abc9_flop))) + if (!box_module) + continue; + if (!box_module->get_bool_attribute(ID::abc9_box)) continue; + log_assert(cell->parameters.empty()); + log_assert(box_module->get_blackbox_attribute()); cell->attributes[ID::abc9_box_seq] = box_count++; - IdString derived_type = box_module->derive(design, cell->parameters); - box_module = design->module(derived_type); - - auto r = cell_cache.insert(derived_type); + auto r = cell_cache.insert(cell->type); auto &holes_cell = r.first->second; if (r.second) { - if (box_module->has_processes()) - Pass::call_on_module(design, box_module, "proc"); - if (box_module->get_bool_attribute(ID::whitebox)) { - holes_cell = holes_module->addCell(cell->name, derived_type); + holes_cell = holes_module->addCell(cell->name, cell->type); if (box_module->has_processes()) Pass::call_on_module(design, box_module, "proc"); @@ -340,22 +808,7 @@ void prep_xaiger(RTLIL::Module *module, bool dff) } } else if (w->port_output) - conn = holes_module->addWire(stringf("%s.%s", derived_type.c_str(), log_id(port_name)), GetSize(w)); - } - - // For flops only, create an extra 1-bit input that drives a new wire - // called "<cell>.abc9_ff.Q" that is used below - if (box_module->get_bool_attribute(ID::abc9_flop)) { - box_inputs++; - Wire *holes_wire = holes_module->wire(stringf("\\i%d", box_inputs)); - if (!holes_wire) { - holes_wire = holes_module->addWire(stringf("\\i%d", box_inputs)); - holes_wire->port_input = true; - holes_wire->port_id = port_id++; - holes_module->ports.push_back(holes_wire->name); - } - Wire *Q = holes_module->addWire(stringf("%s.abc9_ff.Q", cell->name.c_str())); - holes_module->connect(Q, holes_wire); + conn = holes_module->addWire(stringf("%s.%s", cell->type.c_str(), log_id(port_name)), GetSize(w)); } } else // box_module is a blackbox @@ -379,90 +832,6 @@ void prep_xaiger(RTLIL::Module *module, bool dff) } } -void prep_delays(RTLIL::Design *design, bool dff_mode) -{ - TimingInfo timing; - - // Derive all Yosys blackbox modules that are not combinatorial abc9 boxes - // (e.g. DSPs, RAMs, etc.) nor abc9 flops and collect all such instantiations - pool<Module*> flops; - std::vector<Cell*> cells; - for (auto module : design->selected_modules()) { - if (module->processes.size() > 0) { - log("Skipping module %s as it contains processes.\n", log_id(module)); - continue; - } - - for (auto cell : module->cells()) { - if (cell->type.in(ID($_AND_), ID($_NOT_), ID($__ABC9_FF_), ID($__ABC9_DELAY))) - continue; - - RTLIL::Module* inst_module = module->design->module(cell->type); - if (!inst_module) - continue; - if (!inst_module->get_blackbox_attribute()) - continue; - if (inst_module->attributes.count(ID::abc9_box)) - continue; - IdString derived_type = inst_module->derive(design, cell->parameters); - inst_module = design->module(derived_type); - log_assert(inst_module); - - if (dff_mode && inst_module->get_bool_attribute(ID::abc9_flop)) { - flops.insert(inst_module); - continue; // do not add $__ABC9_DELAY boxes to flops - // as delays will be captured in the flop box - } - - if (!timing.count(derived_type)) - timing.setup_module(inst_module); - - cells.emplace_back(cell); - } - } - - // Insert $__ABC9_DELAY cells on all cells that instantiate blackboxes - // with required times - for (auto cell : cells) { - auto module = cell->module; - RTLIL::Module* inst_module = module->design->module(cell->type); - log_assert(inst_module); - IdString derived_type = inst_module->derive(design, cell->parameters); - inst_module = design->module(derived_type); - log_assert(inst_module); - - auto &t = timing.at(derived_type).required; - for (auto &conn : cell->connections_) { - auto port_wire = inst_module->wire(conn.first); - if (!port_wire) - log_error("Port %s in cell %s (type %s) of module %s does not actually exist", - log_id(conn.first), log_id(cell->name), log_id(cell->type), log_id(module->name)); - if (!port_wire->port_input) - continue; - - SigSpec O = module->addWire(NEW_ID, GetSize(conn.second)); - for (int i = 0; i < GetSize(conn.second); i++) { - auto d = t.at(TimingInfo::NameBit(conn.first,i), 0); - if (d == 0) - continue; - -#ifndef NDEBUG - if (ys_debug(1)) { - static std::set<std::tuple<IdString,IdString,int>> seen; - if (seen.emplace(derived_type, conn.first, i).second) log("%s.%s[%d] abc9_required = %d\n", - log_id(cell->type), log_id(conn.first), i, d); - } -#endif - auto box = module->addCell(NEW_ID, ID($__ABC9_DELAY)); - box->setPort(ID::I, conn.second[i]); - box->setPort(ID::O, O[i]); - box->setParam(ID::DELAY, d); - conn.second[i] = O[i]; - } - } - } -} - void prep_lut(RTLIL::Design *design, int maxlut) { TimingInfo timing; @@ -540,7 +909,7 @@ void write_lut(RTLIL::Module *module, const std::string &dst) { ofs.close(); } -void prep_box(RTLIL::Design *design, bool dff_mode) +void prep_box(RTLIL::Design *design) { TimingInfo timing; @@ -555,165 +924,162 @@ void prep_box(RTLIL::Design *design, bool dff_mode) dict<IdString,std::vector<IdString>> box_ports; for (auto module : design->modules()) { - auto abc9_flop = module->get_bool_attribute(ID::abc9_flop); - if (abc9_flop) { - auto r = module->attributes.insert(ID::abc9_box_id); - if (!r.second) - continue; - r.first->second = abc9_box_id++; - - if (dff_mode) { - int num_inputs = 0, num_outputs = 0; - for (auto port_name : module->ports) { - auto wire = module->wire(port_name); - log_assert(GetSize(wire) == 1); - if (wire->port_input) num_inputs++; - if (wire->port_output) num_outputs++; - } - log_assert(num_outputs == 1); + auto it = module->attributes.find(ID::abc9_box); + if (it == module->attributes.end()) + continue; + bool box = it->second.as_bool(); + module->attributes.erase(it); + if (!box) + continue; - ss << log_id(module) << " " << r.first->second.as_int(); - ss << " " << (module->get_bool_attribute(ID::whitebox) ? "1" : "0"); - ss << " " << num_inputs+1 << " " << num_outputs << std::endl; + auto r = module->attributes.insert(ID::abc9_box_id); + if (!r.second) + continue; + r.first->second = abc9_box_id++; + + if (module->get_bool_attribute(ID::abc9_flop)) { + int num_inputs = 0, num_outputs = 0; + for (auto port_name : module->ports) { + auto wire = module->wire(port_name); + log_assert(GetSize(wire) == 1); + if (wire->port_input) num_inputs++; + if (wire->port_output) num_outputs++; + } + log_assert(num_outputs == 1); + + ss << log_id(module) << " " << r.first->second.as_int(); + log_assert(module->get_bool_attribute(ID::whitebox)); + ss << " " << "1"; + ss << " " << num_inputs << " " << num_outputs << std::endl; + + ss << "#"; + bool first = true; + for (auto port_name : module->ports) { + auto wire = module->wire(port_name); + if (!wire->port_input) + continue; + if (first) + first = false; + else + ss << " "; + ss << log_id(wire); + } + ss << std::endl; - ss << "#"; - bool first = true; - for (auto port_name : module->ports) { - auto wire = module->wire(port_name); - if (!wire->port_input) - continue; - if (first) - first = false; - else - ss << " "; - ss << log_id(wire); - } - ss << " abc9_ff.Q" << std::endl; + auto &t = timing.setup_module(module).required; + if (t.empty()) + log_error("Module '%s' with (* abc9_flop *) has no clk-to-q timing (and thus no connectivity) information.\n", log_id(module)); - auto &t = timing.setup_module(module).required; - first = true; - for (auto port_name : module->ports) { - auto wire = module->wire(port_name); - if (!wire->port_input) - continue; - if (first) - first = false; - else - ss << " "; - log_assert(GetSize(wire) == 1); - auto it = t.find(TimingInfo::NameBit(port_name,0)); - if (it == t.end()) - // Assume that no setup time means zero - ss << 0; - else { - ss << it->second; + first = true; + for (auto port_name : module->ports) { + auto wire = module->wire(port_name); + if (!wire->port_input) + continue; + if (first) + first = false; + else + ss << " "; + log_assert(GetSize(wire) == 1); + auto it = t.find(TimingInfo::NameBit(port_name,0)); + if (it == t.end()) + // Assume no connectivity if no setup time + ss << "-"; + else { + ss << it->second; #ifndef NDEBUG - if (ys_debug(1)) { - static std::set<std::pair<IdString,IdString>> seen; - if (seen.emplace(module->name, port_name).second) log("%s.%s abc9_required = %d\n", log_id(module), - log_id(port_name), it->second); - } -#endif + if (ys_debug(1)) { + static std::set<std::pair<IdString,IdString>> seen; + if (seen.emplace(module->name, port_name).second) log("%s.%s abc9_required = %d\n", log_id(module), + log_id(port_name), it->second); } - +#endif } - // Last input is 'abc9_ff.Q' - ss << " 0" << std::endl << std::endl; - continue; } + ss << " # $_DFF_[NP]_.D" << std::endl; + ss << std::endl; } else { - if (!module->attributes.erase(ID::abc9_box)) - continue; - - auto r = module->attributes.insert(ID::abc9_box_id); - if (!r.second) - continue; - r.first->second = abc9_box_id++; - } + auto r2 = box_ports.insert(module->name); + if (r2.second) { + // Make carry in the last PI, and carry out the last PO + // since ABC requires it this way + IdString carry_in, carry_out; + for (const auto &port_name : module->ports) { + auto w = module->wire(port_name); + log_assert(w); + if (w->get_bool_attribute(ID::abc9_carry)) { + log_assert(w->port_input != w->port_output); + if (w->port_input) + carry_in = port_name; + else if (w->port_output) + carry_out = port_name; + } + else + r2.first->second.push_back(port_name); + } - auto r = box_ports.insert(module->name); - if (r.second) { - // Make carry in the last PI, and carry out the last PO - // since ABC requires it this way - IdString carry_in, carry_out; - for (const auto &port_name : module->ports) { - auto w = module->wire(port_name); - log_assert(w); - if (w->get_bool_attribute(ID::abc9_carry)) { - log_assert(w->port_input != w->port_output); - if (w->port_input) - carry_in = port_name; - else if (w->port_output) - carry_out = port_name; + if (carry_in != IdString()) { + r2.first->second.push_back(carry_in); + r2.first->second.push_back(carry_out); } - else - r.first->second.push_back(port_name); } - if (carry_in != IdString()) { - r.first->second.push_back(carry_in); - r.first->second.push_back(carry_out); + std::vector<SigBit> inputs, outputs; + for (auto port_name : r2.first->second) { + auto wire = module->wire(port_name); + if (wire->port_input) + for (int i = 0; i < GetSize(wire); i++) + inputs.emplace_back(wire, i); + if (wire->port_output) + for (int i = 0; i < GetSize(wire); i++) + outputs.emplace_back(wire, i); } - } - - std::vector<SigBit> inputs; - std::vector<SigBit> outputs; - for (auto port_name : r.first->second) { - auto wire = module->wire(port_name); - if (wire->port_input) - for (int i = 0; i < GetSize(wire); i++) - inputs.emplace_back(wire, i); - if (wire->port_output) - for (int i = 0; i < GetSize(wire); i++) - outputs.emplace_back(wire, i); - } - - ss << log_id(module) << " " << module->attributes.at(ID::abc9_box_id).as_int(); - ss << " " << (module->get_bool_attribute(ID::whitebox) ? "1" : "0"); - ss << " " << GetSize(inputs) << " " << GetSize(outputs) << std::endl; - - bool first = true; - ss << "#"; - for (const auto &i : inputs) { - if (first) - first = false; - else - ss << " "; - if (GetSize(i.wire) == 1) - ss << log_id(i.wire); - else - ss << log_id(i.wire) << "[" << i.offset << "]"; - } - ss << std::endl; - auto &t = timing.setup_module(module).comb; - if (!abc9_flop && t.empty()) - log_warning("(* abc9_box *) module '%s' has no timing (and thus no connectivity) information.\n", log_id(module)); + ss << log_id(module) << " " << module->attributes.at(ID::abc9_box_id).as_int(); + ss << " " << (module->get_bool_attribute(ID::whitebox) ? "1" : "0"); + ss << " " << GetSize(inputs) << " " << GetSize(outputs) << std::endl; - for (const auto &o : outputs) { - first = true; + bool first = true; + ss << "#"; for (const auto &i : inputs) { if (first) first = false; else ss << " "; - auto jt = t.find(TimingInfo::BitBit(i,o)); - if (jt == t.end()) - ss << "-"; + if (GetSize(i.wire) == 1) + ss << log_id(i.wire); else - ss << jt->second; + ss << log_id(i.wire) << "[" << i.offset << "]"; } - ss << " # "; - if (GetSize(o.wire) == 1) - ss << log_id(o.wire); - else - ss << log_id(o.wire) << "[" << o.offset << "]"; ss << std::endl; + auto &t = timing.setup_module(module); + if (t.comb.empty()) + log_error("Module '%s' with (* abc9_box *) has no timing (and thus no connectivity) information.\n", log_id(module)); + + for (const auto &o : outputs) { + first = true; + for (const auto &i : inputs) { + if (first) + first = false; + else + ss << " "; + auto jt = t.comb.find(TimingInfo::BitBit(i,o)); + if (jt == t.comb.end()) + ss << "-"; + else + ss << jt->second; + } + ss << " # "; + if (GetSize(o.wire) == 1) + ss << log_id(o.wire); + else + ss << log_id(o.wire) << "[" << o.offset << "]"; + ss << std::endl; + } + ss << std::endl; } - ss << std::endl; } // ABC expects at least one box @@ -730,7 +1096,7 @@ void write_box(RTLIL::Module *module, const std::string &dst) { ofs.close(); } -void reintegrate(RTLIL::Module *module) +void reintegrate(RTLIL::Module *module, bool dff_mode) { auto design = module->design; log_assert(design); @@ -744,6 +1110,8 @@ void reintegrate(RTLIL::Module *module) for (auto w : mapped_mod->wires()) { auto nw = module->addWire(remap_name(w->name), GetSize(w)); nw->start_offset = w->start_offset; + // Remove all (* init *) since they only existon $_DFF_[NP]_ + w->attributes.erase(ID::init); } dict<IdString,std::vector<IdString>> box_ports; @@ -783,7 +1151,14 @@ void reintegrate(RTLIL::Module *module) for (auto cell : module->cells().to_vector()) { if (cell->has_keep_attr()) continue; - if (cell->type.in(ID($_AND_), ID($_NOT_), ID($__ABC9_FF_))) + + // Short out $_DFF_[NP]_ cells since the flop box already has + // all the information we need to reconstruct cell + if (dff_mode && cell->type.in(ID($_DFF_N_), ID($_DFF_P_)) && !cell->get_bool_attribute(ID::abc9_keep)) { + module->connect(cell->getPort(ID::Q), cell->getPort(ID::D)); + module->remove(cell); + } + else if (cell->type.in(ID($_AND_), ID($_NOT_))) module->remove(cell); else if (cell->attributes.erase(ID::abc9_box_seq)) boxes.emplace_back(cell); @@ -797,6 +1172,18 @@ void reintegrate(RTLIL::Module *module) std::map<IdString, int> cell_stats; for (auto mapped_cell : mapped_mod->cells()) { + // Short out $_FF_ cells since the flop box already has + // all the information we need to reconstruct cell + if (dff_mode && mapped_cell->type == ID($_FF_)) { + SigBit D = mapped_cell->getPort(ID::D); + SigBit Q = mapped_cell->getPort(ID::Q); + if (D.wire) + D.wire = module->wires_.at(remap_name(D.wire->name)); + Q.wire = module->wires_.at(remap_name(Q.wire->name)); + module->connect(Q, D); + continue; + } + // TODO: Speed up toposort -- we care about NOT ordering only toposort.node(mapped_cell->name); @@ -846,7 +1233,7 @@ void reintegrate(RTLIL::Module *module) continue; } - if (mapped_cell->type.in(ID($lut), ID($__ABC9_FF_))) { + if (mapped_cell->type == ID($lut)) { RTLIL::Cell *cell = module->addCell(remap_name(mapped_cell->name), mapped_cell->type); cell->parameters = mapped_cell->parameters; cell->attributes = mapped_cell->attributes; @@ -881,7 +1268,7 @@ void reintegrate(RTLIL::Module *module) if (!existing_cell) log_error("Cannot find existing box cell with name '%s' in original design.\n", log_id(mapped_cell)); - if (existing_cell->type == ID($__ABC9_DELAY)) { + if (existing_cell->type.begins_with("$paramod$__ABC9_DELAY\\DELAY=")) { SigBit I = mapped_cell->getPort(ID(i)); SigBit O = mapped_cell->getPort(ID(o)); if (I.wire) @@ -893,10 +1280,8 @@ void reintegrate(RTLIL::Module *module) } RTLIL::Module* box_module = design->module(existing_cell->type); - IdString derived_type = box_module->derive(design, existing_cell->parameters); - RTLIL::Module* derived_module = design->module(derived_type); - log_assert(derived_module); - log_assert(mapped_cell->type == stringf("$__boxid%d", derived_module->attributes.at(ID::abc9_box_id).as_int())); + log_assert(existing_cell->parameters.empty()); + log_assert(mapped_cell->type == stringf("$__boxid%d", box_module->attributes.at(ID::abc9_box_id).as_int())); mapped_cell->type = existing_cell->type; RTLIL::Cell *cell = module->addCell(remap_name(mapped_cell->name), mapped_cell->type); @@ -913,7 +1298,7 @@ void reintegrate(RTLIL::Module *module) SigSpec outputs = std::move(jt->second); mapped_cell->connections_.erase(jt); - auto abc9_flop = box_module->attributes.count(ID::abc9_flop); + auto abc9_flop = box_module->get_bool_attribute(ID::abc9_flop); if (!abc9_flop) { for (const auto &i : inputs) bit_users[i].insert(mapped_cell->name); @@ -924,7 +1309,7 @@ void reintegrate(RTLIL::Module *module) } int input_count = 0, output_count = 0; - for (const auto &port_name : box_ports.at(derived_type)) { + for (const auto &port_name : box_ports.at(existing_cell->type)) { RTLIL::Wire *w = box_module->wire(port_name); log_assert(w); @@ -988,7 +1373,7 @@ void reintegrate(RTLIL::Module *module) RTLIL::Wire *mapped_wire = mapped_mod->wire(port); RTLIL::Wire *wire = module->wire(port); log_assert(wire); - wire->attributes.erase(ID::abc9_scc); + wire->attributes.erase(ID::abc9_keep); RTLIL::Wire *remap_wire = module->wire(remap_name(port)); RTLIL::SigSpec signal(wire, remap_wire->start_offset-wire->start_offset, GetSize(remap_wire)); @@ -1116,6 +1501,37 @@ struct Abc9OpsPass : public Pass { log(" check that the design is valid, e.g. (* abc9_box_id *) values are unique,\n"); log(" (* abc9_carry *) is only given for one input/output port, etc.\n"); log("\n"); + log(" -prep_hier\n"); + log(" derive all used (* abc9_box *) or (* abc9_flop *) (if -dff option)\n"); + log(" whitebox modules. with (* abc9_flop *) modules, only those containing\n"); + log(" $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC limitation\n"); + log(" -- will be derived.\n"); + log("\n"); + log(" -prep_bypass\n"); + log(" create techmap rules in the '$abc9_map' and '$abc9_unmap' designs for\n"); + log(" bypassing sequential (* abc9_box *) modules using a combinatorial box\n"); + log(" (named *_$abc9_byp). bypassing is necessary if sequential elements (e.g.\n"); + log(" $dff, $mem, etc.) are discovered inside so that any combinatorial paths\n"); + log(" will be correctly captured. this bypass box will only contain ports that\n"); + log(" are referenced by a simple path declaration ($specify2 cell) inside a\n"); + log(" specify block.\n"); + log("\n"); + log(" -prep_dff\n"); + log(" select all (* abc9_flop *) modules instantiated in the design and store\n"); + log(" in the named selection '$abc9_flops'.\n"); + log("\n"); + log(" -prep_dff_submod\n"); + log(" within (* abc9_flop *) modules, rewrite all edge-sensitive path\n"); + log(" declarations and $setup() timing checks ($specify3 and $specrule cells)\n"); + log(" that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port to\n"); + log(" the DFF's 'D' port. this is to prepare such specify cells to be moved\n"); + log(" into the flop box.\n"); + log("\n"); + log(" -prep_dff_unmap\n"); + log(" populate the '$abc9_unmap' design with techmap rules for mapping *_$abc9_flop\n"); + log(" cells back into their derived cell types (where the rules created by\n"); + log(" -prep_hier will then map back to the original cell with parameters).\n"); + log("\n"); log(" -prep_delays\n"); log(" insert `$__ABC9_DELAY' blackbox cells into the design to account for\n"); log(" certain required times.\n"); @@ -1128,18 +1544,13 @@ struct Abc9OpsPass : public Pass { log("\n"); log(" -prep_xaiger\n"); log(" prepare the design for XAIGER output. this includes computing the\n"); - log(" topological ordering of ABC9 boxes, as well as preparing the\n"); - log(" '<module-name>$holes' module that contains the logic behaviour of ABC9\n"); - log(" whiteboxes.\n"); + log(" topological ordering of ABC9 boxes, as well as preparing the '$abc9_holes'\n"); + log(" design that contains the logic behaviour of ABC9 whiteboxes.\n"); log("\n"); log(" -dff\n"); log(" consider flop cells (those instantiating modules marked with (* abc9_flop *))\n"); log(" during -prep_{delays,xaiger,box}.\n"); log("\n"); - log(" -prep_dff\n"); - log(" compute the clock domain and initial value of each flop in the design.\n"); - log(" process the '$holes' module to support clock-enable functionality.\n"); - log("\n"); log(" -prep_lut <maxlut>\n"); log(" pre-compute the lut library by analysing all modules marked with\n"); log(" (* abc9_lut=<area> *).\n"); @@ -1167,7 +1578,9 @@ struct Abc9OpsPass : public Pass { bool check_mode = false; bool prep_delays_mode = false; bool mark_scc_mode = false; - bool prep_dff_mode = false; + bool prep_hier_mode = false; + bool prep_bypass_mode = false; + bool prep_dff_mode = false, prep_dff_submod_mode = false, prep_dff_unmap_mode = false; bool prep_xaiger_mode = false; bool prep_lut_mode = false; bool prep_box_mode = false; @@ -1177,53 +1590,81 @@ struct Abc9OpsPass : public Pass { int maxlut = 0; std::string write_box_dst; + bool valid = false; size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; if (arg == "-check") { check_mode = true; + valid = true; continue; } if (arg == "-mark_scc") { mark_scc_mode = true; + valid = true; + continue; + } + if (arg == "-prep_hier") { + prep_hier_mode = true; + valid = true; + continue; + } + if (arg == "-prep_bypass") { + prep_bypass_mode = true; + valid = true; continue; } if (arg == "-prep_dff") { prep_dff_mode = true; + valid = true; + continue; + } + if (arg == "-prep_dff_submod") { + prep_dff_submod_mode = true; + valid = true; + continue; + } + if (arg == "-prep_dff_unmap") { + prep_dff_unmap_mode = true; + valid = true; continue; } if (arg == "-prep_xaiger") { prep_xaiger_mode = true; + valid = true; continue; } if (arg == "-prep_delays") { prep_delays_mode = true; + valid = true; continue; } if (arg == "-prep_lut" && argidx+1 < args.size()) { prep_lut_mode = true; maxlut = atoi(args[++argidx].c_str()); - continue; - } - if (arg == "-maxlut" && argidx+1 < args.size()) { + valid = true; continue; } if (arg == "-write_lut" && argidx+1 < args.size()) { write_lut_dst = args[++argidx]; rewrite_filename(write_lut_dst); + valid = true; continue; } if (arg == "-prep_box") { prep_box_mode = true; + valid = true; continue; } if (arg == "-write_box" && argidx+1 < args.size()) { write_box_dst = args[++argidx]; rewrite_filename(write_box_dst); + valid = true; continue; } if (arg == "-reintegrate") { reintegrate_mode = true; + valid = true; continue; } if (arg == "-dff") { @@ -1234,25 +1675,32 @@ struct Abc9OpsPass : public Pass { } extra_args(args, argidx, design); - if (!(check_mode || mark_scc_mode || prep_delays_mode || prep_xaiger_mode || prep_dff_mode || prep_lut_mode || prep_box_mode || !write_lut_dst.empty() || !write_box_dst.empty() || reintegrate_mode)) - log_cmd_error("At least one of -check, -mark_scc, -prep_{delays,xaiger,dff,lut,box}, -write_{lut,box}, -reintegrate must be specified.\n"); + if (!valid) + log_cmd_error("At least one of -check, -mark_scc, -prep_{delays,xaiger,dff[123],lut,box}, -write_{lut,box}, -reintegrate must be specified.\n"); - if (dff_mode && !prep_delays_mode && !prep_xaiger_mode && !prep_box_mode) - log_cmd_error("'-dff' option is only relevant for -prep_{delay,xaiger,box}.\n"); + if (dff_mode && !check_mode && !prep_hier_mode && !prep_delays_mode && !prep_xaiger_mode && !reintegrate_mode) + log_cmd_error("'-dff' option is only relevant for -prep_{hier,delay,xaiger} or -reintegrate.\n"); if (check_mode) - check(design); + check(design, dff_mode); + if (prep_hier_mode) + prep_hier(design, dff_mode); + if (prep_bypass_mode) + prep_bypass(design); + if (prep_dff_mode) + prep_dff(design); + if (prep_dff_submod_mode) + prep_dff_submod(design); + if (prep_dff_unmap_mode) + prep_dff_unmap(design); if (prep_delays_mode) prep_delays(design, dff_mode); if (prep_lut_mode) prep_lut(design, maxlut); if (prep_box_mode) - prep_box(design, dff_mode); + prep_box(design); for (auto mod : design->selected_modules()) { - if (mod->get_bool_attribute(ID::abc9_holes)) - continue; - if (mod->processes.size() > 0) { log("Skipping module %s as it contains processes.\n", log_id(mod)); continue; @@ -1267,12 +1715,10 @@ struct Abc9OpsPass : public Pass { write_box(mod, write_box_dst); if (mark_scc_mode) mark_scc(mod); - if (prep_dff_mode) - prep_dff(mod); if (prep_xaiger_mode) prep_xaiger(mod, dff_mode); if (reintegrate_mode) - reintegrate(mod); + reintegrate(mod, dff_mode); } } } Abc9OpsPass; |