/* * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. * */ // [[CITE]] Temporal Induction by Incremental SAT Solving // Niklas Een and Niklas Sörensson (2003) // http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.8161 #include "kernel/register.h" #include "kernel/celltypes.h" #include "kernel/consteval.h" #include "kernel/sigtools.h" #include "kernel/log.h" #include "kernel/satgen.h" #include #include #include namespace { struct SatHelper { RTLIL::Design *design; RTLIL::Module *module; ezDefaultSAT ez; SigMap sigmap; CellTypes ct; SatGen satgen; // additional constraints std::vector> sets, prove; std::map>> sets_at; std::map> unsets_at; // model variables std::vector shows; SigPool show_signal_pool; SigSet show_drivers; int max_timestep, timeout; bool gotTimeout; SatHelper(RTLIL::Design *design, RTLIL::Module *module) : design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap) { max_timestep = -1; timeout = 0; gotTimeout = false; } void setup(int timestep = -1) { if (timestep > 0) log ("\nSetting up time step %d:\n", timestep); else log ("\nSetting up SAT problem:\n"); if (timestep > max_timestep) max_timestep = timestep; RTLIL::SigSpec big_lhs, big_rhs; for (auto &s : sets) { RTLIL::SigSpec lhs, rhs; if (!RTLIL::SigSpec::parse(lhs, 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.width != rhs.width) 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.width, s.second.c_str(), log_signal(rhs), rhs.width); 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); } for (auto &s : sets_at[timestep]) { RTLIL::SigSpec lhs, rhs; if (!RTLIL::SigSpec::parse(lhs, 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.width != rhs.width) 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.width, s.second.c_str(), log_signal(rhs), rhs.width); log("Import set-constraint for timestep: %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 : unsets_at[timestep]) { RTLIL::SigSpec lhs; if (!RTLIL::SigSpec::parse(lhs, module, s)) log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str()); show_signal_pool.add(sigmap(lhs)); log("Import unset-constraint for timestep: %s\n", log_signal(lhs)); big_lhs.remove2(lhs, &big_rhs); } log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); std::vector lhs_vec = satgen.importSigSpec(big_lhs, timestep); std::vector rhs_vec = satgen.importSigSpec(big_rhs, timestep); ez.assume(ez.vec_eq(lhs_vec, rhs_vec)); 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); import_cell_counter++; } else log("Warning: failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type)); } log("Imported %d cells to SAT database.\n", import_cell_counter); } int setup_proof(int timestep = -1) { assert(prove.size() > 0); RTLIL::SigSpec big_lhs, big_rhs; for (auto &s : prove) { RTLIL::SigSpec lhs, rhs; if (!RTLIL::SigSpec::parse(lhs, module, s.first)) log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str()); if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second)) log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str()); show_signal_pool.add(sigmap(lhs)); show_signal_pool.add(sigmap(rhs)); if (lhs.width != rhs.width) log_cmd_error("Proof 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.width, s.second.c_str(), log_signal(rhs), rhs.width); log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs)); big_lhs.remove2(lhs, &big_rhs); big_lhs.append(lhs); big_rhs.append(rhs); } log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs)); std::vector lhs_vec = satgen.importSigSpec(big_lhs, timestep); std::vector rhs_vec = satgen.importSigSpec(big_rhs, timestep); return ez.vec_eq(lhs_vec, rhs_vec); } 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.vec_ne(satgen.importSigSpec(state_signals, i), satgen.importSigSpec(state_signals, timestep_to))); } bool solve(const std::vector &assumptions) { log_assert(gotTimeout == false); ez.setSolverTimeout(timeout); bool success = ez.solve(modelExpressions, modelValues, assumptions); if (ez.getSolverTimoutStatus()) gotTimeout = true; return success; } 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()) gotTimeout = true; return success; } struct ModelBlockInfo { int timestep, offset, width; std::string description; bool operator < (const ModelBlockInfo &other) const { if (timestep != other.timestep) return timestep < other.timestep; if (description != other.description) return description < other.description; if (offset != other.offset) return offset < other.offset; if (width != other.width) return width < other.width; return false; } }; std::vector modelExpressions; std::vector modelValues; std::set modelInfo; void generate_model() { RTLIL::SigSpec modelSig; modelExpressions.clear(); modelInfo.clear(); // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals if (shows.size() == 0) { SigPool queued_signals, handled_signals, final_signals; queued_signals = show_signal_pool; while (queued_signals.size() > 0) { RTLIL::SigSpec sig = queued_signals.export_one(); queued_signals.del(sig); handled_signals.add(sig); std::set drivers = show_drivers.find(sig); if (drivers.size() == 0) { final_signals.add(sig); } else { for (auto &d : drivers) for (auto &p : d->connections) { if (d->type == "$dff" && p.first == "\\CLK") continue; if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C") continue; queued_signals.add(handled_signals.remove(sigmap(p.second))); } } } modelSig = final_signals.export_all(); // additionally add all set and prove signals directly // (it improves user confidence if we write the constraints back ;-) modelSig.append(show_signal_pool.export_all()); } else { for (auto &s : shows) { RTLIL::SigSpec sig; if (!RTLIL::SigSpec::parse(sig, module, s)) log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str()); log("Import show expression: %s\n", log_signal(sig)); modelSig.append(sig); } } modelSig.sort_and_unify(); // log("Model signals: %s\n", log_signal(modelSig)); for (auto &c : modelSig.chunks) if (c.wire != NULL) { ModelBlockInfo info; RTLIL::SigSpec chunksig = c; info.width = chunksig.width; info.description = log_signal(chunksig); for (int timestep = -1; timestep <= max_timestep; timestep++) { if ((timestep == -1 && max_timestep > 0) || timestep == 0) continue; std::vector vec = satgen.importSigSpec(chunksig, timestep); info.timestep = timestep; info.offset = modelExpressions.size(); modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end()); modelInfo.insert(info); } } // Add zero step signals as collected by satgen modelSig = satgen.initial_state.export_all(); for (auto &c : modelSig.chunks) if (c.wire != NULL) { ModelBlockInfo info; RTLIL::SigSpec chunksig = c; info.timestep = 0; info.offset = modelExpressions.size(); info.width = chunksig.width; info.description = log_signal(chunksig); std::vector vec = satgen.importSigSpec(chunksig, 1); modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end()); modelInfo.insert(info); } } void print_model() { int maxModelName = 10; int maxModelWidth = 10; for (auto &info : modelInfo) { maxModelName = std::max(maxModelName, int(info.description.size())); maxModelWidth = std::max(maxModelWidth, info.width); } log("\n"); int last_timestep = -2; for (auto &info : modelInfo) { RTLIL::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 (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i)) value.bits.back() = RTLIL::State::Sx; } if (info.timestep != last_timestep) { const char *hline = "---------------------------------------------------------------------------------------------------" "---------------------------------------------------------------------------------------------------" "---------------------------------------------------------------------------------------------------"; 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(max_timestep > 0 ? " ---- " : " "); log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10, hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline); last_timestep = info.timestep; } if (max_timestep > 0) { if (info.timestep > 0) log(" %4d ", info.timestep); else log(" init "); } else log(" "); if (info.width <= 32) 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()); else log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str()); } if (last_timestep == -2) log(" no model variables selected for display.\n"); } void invalidate_model() { std::vector clause; 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)); } }; } /* namespace */ static void print_proof_failed() { log("\n"); log(" ______ ___ ___ _ _ _ _ \n"); log(" (_____ \\ / __) / __) (_) | | | |\n"); log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n"); log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n"); log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n"); log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n"); log("\n"); } static void print_timeout() { log("\n"); log(" _____ _ _ _____ ____ _ _____\n"); log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n"); log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n"); log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n"); log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n"); log("\n"); } static void print_qed() { log("\n"); log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n"); log(" /$$__ $$ | $$_____/ | $$__ $$ \n"); log(" | $$ \\ $$ | $$ | $$ \\ $$ \n"); log(" | $$ | $$ | $$$$$ | $$ | $$ \n"); log(" | $$ | $$ | $$__/ | $$ | $$ \n"); log(" | $$/$$ $$ | $$ | $$ | $$ \n"); log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n"); log(" \\____ $$$|__/|________/|__/|_______/|__/\n"); log(" \\__/ \n"); log("\n"); } struct SatPass : public Pass { SatPass() : Pass("sat", "solve a SAT problem in the circuit") { } virtual void help() { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); log(" sat [options] [selection]\n"); log("\n"); log("This command solves a SAT problem defined over the currently selected circuit\n"); log("and additional constraints passed as parameters.\n"); log("\n"); log(" -all\n"); log(" show all solutions to the problem (this can grow exponentially, use\n"); log(" -max instead to get solutions)\n"); log("\n"); log(" -max \n"); log(" like -all, but limit number of solutions to \n"); log("\n"); log(" -set \n"); log(" set the specified signal to the specified value.\n"); log("\n"); log(" -show \n"); log(" show the model for the specified signal. if no -show option is\n"); log(" passed then a set of signals to be shown is automatically selected.\n"); log("\n"); log(" -ignore_div_by_zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); log("The following options can be used to set up a sequential problem:\n"); log("\n"); log(" -seq \n"); log(" set up a sequential problem with time steps. The steps will\n"); log(" be numbered from 1 to N.\n"); log("\n"); log(" -set-at \n"); log(" -unset-at \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("The following additional options can be used to set up a proof. If also -seq\n"); log("is passed, a temporal induction proof is performed.\n"); log("\n"); log(" -prove \n"); log(" Attempt to proof that is always . In a temporal\n"); log(" induction proof it is proven that the condition holds forever after\n"); log(" the number of time steps passed using -seq.\n"); log("\n"); log(" -maxsteps \n"); log(" Set a maximum length for the induction.\n"); log("\n"); log(" -timeout \n"); log(" Maximum number of seconds a single SAT instance may take.\n"); log("\n"); log(" -verify\n"); log(" Return an error and stop the synthesis script if the proof fails.\n"); log("\n"); log(" -verify-no-timeout\n"); log(" Like -verify but do not return an error for timeouts.\n"); log("\n"); } virtual void execute(std::vector args, RTLIL::Design *design) { std::vector> sets, prove; std::map>> sets_at; std::map> unsets_at; std::vector shows; int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; bool verify = false, fail_on_timeout = false, ignore_div_by_zero = false; log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-all") { loopcount = -1; continue; } if (args[argidx] == "-verify") { fail_on_timeout = true; verify = true; continue; } if (args[argidx] == "-verify-no-timeout") { verify = true; continue; } if (args[argidx] == "-timeout" && argidx+1 < args.size()) { timeout = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-max" && argidx+1 < args.size()) { loopcount = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) { maxsteps = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-ignore_div_by_zero" && argidx+1 < args.size()) { ignore_div_by_zero = true; continue; } if (args[argidx] == "-set" && argidx+2 < args.size()) { std::string lhs = args[++argidx].c_str(); std::string rhs = args[++argidx].c_str(); sets.push_back(std::pair(lhs, rhs)); continue; } if (args[argidx] == "-prove" && argidx+2 < args.size()) { std::string lhs = args[++argidx].c_str(); std::string rhs = args[++argidx].c_str(); prove.push_back(std::pair(lhs, rhs)); continue; } if (args[argidx] == "-seq" && argidx+1 < args.size()) { seq_len = atoi(args[++argidx].c_str()); continue; } if (args[argidx] == "-set-at" && argidx+3 < args.size()) { int timestep = atoi(args[++argidx].c_str()); std::string lhs = args[++argidx].c_str(); std::string rhs = args[++argidx].c_str(); sets_at[timestep].push_back(std::pair(lhs, rhs)); continue; } if (args[argidx] == "-unset-at" && argidx+2 < args.size()) { int timestep = atoi(args[++argidx].c_str()); std::string lhs = args[++argidx].c_str(); unsets_at[timestep].push_back(lhs); continue; } if (args[argidx] == "-show" && argidx+1 < args.size()) { shows.push_back(args[++argidx]); continue; } break; } 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) log_cmd_error("Can't perform SAT on an empty selection!\n"); if (prove.size() == 0 && verify) log_cmd_error("Got -verify but nothing to prove!\n"); if (prove.size() > 0 && seq_len > 0) { if (loopcount > 0) log_cmd_error("The options -max and -all are not supported for temporal induction proofs!\n"); SatHelper basecase(design, module); SatHelper inductstep(design, module); basecase.sets = sets; basecase.prove = prove; basecase.sets_at = sets_at; basecase.unsets_at = unsets_at; basecase.shows = shows; basecase.timeout = timeout; basecase.satgen.ignore_div_by_zero = ignore_div_by_zero; for (int timestep = 1; timestep <= seq_len; timestep++) basecase.setup(timestep); inductstep.sets = sets; inductstep.prove = prove; inductstep.shows = shows; inductstep.timeout = timeout; inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero; inductstep.setup(1); inductstep.ez.assume(inductstep.setup_proof(1)); for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++) { log("\n** Trying induction with length %d **\n", inductlen); // 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); log("\n[base case] Solving problem with %d variables and %d clauses..\n", 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(); goto tip_failed; } if (basecase.gotTimeout) goto timeout; log("Base case for induction length %d proven.\n", inductlen); 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); 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; } log("Induction step failed. Incrementing induction length.\n"); inductstep.ez.assume(property); inductstep.print_model(); } log("\nReached maximum number of time steps -> proof failed.\n"); print_proof_failed(); tip_failed: if (verify) { log("\n"); log_error("Called with -verify and proof did fail!\n"); } tip_success:; } else { if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); SatHelper sathelper(design, module); sathelper.sets = sets; sathelper.prove = prove; sathelper.sets_at = sets_at; sathelper.unsets_at = unsets_at; sathelper.shows = shows; sathelper.timeout = timeout; sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero; if (seq_len == 0) { sathelper.setup(); if (sathelper.prove.size() > 0) sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); } else { for (int timestep = 1; timestep <= seq_len; timestep++) sathelper.setup(timestep); } sathelper.generate_model(); #if 0 // print CNF for debugging sathelper.ez.printDIMACS(stdout, true); #endif bool did_rerun = false; rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); if (sathelper.solve()) { if (prove.size() == 0) { log("SAT solving finished - model found:\n"); } else { log("SAT proof finished - model found: FAIL!\n"); print_proof_failed(); } sathelper.print_model(); if (loopcount != 0) { loopcount--, did_rerun = true; sathelper.invalidate_model(); goto rerun_solver; } if (verify) { log("\n"); log_error("Called with -verify and proof did fail!\n"); } } else { if (sathelper.gotTimeout) goto timeout; if (did_rerun) log("SAT solving finished - no more models found.\n"); else if (prove.size() == 0) log("SAT solving finished - no model found.\n"); else { log("SAT proof finished - no model found: SUCCESS!\n"); print_qed(); } } if (verify && did_rerun) { log("\n"); log_error("Called with -verify and proof did fail!\n"); } } if (0) { timeout: log("Interrupted SAT solver: TIMEOUT!\n"); print_timeout(); if (fail_on_timeout) log_error("Called with -verify and proof did time out!\n"); } } } SatPass;