From: Clifford Wolf Date: Sun, 9 Jun 2013 14:30:37 +0000 (+0200) Subject: Added support for non-temporal proofs to sat_solve X-Git-Tag: yosys-0.2.0~593 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b210234612beb3e20d5338d03debf084c9b6c7b9;p=yosys.git Added support for non-temporal proofs to sat_solve --- diff --git a/passes/sat/example.ys b/passes/sat/example.ys index dd1a117f8..19f8f50ee 100644 --- a/passes/sat/example.ys +++ b/passes/sat/example.ys @@ -5,3 +5,7 @@ sat_solve -set y 1'b1 example002 sat_solve -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003 sat_solve -set y 1'b1 example004 sat_solve -show rst,counter -set-at 3 y 1'b1 -seq 4 example004 + +sat_solve -prove y 1'b0 example001 +# sat_solve -show rst,counter -prove y 1'b0 -set-at 1 rst 1'b1 -seq 1 example004 + diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc index 20f797421..bd8ffb6da 100644 --- a/passes/sat/sat_solve.cc +++ b/passes/sat/sat_solve.cc @@ -116,7 +116,7 @@ struct SatHelper SatGen satgen; // additional constraints - std::vector> sets; + std::vector> sets, prove; std::map>> sets_at; std::map> unsets_at; @@ -222,6 +222,41 @@ struct SatHelper log("Imported %d cells to SAT database.\n", import_cell_counter); } + void setup_proof(int timestep = -1) + { + if (prove.size() == 0) + return; + + RTLIL::SigSpec big_lhs, big_rhs; + + for (auto &s : prove) + { + RTLIL::SigSpec lhs, rhs; + + if (!parse_sigstr(lhs, module, s.first)) + log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str()); + if (!parse_sigstr(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); + ez.assume(ez.vec_ne(lhs_vec, rhs_vec)); + } + bool solve() { return ez.solve(modelExpressions, modelValues); @@ -418,14 +453,26 @@ struct SatSolvePass : public Pass { 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(" -verify\n"); + log(" Return an error and stop the synthesis script if the proof fails.\n"); + log("\n"); } virtual void execute(std::vector args, RTLIL::Design *design) { - std::vector> sets; + std::vector> sets, prove; std::map>> sets_at; std::map> unsets_at; std::vector shows; int loopcount = 0, seq_len = 0; + bool verify = false; log_header("Executing SAT_SOLVE pass (solving SAT problems in the circuit).\n"); @@ -435,6 +482,10 @@ struct SatSolvePass : public Pass { loopcount = -1; continue; } + if (args[argidx] == "-verify") { + verify = true; + continue; + } if (args[argidx] == "-max" && argidx+1 < args.size()) { loopcount = atoi(args[++argidx].c_str()); continue; @@ -445,6 +496,12 @@ struct SatSolvePass : public Pass { 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; @@ -478,40 +535,80 @@ struct SatSolvePass : 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 SAT_SOLVE on an empty selection!\n"); - SatHelper sathelper(design, module); - sathelper.sets = sets; - sathelper.sets_at = sets_at; - sathelper.unsets_at = unsets_at; - sathelper.shows = shows; + if (prove.size() == 0 && verify) + log_cmd_error("Got -verify but nothing to prove!\n"); - if (seq_len == 0) - sathelper.setup(); + if (prove.size() > 0 && seq_len > 0) + { + log_cmd_error("Temporal induction proofs are not implemented yet!\n"); + } else - for (int timestep = 1; timestep <= seq_len; timestep++) - sathelper.setup(timestep); - sathelper.generate_model(); + { + SatHelper sathelper(design, module); + sathelper.sets = sets; + sathelper.prove = prove; + sathelper.sets_at = sets_at; + sathelper.unsets_at = unsets_at; + sathelper.shows = shows; + + if (seq_len == 0) { + sathelper.setup(); + 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); + // print CNF for debugging + sathelper.ez.printDIMACS(stdout, true); #endif rerun_solver: - log("\nSolving problem with %d variables and %d clauses..\n", - sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses()); - if (sathelper.solve()) { - log("SAT solving finished - model found:\n"); - sathelper.print_model(); - if (loopcount != 0) { - loopcount--; - sathelper.invalidate_model(); - goto 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"); + log("\n"); + log(" ______ ___ ___ _ _ _ _ \n"); + log(" (_____ \\ / __) / __) (_) | | | |\n"); + log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n"); + log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n"); + log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n"); + log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n"); + log("\n"); + } + + sathelper.print_model(); + + if (verify) { + log("\n"); + log_error("Called with -verify and proof did fail!\n"); + } + + if (loopcount != 0) { + loopcount--; + sathelper.invalidate_model(); + goto rerun_solver; + } } - } else - log("SAT solving finished - no model 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"); + } + } } } SatSolvePass;