diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/eval.cc | 38 | ||||
| -rw-r--r-- | passes/sat/expose.cc | 32 | ||||
| -rw-r--r-- | passes/sat/freduce.cc | 85 | ||||
| -rw-r--r-- | passes/sat/miter.cc | 110 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 465 |
5 files changed, 529 insertions, 201 deletions
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc index 62534ec0b..09f69cc5c 100644 --- a/passes/sat/eval.cc +++ b/passes/sat/eval.cc @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -87,7 +87,7 @@ struct BruteForceEquivChecker BruteForceEquivChecker(RTLIL::Module *mod1, RTLIL::Module *mod2, bool ignore_x_mod1) : mod1(mod1), mod2(mod2), counter(0), errors(0), ignore_x_mod1(ignore_x_mod1) { - log("Checking for equivialence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str()); + log("Checking for equivalence (brute-force): %s vs %s\n", mod1->name.c_str(), mod2->name.c_str()); for (auto &w : mod1->wires_) { RTLIL::Wire *wire1 = w.second; @@ -143,16 +143,16 @@ struct VlogHammerReporter { log("Verifying SAT model (%s)..\n", model_undef ? "with undef" : "without undef"); - ezDefaultSAT ez; + ezSatPtr ez; SigMap sigmap(module); - SatGen satgen(&ez, &sigmap); + SatGen satgen(ez.get(), &sigmap); satgen.model_undef = model_undef; for (auto &c : module->cells_) if (!satgen.importCell(c.second)) log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); - ez.assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); + ez->assume(satgen.signals_eq(recorded_set_vars, recorded_set_vals)); std::vector<int> y_vec = satgen.importDefSigSpec(module->wires_.at("\\y")); std::vector<bool> y_values; @@ -163,9 +163,9 @@ struct VlogHammerReporter } log(" Created SAT problem with %d variables and %d clauses.\n", - ez.numCnfVariables(), ez.numCnfClauses()); + ez->numCnfVariables(), ez->numCnfClauses()); - if (!ez.solve(y_vec, y_values)) + if (!ez->solve(y_vec, y_values)) log_error("Failed to find solution to SAT problem.\n"); for (int i = 0; i < expected_y.size(); i++) { @@ -204,7 +204,7 @@ struct VlogHammerReporter if (y_undef.at(i)) { log(" Toggling undef bit %d to test undef gating.\n", i); - if (!ez.solve(y_vec, y_values, ez.IFF(y_vec.at(i), y_values.at(i) ? ez.CONST_FALSE : ez.CONST_TRUE))) + if (!ez->solve(y_vec, y_values, ez->IFF(y_vec.at(i), y_values.at(i) ? ez->CONST_FALSE : ez->CONST_TRUE))) log_error("Failed to find solution with toggled bit!\n"); cmp_vars.push_back(y_vec.at(expected_y.size() + i)); @@ -220,15 +220,15 @@ struct VlogHammerReporter } log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(cmp_vars, ez.vec_const(cmp_vals))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(cmp_vars, ez->vec_const(cmp_vals))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } else { log(" Testing if SAT solution is unique.\n"); - ez.assume(ez.vec_ne(y_vec, ez.vec_const(y_values))); - if (ez.solve(y_vec, y_values)) + ez->assume(ez->vec_ne(y_vec, ez->vec_const(y_values))); + if (ez->solve(y_vec, y_values)) log_error("Found two distinct solutions to SAT problem.\n"); } @@ -389,7 +389,7 @@ struct EvalPass : public Pass { std::vector<std::string> shows, tables; bool set_undef = false; - log_header("Executing EVAL pass (evaluate the circuit given an input).\n"); + log_header(design, "Executing EVAL pass (evaluate the circuit given an input).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -421,7 +421,7 @@ struct EvalPass : public Pass { log_error("Can't find module `%s'!\n", mod2_name.c_str()); BruteForceEquivChecker checker(design->modules_.at(mod1_name), design->modules_.at(mod2_name), args[argidx-2] == "-brute_force_equiv_checker_x"); if (checker.errors > 0) - log_cmd_error("Modules are not equivialent!\n"); + log_cmd_error("Modules are not equivalent!\n"); log("Verified %s = %s (using brute-force check on %d cases).\n", mod1_name.c_str(), mod2_name.c_str(), checker.counter); return; @@ -448,7 +448,7 @@ struct EvalPass : public Pass { RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first)); module = mod_it.second; } - if (module == NULL) + if (module == NULL) log_cmd_error("Can't perform EVAL on an empty selection!\n"); ConstEval ce(module); @@ -568,7 +568,7 @@ struct EvalPass : public Pass { if (tab_column_width.size() < row.size()) tab_column_width.resize(row.size()); for (size_t i = 0; i < row.size(); i++) - tab_column_width[i] = std::max(tab_column_width[i], int(row[i].size())); + tab_column_width[i] = max(tab_column_width[i], int(row[i].size())); } log("\n"); @@ -594,10 +594,10 @@ struct EvalPass : public Pass { log("\n"); if (undef.size() > 0) { undef.sort_and_unify(); - log("Assumend undef (x) value for the following singals: %s\n\n", log_signal(undef)); + log("Assumed undef (x) value for the following signals: %s\n\n", log_signal(undef)); } } } } EvalPass; - + PRIVATE_NAMESPACE_END diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc index b012bc6a4..9427547f3 100644 --- a/passes/sat/expose.cc +++ b/passes/sat/expose.cc @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -116,7 +116,7 @@ void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::De info.cell = it.second; if (info.cell->type == "$dff") { - info.bit_clk = sigmap(info.cell->getPort("\\CLK")).to_single_sigbit(); + info.bit_clk = sigmap(info.cell->getPort("\\CLK")).as_bit(); info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool(); std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector(); std::vector<RTLIL::SigBit> sig_q = sigmap(info.cell->getPort("\\Q")).to_sigbit_vector(); @@ -128,8 +128,8 @@ void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::De } if (info.cell->type == "$adff") { - info.bit_clk = sigmap(info.cell->getPort("\\CLK")).to_single_sigbit(); - info.bit_arst = sigmap(info.cell->getPort("\\ARST")).to_single_sigbit(); + info.bit_clk = sigmap(info.cell->getPort("\\CLK")).as_bit(); + info.bit_arst = sigmap(info.cell->getPort("\\ARST")).as_bit(); info.clk_polarity = info.cell->parameters.at("\\CLK_POLARITY").as_bool(); info.arst_polarity = info.cell->parameters.at("\\ARST_POLARITY").as_bool(); std::vector<RTLIL::SigBit> sig_d = sigmap(info.cell->getPort("\\D")).to_sigbit_vector(); @@ -144,21 +144,21 @@ void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::De } if (info.cell->type == "$_DFF_N_" || info.cell->type == "$_DFF_P_") { - info.bit_clk = sigmap(info.cell->getPort("\\C")).to_single_sigbit(); + info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit(); info.clk_polarity = info.cell->type == "$_DFF_P_"; - info.bit_d = sigmap(info.cell->getPort("\\D")).to_single_sigbit(); - bit_info[sigmap(info.cell->getPort("\\Q")).to_single_sigbit()] = info; + info.bit_d = sigmap(info.cell->getPort("\\D")).as_bit(); + bit_info[sigmap(info.cell->getPort("\\Q")).as_bit()] = info; continue; } if (info.cell->type.size() == 10 && info.cell->type.substr(0, 6) == "$_DFF_") { - info.bit_clk = sigmap(info.cell->getPort("\\C")).to_single_sigbit(); - info.bit_arst = sigmap(info.cell->getPort("\\R")).to_single_sigbit(); + info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit(); + info.bit_arst = sigmap(info.cell->getPort("\\R")).as_bit(); info.clk_polarity = info.cell->type[6] == 'P'; info.arst_polarity = info.cell->type[7] == 'P'; info.arst_value = info.cell->type[0] == '1' ? RTLIL::State::S1 : RTLIL::State::S0; - info.bit_d = sigmap(info.cell->getPort("\\D")).to_single_sigbit(); - bit_info[sigmap(info.cell->getPort("\\Q")).to_single_sigbit()] = info; + info.bit_d = sigmap(info.cell->getPort("\\D")).as_bit(); + bit_info[sigmap(info.cell->getPort("\\Q")).as_bit()] = info; continue; } } @@ -237,8 +237,8 @@ struct ExposePass : public Pass { log(" signal path at that wire.\n"); log("\n"); log(" -shared\n"); - log(" only expose those signals that are shared ammong the selected modules.\n"); - log(" this is useful for preparing modules for equivialence checking.\n"); + log(" only expose those signals that are shared among the selected modules.\n"); + log(" this is useful for preparing modules for equivalence checking.\n"); log("\n"); log(" -evert\n"); log(" also turn connections to instances of other modules to additional\n"); @@ -262,7 +262,7 @@ struct ExposePass : public Pass { bool flag_evert_dff = false; std::string sep = "."; - log_header("Executing EXPOSE pass (exposing internal signals as outputs).\n"); + log_header(design, "Executing EXPOSE pass (exposing internal signals as outputs).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) @@ -646,5 +646,5 @@ struct ExposePass : public Pass { } } } ExposePass; - + PRIVATE_NAMESPACE_END diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc index fbca35861..77263f6a2 100644 --- a/passes/sat/freduce.cc +++ b/passes/sat/freduce.cc @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -73,7 +73,7 @@ struct FindReducedInputs SigMap &sigmap; drivers_t &drivers; - ezDefaultSAT ez; + ezSatPtr ez; std::set<RTLIL::Cell*> ez_cells; SatGen satgen; @@ -81,7 +81,7 @@ struct FindReducedInputs std::vector<int> sat_pi_uniq_bitvec; FindReducedInputs(SigMap &sigmap, drivers_t &drivers) : - sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap) + sigmap(sigmap), drivers(drivers), satgen(ez.get(), &sigmap) { satgen.model_undef = true; } @@ -104,30 +104,30 @@ struct FindReducedInputs satgen.setContext(&sigmap, "A"); int sat_a = satgen.importSigSpec(bit).front(); - ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front())); satgen.setContext(&sigmap, "B"); int sat_b = satgen.importSigSpec(bit).front(); - ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(bit).front())); int idx = sat_pi.size(); size_t idx_bits = get_bits(idx); if (sat_pi_uniq_bitvec.size() != idx_bits) { - sat_pi_uniq_bitvec.push_back(ez.frozen_literal(stringf("uniq_%d", int(idx_bits)-1))); + sat_pi_uniq_bitvec.push_back(ez->frozen_literal(stringf("uniq_%d", int(idx_bits)-1))); for (auto &it : sat_pi) - ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back()))); + ez->assume(ez->OR(ez->NOT(it.second), ez->NOT(sat_pi_uniq_bitvec.back()))); } log_assert(sat_pi_uniq_bitvec.size() == idx_bits); - sat_pi[bit] = ez.frozen_literal(stringf("p, falsei_%s", log_signal(bit))); - ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit])); + sat_pi[bit] = ez->frozen_literal(stringf("p, falsei_%s", log_signal(bit))); + ez->assume(ez->IFF(ez->XOR(sat_a, sat_b), sat_pi[bit])); for (size_t i = 0; i < idx_bits; i++) if ((idx & (1 << i)) == 0) - ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i]))); + ez->assume(ez->OR(ez->NOT(sat_pi[bit]), ez->NOT(sat_pi_uniq_bitvec[i]))); else - ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i])); + ez->assume(ez->OR(ez->NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i])); } void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out) @@ -201,7 +201,7 @@ struct FindReducedInputs model_expr.push_back(sat_pi.at(pi[i])); } - if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) + if (!ez->solve(model_expr, model, ez->expression(ezSAT::OpOr, model_expr), ez->XOR(output_a, output_b), ez->NOT(output_undef_a), ez->NOT(output_undef_b))) break; int found_count = 0; @@ -229,8 +229,9 @@ struct PerformReduction SigMap &sigmap; drivers_t &drivers; std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs; + pool<SigBit> recursion_guard; - ezDefaultSAT ez; + ezSatPtr ez; SatGen satgen; std::vector<int> sat_pi, sat_out, sat_def; @@ -246,6 +247,15 @@ struct PerformReduction if (sigdepth.count(out) != 0) return sigdepth.at(out); + if (recursion_guard.count(out)) { + string loop_signals; + for (auto loop_bit : recursion_guard) + loop_signals += string(" ") + log_signal(loop_bit); + log_error("Found logic loop:%s\n", loop_signals.c_str()); + } + + recursion_guard.insert(out); + if (drivers.count(out) != 0) { std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out); if (celldone.count(drv.first) == 0) { @@ -255,20 +265,21 @@ struct PerformReduction } int max_child_depth = 0; for (auto &bit : drv.second) - max_child_depth = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_depth); + max_child_depth = max(register_cone_worker(celldone, sigdepth, bit), max_child_depth); sigdepth[out] = max_child_depth + 1; } else { pi_bits.push_back(out); sat_pi.push_back(satgen.importSigSpec(out).front()); - ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front())); + ez->assume(ez->NOT(satgen.importUndefSigSpec(out).front())); sigdepth[out] = 0; } + recursion_guard.erase(out); return sigdepth.at(out); } PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits, int cone_size) : - sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits), cone_size(cone_size) + sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(ez.get(), &sigmap), out_bits(bits), cone_size(cone_size) { satgen.model_undef = true; @@ -278,15 +289,15 @@ struct PerformReduction for (auto &bit : bits) { out_depth.push_back(register_cone_worker(celldone, sigdepth, bit)); sat_out.push_back(satgen.importSigSpec(bit).front()); - sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front())); + sat_def.push_back(ez->NOT(satgen.importUndefSigSpec(bit).front())); } if (inv_mode && cone_size > 0) { - if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def))) + if (!ez->solve(sat_out, out_inverted, ez->expression(ezSAT::OpAnd, sat_def))) log_error("Solving for initial model failed!\n"); for (size_t i = 0; i < sat_out.size(); i++) if (out_inverted.at(i)) - sat_out[i] = ez.NOT(sat_out[i]); + sat_out[i] = ez->NOT(sat_out[i]); } else out_inverted = std::vector<bool>(sat_out.size(), false); } @@ -296,8 +307,8 @@ struct PerformReduction if (verbose_level == 1) log(" Finding const value for %s.\n", log_signal(out_bits[idx])); - bool can_be_set = ez.solve(ez.AND(sat_out[idx], sat_def[idx])); - bool can_be_clr = ez.solve(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + bool can_be_set = ez->solve(ez->AND(sat_out[idx], sat_def[idx])); + bool can_be_clr = ez->solve(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); log_assert(!can_be_set || !can_be_clr); RTLIL::SigBit value(RTLIL::State::Sx); @@ -355,8 +366,8 @@ struct PerformReduction std::vector<int> sat_set_list, sat_clr_list; for (int idx : bucket) { - sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx])); - sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx])); + sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); } std::vector<int> modelVars = sat_out; @@ -366,7 +377,7 @@ struct PerformReduction if (verbose_level >= 2) modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end()); - if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list))) + if (ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list))) { int iter_count = 1; @@ -379,13 +390,13 @@ struct PerformReduction for (int idx : bucket) if (!model[sat_out.size() + idx]) { - sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx])); - sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx])); + sat_set_list.push_back(ez->AND(sat_out[idx], sat_def[idx])); + sat_clr_list.push_back(ez->AND(ez->NOT(sat_out[idx]), sat_def[idx])); } else { sat_def_list.push_back(sat_def[idx]); } - if (!ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list), ez.expression(ezSAT::OpAnd, sat_def_list))) + if (!ez->solve(modelVars, model, ez->expression(ezSAT::OpOr, sat_set_list), ez->expression(ezSAT::OpOr, sat_clr_list), ez->expression(ezSAT::OpAnd, sat_def_list))) break; iter_count++; } @@ -431,7 +442,7 @@ struct PerformReduction for (int idx2 : bucket) if (idx != idx2) sat_def_list.push_back(sat_def[idx2]); - if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list))) + if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list))) undef_slaves.push_back(idx); } @@ -446,7 +457,7 @@ struct PerformReduction out_depth[idx] = std::numeric_limits<int>::max(); if (verbose_level >= 1) { - log("%s Found %d equivialent signals:", indt, int(bucket.size())); + log("%s Found %d equivalent signals:", indt, int(bucket.size())); for (int idx : bucket) log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx])); log("\n"); @@ -495,7 +506,7 @@ struct PerformReduction std::vector<RTLIL::SigBit> r_sigbits; for (int idx : r) r_sigbits.push_back(out_bits[idx]); - log(" Found group of %d equivialent signals: %s\n", int(r.size()), log_signal(r_sigbits)); + log(" Found group of %d equivalent signals: %s\n", int(r.size()), log_signal(r_sigbits)); } std::vector<int> undef_slaves; @@ -505,7 +516,7 @@ struct PerformReduction for (int idx2 : r) if (idx != idx2) sat_def_list.push_back(sat_def[idx2]); - if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list))) + if (ez->solve(ez->NOT(sat_def[idx]), ez->expression(ezSAT::OpOr, sat_def_list))) undef_slaves.push_back(idx); } @@ -681,7 +692,7 @@ struct FreduceWorker if (!dump_prefix.empty()) dump(); - log(" Rewiring %d equivialent groups:\n", int(equiv.size())); + log(" Rewiring %d equivalent groups:\n", int(equiv.size())); int rewired_sigbits = 0; for (auto &grp : equiv) { @@ -755,7 +766,7 @@ struct FreducePass : public Pass { log(" freduce [options] [selection]\n"); log("\n"); log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n"); - log("equivialent, they are merged to one node and one of the redundant drivers is\n"); + log("equivalent, they are merged to one node and one of the redundant drivers is\n"); log("disconnected. A subsequent call to 'clean' will remove the redundant drivers.\n"); log("\n"); log(" -v, -vv\n"); @@ -773,7 +784,7 @@ struct FreducePass : public Pass { log(" operation. this is mostly used for debugging the freduce command.\n"); log("\n"); log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n"); - log("equivialent nodes.\n"); + log("equivalent nodes.\n"); log("\n"); log("All selected wires are considered for rewiring. The selected cells cover the\n"); log("circuit that is analyzed.\n"); @@ -787,7 +798,7 @@ struct FreducePass : public Pass { inv_mode = false; dump_prefix = std::string(); - log_header("Executing FREDUCE pass (perform functional reduction).\n"); + log_header(design, "Executing FREDUCE pass (perform functional reduction).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -825,5 +836,5 @@ struct FreducePass : public Pass { log("Rewired a total of %d signal bits.\n", bitcount); } } FreducePass; - + PRIVATE_NAMESPACE_END diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 9853cd0c6..4854e19bf 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -32,7 +32,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: bool flag_make_assert = false; bool flag_flatten = false; - log_header("Executing MITER pass (creating miter circuit).\n"); + log_header(design, "Executing MITER pass (creating miter circuit).\n"); size_t argidx; for (argidx = 2; argidx < args.size(); argidx++) @@ -61,7 +61,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: } if (argidx+3 != args.size() || args[argidx].substr(0, 1) == "-") that->cmd_error(args, argidx, "command argument error"); - + RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]); RTLIL::IdString gate_name = RTLIL::escape_id(args[argidx++]); RTLIL::IdString miter_name = RTLIL::escape_id(args[argidx++]); @@ -71,7 +71,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: if (design->modules_.count(gate_name) == 0) log_cmd_error("Can't find gate module %s!\n", gate_name.c_str()); if (design->modules_.count(miter_name) != 0) - log_cmd_error("There is already a module %s!\n", gate_name.c_str()); + log_cmd_error("There is already a module %s!\n", miter_name.c_str()); RTLIL::Module *gold_module = design->modules_.at(gold_name); RTLIL::Module *gate_module = design->modules_.at(gate_name); @@ -254,7 +254,80 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL: if (flag_flatten) { log_push(); - Pass::call_on_module(design, miter_module, "flatten; opt_const -keepdc -undriven;;"); + Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;"); + log_pop(); + } +} + +void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL::Design *design) +{ + bool flag_make_outputs = false; + bool flag_flatten = false; + + log_header(design, "Executing MITER pass (creating miter circuit).\n"); + + size_t argidx; + for (argidx = 2; argidx < args.size(); argidx++) + { + if (args[argidx] == "-make_outputs") { + flag_make_outputs = true; + continue; + } + if (args[argidx] == "-flatten") { + flag_flatten = true; + continue; + } + break; + } + if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].substr(0, 1) == "-") + that->cmd_error(args, argidx, "command argument error"); + + IdString module_name = RTLIL::escape_id(args[argidx++]); + IdString miter_name = argidx < args.size() ? RTLIL::escape_id(args[argidx++]) : ""; + + if (design->modules_.count(module_name) == 0) + log_cmd_error("Can't find module %s!\n", module_name.c_str()); + if (!miter_name.empty() && design->modules_.count(miter_name) != 0) + log_cmd_error("There is already a module %s!\n", miter_name.c_str()); + + Module *module = design->module(module_name); + + if (!miter_name.empty()) { + module = module->clone(); + module->name = miter_name; + design->add(module); + } + + if (!flag_make_outputs) + for (auto wire : module->wires()) + wire->port_output = false; + + Wire *trigger = module->addWire("\\trigger"); + trigger->port_output = true; + module->fixup_ports(); + + if (flag_flatten) { + log_push(); + Pass::call_on_module(design, module, "flatten;;"); + log_pop(); + } + + SigSpec or_signals; + vector<Cell*> cell_list = module->cells(); + for (auto cell : cell_list) { + if (cell->type == "$assert") { + SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); + SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); + or_signals.append(module->And(NEW_ID, is_active, is_enabled)); + module->remove(cell); + } + } + + module->addReduceOr(NEW_ID, or_signals, trigger); + + if (flag_flatten) { + log_push(); + Pass::call_on_module(design, module, "opt_expr -keepdc -undriven;;"); log_pop(); } } @@ -267,7 +340,7 @@ struct MiterPass : public Pass { log("\n"); log(" miter -equiv [options] gold_name gate_name miter_name\n"); log("\n"); - log("Creates a miter circuit for equivialence checking. The gold- and gate- modules\n"); + log("Creates a miter circuit for equivalence checking. The gold- and gate- modules\n"); log("must have the same interfaces. The miter circuit will have all inputs of the\n"); log("two source modules, prefixed with 'in_'. The miter circuit has a 'trigger'\n"); log("output that goes high if an output mismatch between the two source modules is\n"); @@ -288,7 +361,21 @@ struct MiterPass : public Pass { log(" also create an 'assert' cell that checks if trigger is always low.\n"); log("\n"); log(" -flatten\n"); - log(" call 'flatten; opt_const -keepdc -undriven;;' on the miter circuit.\n"); + log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); + log("\n"); + log("\n"); + log(" miter -assert [options] module [miter_name]\n"); + log("\n"); + log("Creates a miter circuit for property checking. All input ports are kept,\n"); + log("output ports are discarded. An additional output 'trigger' is created that\n"); + log("goes high when an assert is violated. Without a miter_name, the existing\n"); + log("module is modified.\n"); + log("\n"); + log(" -make_outputs\n"); + log(" keep module output ports.\n"); + log("\n"); + log(" -flatten\n"); + log(" call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n"); log("\n"); } virtual void execute(std::vector<std::string> args, RTLIL::Design *design) @@ -298,8 +385,13 @@ struct MiterPass : public Pass { return; } + if (args.size() > 1 && args[1] == "-assert") { + create_miter_assert(this, args, design); + return; + } + log_cmd_error("Missing mode parameter!\n"); } } MiterPass; - + PRIVATE_NAMESPACE_END diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 1aae421f0..c3cb435d1 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -2,11 +2,11 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> - * + * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. - * + * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -41,16 +41,17 @@ struct SatHelper RTLIL::Design *design; RTLIL::Module *module; - ezDefaultSAT ez; SigMap sigmap; CellTypes ct; + + ezSatPtr ez; SatGen satgen; // additional constraints std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init; std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at; std::map<int, std::vector<std::string>> unsets_at; - bool prove_asserts; + bool prove_asserts, set_assumes; // undef constraints bool enable_undef, set_init_def, set_init_undef, set_init_zero, ignore_unknown_cells; @@ -65,7 +66,7 @@ struct SatHelper bool gotTimeout; SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) : - design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap) + design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap) { this->enable_undef = enable_undef; satgen.model_undef = enable_undef; @@ -155,7 +156,7 @@ struct SatHelper if (set_init_def) { RTLIL::SigSpec rem = satgen.initial_state.export_all(); std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1); - ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_rem))); + ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem))); } if (set_init_undef) { @@ -179,7 +180,7 @@ struct SatHelper log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs)); check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); - ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1)); + ez->assume(satgen.signals_eq(big_lhs, big_rhs, 1)); } void setup(int timestep = -1) @@ -250,7 +251,7 @@ struct SatHelper log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); - ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); + ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); // 0 = sets_def // 1 = sets_any_undef @@ -310,28 +311,36 @@ struct SatHelper log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig)); std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep); if (t == 0) - ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig))); + ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_sig))); if (t == 1) - ez.assume(ez.expression(ezSAT::OpOr, undef_sig)); + ez->assume(ez->expression(ezSAT::OpOr, undef_sig)); if (t == 2) - ez.assume(ez.expression(ezSAT::OpAnd, undef_sig)); + ez->assume(ez->expression(ezSAT::OpAnd, undef_sig)); } int import_cell_counter = 0; - for (auto &c : module->cells_) - if (design->selected(module, c.second)) { - // log("Import cell: %s\n", RTLIL::id2cstr(c.first)); - if (satgen.importCell(c.second, timestep)) { - for (auto &p : c.second->connections()) - if (ct.cell_output(c.second->type, p.first)) - show_drivers.insert(sigmap(p.second), c.second); + for (auto cell : module->cells()) + if (design->selected(module, cell)) { + // log("Import cell: %s\n", RTLIL::id2cstr(cell->name)); + if (satgen.importCell(cell, timestep)) { + for (auto &p : cell->connections()) + if (ct.cell_output(cell->type, p.first)) + show_drivers.insert(sigmap(p.second), cell); import_cell_counter++; } else if (ignore_unknown_cells) - log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); + log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); else - log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); + log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); } log("Imported %d cells to SAT database.\n", import_cell_counter); + + if (set_assumes) { + RTLIL::SigSpec assumes_a, assumes_en; + satgen.getAssumes(assumes_a, assumes_en, timestep); + for (int i = 0; i < GetSize(assumes_a); i++) + log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); + ez->assume(satgen.importAssumes(timestep)); + } } int setup_proof(int timestep = -1) @@ -401,7 +410,7 @@ struct SatHelper std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep); for (size_t i = 0; i < value_lhs.size(); i++) - prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i)))))); + prove_bits.push_back(ez->OR(undef_lhs.at(i), ez->AND(ez->NOT(undef_rhs.at(i)), ez->NOT(ez->XOR(value_lhs.at(i), value_rhs.at(i)))))); } if (prove_asserts) { @@ -412,22 +421,22 @@ struct SatHelper prove_bits.push_back(satgen.importAsserts(timestep)); } - return ez.expression(ezSAT::OpAnd, prove_bits); + return ez->expression(ezSAT::OpAnd, prove_bits); } void force_unique_state(int timestep_from, int timestep_to) { RTLIL::SigSpec state_signals = satgen.initial_state.export_all(); for (int i = timestep_from; i < timestep_to; i++) - ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to))); + ez->assume(ez->NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to))); } bool solve(const std::vector<int> &assumptions) { log_assert(gotTimeout == false); - ez.setSolverTimeout(timeout); - bool success = ez.solve(modelExpressions, modelValues, assumptions); - if (ez.getSolverTimoutStatus()) + ez->setSolverTimeout(timeout); + bool success = ez->solve(modelExpressions, modelValues, assumptions); + if (ez->getSolverTimoutStatus()) gotTimeout = true; return success; } @@ -435,9 +444,9 @@ struct SatHelper bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0) { log_assert(gotTimeout == false); - ez.setSolverTimeout(timeout); - bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f); - if (ez.getSolverTimoutStatus()) + ez->setSolverTimeout(timeout); + bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f); + if (ez->getSolverTimoutStatus()) gotTimeout = true; return success; } @@ -478,7 +487,7 @@ struct SatHelper maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i)); backupValues.swap(modelValues); - if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef))) + if (!solve(ez->expression(ezSAT::OpAnd, must_undef), ez->expression(ezSAT::OpOr, maybe_undef))) break; } @@ -597,8 +606,8 @@ struct SatHelper int maxModelWidth = 10; for (auto &info : modelInfo) { - maxModelName = std::max(maxModelName, int(info.description.size())); - maxModelWidth = std::max(maxModelWidth, info.width); + maxModelName = max(maxModelName, int(info.description.size())); + maxModelWidth = max(maxModelWidth, info.width); } log("\n"); @@ -621,11 +630,11 @@ struct SatHelper "---------------------------------------------------------------------------------------------------"; if (last_timestep == -2) { log(max_timestep > 0 ? " Time " : " "); - log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin"); + log("%-*s %11s %9s %*s\n", maxModelName+5, "Signal Name", "Dec", "Hex", maxModelWidth+3, "Bin"); } log(max_timestep > 0 ? " ---- " : " "); - log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10, - hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline); + log("%*.*s %11.11s %9.9s %*.*s\n", maxModelName+5, maxModelName+5, + hline, hline, hline, maxModelWidth+3, maxModelWidth+3, hline); last_timestep = info.timestep; } @@ -638,9 +647,9 @@ struct SatHelper log(" "); if (info.width <= 32 && !found_undef) - log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str()); + log("%-*s %11d %9x %*s\n", maxModelName+5, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+3, value.as_string().c_str()); else - log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str()); + log("%-*s %11s %9s %*s\n", maxModelName+5, info.description.c_str(), "--", "--", maxModelWidth+3, value.as_string().c_str()); } if (last_timestep == -2) @@ -671,7 +680,7 @@ struct SatHelper fprintf(f, " %s\n", stime); fprintf(f, "$end\n"); fprintf(f, "$version\n"); - fprintf(f, " Generated by %s\n", yosys_version_str); + fprintf(f, " Generated by %s\n", yosys_version_str); fprintf(f, "$end\n"); fprintf(f, "$comment\n"); fprintf(f, " Generated from SAT problem in module %s (declared at %s)\n", @@ -750,6 +759,80 @@ struct SatHelper fclose(f); } + void dump_model_to_json(std::string json_file_name) + { + FILE *f = fopen(json_file_name.c_str(), "w"); + if (!f) + log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno)); + + log("Dumping SAT model to WaveJSON file '%s'.\n", json_file_name.c_str()); + + int mintime = 1, maxtime = 0, maxwidth = 0;; + dict<string, pair<int, dict<int, Const>>> wavedata; + + for (auto &info : modelInfo) + { + Const value; + for (int i = 0; i < info.width; i++) { + value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0); + if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i)) + value.bits.back() = RTLIL::State::Sx; + } + + wavedata[info.description].first = info.width; + wavedata[info.description].second[info.timestep] = value; + mintime = min(mintime, info.timestep); + maxtime = max(maxtime, info.timestep); + maxwidth = max(maxwidth, info.width); + } + + fprintf(f, "{ \"signal\": ["); + bool fist_wavedata = true; + for (auto &wd : wavedata) + { + fprintf(f, "%s", fist_wavedata ? "\n" : ",\n"); + fist_wavedata = false; + + vector<string> data; + string name = wd.first.c_str(); + while (name.substr(0, 1) == "\\") + name = name.substr(1); + + fprintf(f, " { \"name\": \"%s\", \"wave\": \"", name.c_str()); + for (int i = mintime; i <= maxtime; i++) { + if (wd.second.second.count(i)) { + string this_data = wd.second.second[i].as_string(); + char ch = '='; + if (wd.second.first == 1) + ch = this_data[0]; + if (!data.empty() && data.back() == this_data) { + fprintf(f, "."); + } else { + data.push_back(this_data); + fprintf(f, "%c", ch); + } + } else { + data.push_back(""); + fprintf(f, "4"); + } + } + if (wd.second.first != 1) { + fprintf(f, "\", \"data\": ["); + for (int i = 0; i < GetSize(data); i++) + fprintf(f, "%s\"%s\"", i ? ", " : "", data[i].c_str()); + fprintf(f, "] }"); + } else { + fprintf(f, "\" }"); + } + } + fprintf(f, "\n ],\n"); + fprintf(f, " \"config\": {\n"); + fprintf(f, " \"hscale\": %.2f\n", maxwidth / 4.0); + fprintf(f, " }\n"); + fprintf(f, "}\n"); + fclose(f); + } + void invalidate_model(bool max_undef) { std::vector<int> clause; @@ -758,12 +841,12 @@ struct SatHelper int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i); bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i); if (!max_undef || !val_undef) - clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit); + clause.push_back(val_undef ? ez->NOT(bit_undef) : val ? ez->NOT(bit) : bit); } } else for (size_t i = 0; i < modelExpressions.size(); i++) - clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i)); - ez.assume(ez.expression(ezSAT::OpOr, clause)); + clause.push_back(modelValues.at(i) ? ez->NOT(modelExpressions.at(i)) : modelExpressions.at(i)); + ez->assume(ez->expression(ezSAT::OpOr, clause)); } }; @@ -853,6 +936,9 @@ struct SatPass : public Pass { log(" -show-inputs, -show-outputs, -show-ports\n"); log(" add all module (input/output) ports to the list of shown signals\n"); log("\n"); + log(" -show-regs, -show-public, -show-all\n"); + log(" show all registers, show signals with 'public' names, show all signals\n"); + log("\n"); log(" -ignore_div_by_zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); @@ -865,11 +951,17 @@ struct SatPass : public Pass { log(" set up a sequential problem with <N> time steps. The steps will\n"); log(" be numbered from 1 to N.\n"); log("\n"); + log(" note: for large <N> it can be significantly faster to use\n"); + log(" -tempinduct-baseonly -maxsteps <N> instead of -seq <N>.\n"); + log("\n"); log(" -set-at <N> <signal> <value>\n"); log(" -unset-at <N> <signal>\n"); log(" set or unset the specified signal to the specified value in the\n"); log(" given timestep. this has priority over a -set for the same signal.\n"); log("\n"); + log(" -set-assumes\n"); + log(" set all assumptions provided via $assume cells\n"); + log("\n"); log(" -set-def-at <N> <signal>\n"); log(" -set-any-undef-at <N> <signal>\n"); log(" -set-all-undef-at <N> <signal>\n"); @@ -890,6 +982,9 @@ struct SatPass : public Pass { log(" -dump_vcd <vcd-file-name>\n"); log(" dump SAT model (counter example in proof) to VCD file\n"); log("\n"); + log(" -dump_json <json-file-name>\n"); + log(" dump SAT model (counter example in proof) to a WaveJSON file.\n"); + log("\n"); log(" -dump_cnf <cnf-file-name>\n"); log(" dump CNF of SAT problem (in DIMACS format). in temporal induction\n"); log(" proofs this is the CNF of the first induction step.\n"); @@ -898,7 +993,7 @@ struct SatPass : public Pass { log("is passed, a temporal induction proof is performed.\n"); log("\n"); log(" -tempinduct\n"); - log(" Perform a temporal induction proof. In a temporalinduction proof it is\n"); + log(" Perform a temporal induction proof. In a temporal induction proof it is\n"); log(" proven that the condition holds forever after the number of time steps\n"); log(" specified using -seq.\n"); log("\n"); @@ -906,12 +1001,26 @@ struct SatPass : public Pass { log(" Perform a temporal induction proof. Assume an initial state with all\n"); log(" registers set to defined values for the induction step.\n"); log("\n"); + log(" -tempinduct-baseonly\n"); + log(" Run only the basecase half of temporal induction (requires -maxsteps)\n"); + log("\n"); + log(" -tempinduct-inductonly\n"); + log(" Run only the induction half of temporal induction\n"); + log("\n"); + log(" -tempinduct-skip <N>\n"); + log(" Skip the first <N> steps of the induction proof.\n"); + log("\n"); + log(" note: this will assume that the base case holds for <N> steps.\n"); + log(" this must be proven independently with \"-tempinduct-baseonly\n"); + log(" -maxsteps <N>\". Use -initsteps if you just want to set a\n"); + log(" minimal induction length.\n"); + log("\n"); log(" -prove <signal> <value>\n"); log(" Attempt to proof that <signal> is always <value>.\n"); log("\n"); log(" -prove-x <signal> <value>\n"); log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n"); - log(" the right hand side. Useful for equivialence checking.\n"); + log(" the right hand side. Useful for equivalence checking.\n"); log("\n"); log(" -prove-asserts\n"); log(" Prove that all asserts in the design hold.\n"); @@ -924,6 +1033,13 @@ struct SatPass : public Pass { log("\n"); log(" -initsteps <N>\n"); log(" Set initial length for the induction.\n"); + log(" This will speed up the search of the right induction length\n"); + log(" for deep induction proofs.\n"); + log("\n"); + log(" -stepsize <N>\n"); + log(" Increase the size of the induction proof in steps of <N>.\n"); + log(" This will speed up the search of the right induction length\n"); + log(" for deep induction proofs.\n"); log("\n"); log(" -timeout <N>\n"); log(" Maximum number of seconds a single SAT instance may take.\n"); @@ -951,10 +1067,13 @@ struct SatPass : public Pass { bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false; bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false; bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false; + bool show_regs = false, show_public = false, show_all = false; bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false; - std::string vcd_file_name, cnf_file_name; + bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false; + int tempinduct_skip = 0, stepsize = 1; + std::string vcd_file_name, json_file_name, cnf_file_name; - log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); + log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -996,6 +1115,10 @@ struct SatPass : public Pass { initsteps = atoi(args[++argidx].c_str()); continue; } + if (args[argidx] == "-stepsize" && argidx+1 < args.size()) { + stepsize = max(1, atoi(args[++argidx].c_str())); + continue; + } if (args[argidx] == "-ignore_div_by_zero") { ignore_div_by_zero = true; continue; @@ -1035,6 +1158,10 @@ struct SatPass : public Pass { enable_undef = true; continue; } + if (args[argidx] == "-set-assumes") { + set_assumes = true; + continue; + } if (args[argidx] == "-tempinduct") { tempinduct = true; continue; @@ -1044,6 +1171,20 @@ struct SatPass : public Pass { tempinduct_def = true; continue; } + if (args[argidx] == "-tempinduct-baseonly") { + tempinduct = true; + tempinduct_baseonly = true; + continue; + } + if (args[argidx] == "-tempinduct-inductonly") { + tempinduct = true; + tempinduct_inductonly = true; + continue; + } + if (args[argidx] == "-tempinduct-skip" && argidx+1 < args.size()) { + tempinduct_skip = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-prove" && argidx+2 < args.size()) { std::string lhs = args[++argidx]; std::string rhs = args[++argidx]; @@ -1135,6 +1276,18 @@ struct SatPass : public Pass { show_outputs = true; continue; } + if (args[argidx] == "-show-regs") { + show_regs = true; + continue; + } + if (args[argidx] == "-show-public") { + show_public = true; + continue; + } + if (args[argidx] == "-show-all") { + show_all = true; + continue; + } if (args[argidx] == "-ignore_unknown_cells") { ignore_unknown_cells = true; continue; @@ -1143,6 +1296,10 @@ struct SatPass : public Pass { vcd_file_name = args[++argidx]; continue; } + if (args[argidx] == "-dump_json" && argidx+1 < args.size()) { + json_file_name = args[++argidx]; + continue; + } if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) { cnf_file_name = args[++argidx]; continue; @@ -1152,14 +1309,12 @@ struct SatPass : public Pass { extra_args(args, argidx, design); RTLIL::Module *module = NULL; - for (auto &mod_it : design->modules_) - if (design->selected(mod_it.second)) { - if (module) - log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n", - RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first)); - module = mod_it.second; - } - if (module == NULL) + for (auto mod : design->selected_modules()) { + if (module) + log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod)); + module = mod; + } + if (module == NULL) log_cmd_error("Can't perform SAT on an empty selection!\n"); if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct) @@ -1192,6 +1347,29 @@ struct SatPass : public Pass { shows.push_back(it.second->name.str()); } + if (show_regs) { + pool<Wire*> reg_wires; + for (auto cell : module->cells()) { + if (cell->type == "$dff" || cell->type.substr(0, 6) == "$_DFF_") + for (auto bit : cell->getPort("\\Q")) + if (bit.wire) + reg_wires.insert(bit.wire); + } + for (auto wire : reg_wires) + shows.push_back(wire->name.str()); + } + + if (show_public) { + for (auto wire : module->wires()) + if (wire->name[0] == '\\') + shows.push_back(wire->name.str()); + } + + if (show_all) { + for (auto wire : module->wires()) + shows.push_back(wire->name.str()); + } + if (tempinduct) { if (loopcount > 0 || max_undef) @@ -1199,8 +1377,10 @@ struct SatPass : public Pass { SatHelper basecase(design, module, enable_undef); SatHelper inductstep(design, module, enable_undef); + bool basecase_setup_init = true; basecase.sets = sets; + basecase.set_assumes = set_assumes; basecase.prove = prove; basecase.prove_x = prove_x; basecase.prove_asserts = prove_asserts; @@ -1222,10 +1402,11 @@ struct SatPass : public Pass { basecase.ignore_unknown_cells = ignore_unknown_cells; for (int timestep = 1; timestep <= seq_len; timestep++) - basecase.setup(timestep); - basecase.setup_init(); + if (!tempinduct_inductonly) + basecase.setup(timestep); inductstep.sets = sets; + inductstep.set_assumes = set_assumes; inductstep.prove = prove; inductstep.prove_x = prove_x; inductstep.prove_asserts = prove_asserts; @@ -1237,12 +1418,14 @@ struct SatPass : public Pass { inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero; inductstep.ignore_unknown_cells = ignore_unknown_cells; - inductstep.setup(1); - inductstep.ez.assume(inductstep.setup_proof(1)); + if (!tempinduct_baseonly) { + inductstep.setup(1); + inductstep.ez->assume(inductstep.setup_proof(1)); + } if (tempinduct_def) { std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1); - inductstep.ez.assume(inductstep.ez.NOT(inductstep.ez.expression(ezSAT::OpOr, undef_state))); + inductstep.ez->assume(inductstep.ez->NOT(inductstep.ez->expression(ezSAT::OpOr, undef_state))); } for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++) @@ -1251,81 +1434,120 @@ struct SatPass : public Pass { // phase 1: proving base case - basecase.setup(seq_len + inductlen); - int property = basecase.setup_proof(seq_len + inductlen); - basecase.generate_model(); - - if (inductlen > 1) - basecase.force_unique_state(seq_len + 1, seq_len + inductlen); + if (!tempinduct_inductonly) + { + basecase.setup(seq_len + inductlen); + int property = basecase.setup_proof(seq_len + inductlen); + basecase.generate_model(); - log("\n[base case] Solving problem with %d variables and %d clauses..\n", - basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses()); + if (basecase_setup_init) { + basecase.setup_init(); + basecase_setup_init = false; + } - if (basecase.solve(basecase.ez.NOT(property))) { - log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); - print_proof_failed(); - basecase.print_model(); - if(!vcd_file_name.empty()) - basecase.dump_model_to_vcd(vcd_file_name); - goto tip_failed; - } + if (inductlen > 1) + basecase.force_unique_state(seq_len + 1, seq_len + inductlen); - if (basecase.gotTimeout) - goto timeout; + if (tempinduct_skip < inductlen) + { + log("\n[base case %d] Solving problem with %d variables and %d clauses..\n", + inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); + + if (basecase.solve(basecase.ez->NOT(property))) { + log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); + print_proof_failed(); + basecase.print_model(); + if(!vcd_file_name.empty()) + basecase.dump_model_to_vcd(vcd_file_name); + if(!json_file_name.empty()) + basecase.dump_model_to_json(json_file_name); + goto tip_failed; + } + + if (basecase.gotTimeout) + goto timeout; - log("Base case for induction length %d proven.\n", inductlen); - basecase.ez.assume(property); + log("Base case for induction length %d proven.\n", inductlen); + } + else + { + log("\n[base case %d] Skipping prove for this step (-tempinduct-skip %d).", + inductlen, tempinduct_skip); + log("\n[base case %d] Problem size so far: %d variables and %d clauses.\n", + inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); + } + basecase.ez->assume(property); + } // phase 2: proving induction step - inductstep.setup(inductlen + 1); - property = inductstep.setup_proof(inductlen + 1); - inductstep.generate_model(); - - if (inductlen > 1) - inductstep.force_unique_state(1, inductlen + 1); - - if (inductlen < initsteps) - { - log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n", - inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); - inductstep.ez.assume(property); - } - else + if (!tempinduct_baseonly) { - if (!cnf_file_name.empty()) - { - FILE *f = fopen(cnf_file_name.c_str(), "w"); - if (!f) - log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); + inductstep.setup(inductlen + 1); + int property = inductstep.setup_proof(inductlen + 1); + inductstep.generate_model(); - log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); - cnf_file_name.clear(); + if (inductlen > 1) + inductstep.force_unique_state(1, inductlen + 1); - inductstep.ez.printDIMACS(f, false); - fclose(f); + if (inductlen <= tempinduct_skip || inductlen <= initsteps || inductlen % stepsize != 0) + { + if (inductlen < tempinduct_skip) + log("\n[induction step %d] Skipping prove for this step (-tempinduct-skip %d).", + inductlen, tempinduct_skip); + if (inductlen < initsteps) + log("\n[induction step %d] Skipping prove for this step (-initsteps %d).", + inductlen, tempinduct_skip); + if (inductlen % stepsize != 0) + log("\n[induction step %d] Skipping prove for this step (-stepsize %d).", + inductlen, stepsize); + log("\n[induction step %d] Problem size so far: %d variables and %d clauses.\n", + inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); + inductstep.ez->assume(property); } - - log("\n[induction step] Solving problem with %d variables and %d clauses..\n", - inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses()); - - if (!inductstep.solve(inductstep.ez.NOT(property))) { - if (inductstep.gotTimeout) - goto timeout; - log("Induction step proven: SUCCESS!\n"); - print_qed(); - goto tip_success; + else + { + if (!cnf_file_name.empty()) + { + FILE *f = fopen(cnf_file_name.c_str(), "w"); + if (!f) + log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno)); + + log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); + cnf_file_name.clear(); + + inductstep.ez->printDIMACS(f, false); + fclose(f); + } + + log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n", + inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); + + if (!inductstep.solve(inductstep.ez->NOT(property))) { + if (inductstep.gotTimeout) + goto timeout; + log("Induction step proven: SUCCESS!\n"); + print_qed(); + goto tip_success; + } + + log("Induction step failed. Incrementing induction length.\n"); + inductstep.ez->assume(property); + inductstep.print_model(); } - - log("Induction step failed. Incrementing induction length.\n"); - inductstep.ez.assume(property); - inductstep.print_model(); } } + if (tempinduct_baseonly) { + log("\nReached maximum number of time steps -> proved base case for %d steps: SUCCESS!\n", maxsteps); + goto tip_success; + } + log("\nReached maximum number of time steps -> proof failed.\n"); if(!vcd_file_name.empty()) inductstep.dump_model_to_vcd(vcd_file_name); + if(!json_file_name.empty()) + inductstep.dump_model_to_json(json_file_name); print_proof_failed(); tip_failed: @@ -1349,6 +1571,7 @@ struct SatPass : public Pass { SatHelper sathelper(design, module, enable_undef); sathelper.sets = sets; + sathelper.set_assumes = set_assumes; sathelper.prove = prove; sathelper.prove_x = prove_x; sathelper.prove_asserts = prove_asserts; @@ -1372,7 +1595,7 @@ struct SatPass : public Pass { if (seq_len == 0) { sathelper.setup(); if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) - sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); + sathelper.ez->assume(sathelper.ez->NOT(sathelper.setup_proof())); } else { std::vector<int> prove_bits; for (int timestep = 1; timestep <= seq_len; timestep++) { @@ -1382,7 +1605,7 @@ struct SatPass : public Pass { prove_bits.push_back(sathelper.setup_proof(timestep)); } if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) - sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits))); + sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits))); sathelper.setup_init(); } sathelper.generate_model(); @@ -1396,7 +1619,7 @@ struct SatPass : public Pass { log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str()); cnf_file_name.clear(); - sathelper.ez.printDIMACS(f, false); + sathelper.ez->printDIMACS(f, false); fclose(f); } @@ -1404,7 +1627,7 @@ struct SatPass : public Pass { rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", - sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); + sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses()); if (sathelper.solve()) { @@ -1424,6 +1647,8 @@ struct SatPass : public Pass { if(!vcd_file_name.empty()) sathelper.dump_model_to_vcd(vcd_file_name); + if(!json_file_name.empty()) + sathelper.dump_model_to_json(json_file_name); if (loopcount != 0) { loopcount--, rerun_counter++; @@ -1487,5 +1712,5 @@ struct SatPass : public Pass { } } } SatPass; - + PRIVATE_NAMESPACE_END |