diff options
Diffstat (limited to 'passes/sat/sat.cc')
-rw-r--r-- | passes/sat/sat.cc | 217 |
1 files changed, 107 insertions, 110 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 2e9c6d2f..a6ac7afd 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -90,106 +90,16 @@ struct SatHelper log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig)); } - void setup_init() - { - log ("\nSetting up initial state:\n"); - - RTLIL::SigSpec big_lhs, big_rhs; - - for (auto &it : module->wires_) - { - if (it.second->attributes.count("\\init") == 0) - continue; - - RTLIL::SigSpec lhs = sigmap(it.second); - RTLIL::SigSpec rhs = it.second->attributes.at("\\init"); - log_assert(lhs.size() == rhs.size()); - - RTLIL::SigSpec removed_bits; - for (int i = 0; i < lhs.size(); i++) { - RTLIL::SigSpec bit = lhs.extract(i, 1); - if (!satgen.initial_state.check_all(bit)) { - removed_bits.append(bit); - lhs.remove(i, 1); - rhs.remove(i, 1); - i--; - } - } - - if (removed_bits.size()) - log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits)); - - if (lhs.size()) { - log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs)); - big_lhs.remove2(lhs, &big_rhs); - big_lhs.append(lhs); - big_rhs.append(rhs); - } - } - - for (auto &s : sets_init) - { - RTLIL::SigSpec lhs, rhs; - - if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first)) - log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str()); - if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second)) - log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str()); - show_signal_pool.add(sigmap(lhs)); - show_signal_pool.add(sigmap(rhs)); - - if (lhs.size() != rhs.size()) - log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n", - s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size()); - - log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs)); - big_lhs.remove2(lhs, &big_rhs); - big_lhs.append(lhs); - big_rhs.append(rhs); - } - - if (!satgen.initial_state.check_all(big_lhs)) { - RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs); - log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem)); - } - - if (set_init_def) { - RTLIL::SigSpec rem = satgen.initial_state.export_all(); - std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1); - ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem))); - } - - if (set_init_undef) { - RTLIL::SigSpec rem = satgen.initial_state.export_all(); - rem.remove(big_lhs); - big_lhs.append(rem); - big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size())); - } - - if (set_init_zero) { - RTLIL::SigSpec rem = satgen.initial_state.export_all(); - rem.remove(big_lhs); - big_lhs.append(rem); - big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size())); - } - - if (big_lhs.size() == 0) { - log("No constraints for initial state found.\n\n"); - return; - } - - log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs)); - check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); - ez->assume(satgen.signals_eq(big_lhs, big_rhs, 1)); - } - - void setup(int timestep = -1) + void setup(int timestep = -1, bool initstate = false) { if (timestep > 0) log ("\nSetting up time step %d:\n", timestep); else log ("\nSetting up SAT problem:\n"); + if (initstate) + satgen.setInitState(timestep); + if (timestep > max_timestep) max_timestep = timestep; @@ -341,6 +251,97 @@ struct SatHelper log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); ez->assume(satgen.importAssumes(timestep)); } + + if (initstate) + { + RTLIL::SigSpec big_lhs, big_rhs; + + for (auto &it : module->wires_) + { + if (it.second->attributes.count("\\init") == 0) + continue; + + RTLIL::SigSpec lhs = sigmap(it.second); + RTLIL::SigSpec rhs = it.second->attributes.at("\\init"); + log_assert(lhs.size() == rhs.size()); + + RTLIL::SigSpec removed_bits; + for (int i = 0; i < lhs.size(); i++) { + RTLIL::SigSpec bit = lhs.extract(i, 1); + if (!satgen.initial_state.check_all(bit)) { + removed_bits.append(bit); + lhs.remove(i, 1); + rhs.remove(i, 1); + i--; + } + } + + if (removed_bits.size()) + log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits)); + + if (lhs.size()) { + log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs)); + big_lhs.remove2(lhs, &big_rhs); + big_lhs.append(lhs); + big_rhs.append(rhs); + } + } + + for (auto &s : sets_init) + { + RTLIL::SigSpec lhs, rhs; + + if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first)) + log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str()); + if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second)) + log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str()); + show_signal_pool.add(sigmap(lhs)); + show_signal_pool.add(sigmap(rhs)); + + if (lhs.size() != rhs.size()) + log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n", + s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size()); + + log("Import init set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs)); + big_lhs.remove2(lhs, &big_rhs); + big_lhs.append(lhs); + big_rhs.append(rhs); + } + + if (!satgen.initial_state.check_all(big_lhs)) { + RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs); + log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem)); + } + + if (set_init_def) { + RTLIL::SigSpec rem = satgen.initial_state.export_all(); + std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1); + ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_rem))); + } + + if (set_init_undef) { + RTLIL::SigSpec rem = satgen.initial_state.export_all(); + rem.remove(big_lhs); + big_lhs.append(rem); + big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size())); + } + + if (set_init_zero) { + RTLIL::SigSpec rem = satgen.initial_state.export_all(); + rem.remove(big_lhs); + big_lhs.append(rem); + big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size())); + } + + if (big_lhs.size() == 0) { + log("No constraints for initial state found.\n\n"); + return; + } + + log("Final init constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); + check_undef_enabled(big_lhs), check_undef_enabled(big_rhs); + ez->assume(satgen.signals_eq(big_lhs, big_rhs, timestep)); + } } int setup_proof(int timestep = -1) @@ -630,11 +631,11 @@ struct SatHelper "---------------------------------------------------------------------------------------------------"; if (last_timestep == -2) { log(max_timestep > 0 ? " Time " : " "); - log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin"); + log("%-*s %11s %9s %*s\n", maxModelName+5, "Signal Name", "Dec", "Hex", maxModelWidth+3, "Bin"); } log(max_timestep > 0 ? " ---- " : " "); - log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10, - hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline); + log("%*.*s %11.11s %9.9s %*.*s\n", maxModelName+5, maxModelName+5, + hline, hline, hline, maxModelWidth+3, maxModelWidth+3, hline); last_timestep = info.timestep; } @@ -647,9 +648,9 @@ struct SatHelper log(" "); if (info.width <= 32 && !found_undef) - log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str()); + log("%-*s %11d %9x %*s\n", maxModelName+5, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+3, value.as_string().c_str()); else - log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str()); + log("%-*s %11s %9s %*s\n", maxModelName+5, info.description.c_str(), "--", "--", maxModelWidth+3, value.as_string().c_str()); } if (last_timestep == -2) @@ -1073,7 +1074,7 @@ struct SatPass : public Pass { int tempinduct_skip = 0, stepsize = 1; std::string vcd_file_name, json_file_name, cnf_file_name; - log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); + log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -1377,7 +1378,6 @@ struct SatPass : public Pass { SatHelper basecase(design, module, enable_undef); SatHelper inductstep(design, module, enable_undef); - bool basecase_setup_init = true; basecase.sets = sets; basecase.set_assumes = set_assumes; @@ -1403,7 +1403,7 @@ struct SatPass : public Pass { for (int timestep = 1; timestep <= seq_len; timestep++) if (!tempinduct_inductonly) - basecase.setup(timestep); + basecase.setup(timestep, timestep == 1); inductstep.sets = sets; inductstep.set_assumes = set_assumes; @@ -1436,15 +1436,10 @@ struct SatPass : public Pass { if (!tempinduct_inductonly) { - basecase.setup(seq_len + inductlen); + basecase.setup(seq_len + inductlen, seq_len + inductlen == 1); int property = basecase.setup_proof(seq_len + inductlen); basecase.generate_model(); - if (basecase_setup_init) { - basecase.setup_init(); - basecase_setup_init = false; - } - if (inductlen > 1) basecase.force_unique_state(seq_len + 1, seq_len + inductlen); @@ -1452,6 +1447,7 @@ struct SatPass : public Pass { { log("\n[base case %d] Solving problem with %d variables and %d clauses..\n", inductlen, basecase.ez->numCnfVariables(), basecase.ez->numCnfClauses()); + log_flush(); if (basecase.solve(basecase.ez->NOT(property))) { log("SAT temporal induction proof finished - model found for base case: FAIL!\n"); @@ -1522,6 +1518,7 @@ struct SatPass : public Pass { log("\n[induction step %d] Solving problem with %d variables and %d clauses..\n", inductlen, inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses()); + log_flush(); if (!inductstep.solve(inductstep.ez->NOT(property))) { if (inductstep.gotTimeout) @@ -1599,14 +1596,13 @@ struct SatPass : public Pass { } else { std::vector<int> prove_bits; for (int timestep = 1; timestep <= seq_len; timestep++) { - sathelper.setup(timestep); + sathelper.setup(timestep, timestep == 1); if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) if (timestep > prove_skip) prove_bits.push_back(sathelper.setup_proof(timestep)); } if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) sathelper.ez->assume(sathelper.ez->NOT(sathelper.ez->expression(ezSAT::OpAnd, prove_bits))); - sathelper.setup_init(); } sathelper.generate_model(); @@ -1628,6 +1624,7 @@ struct SatPass : public Pass { rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", sathelper.ez->numCnfVariables(), sathelper.ez->numCnfClauses()); + log_flush(); if (sathelper.solve()) { |