From 2b90ba1e96eb46ac0dcd9070f46a9451bd45868a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 7 Dec 2013 23:58:55 +0100 Subject: Added sat -max_undef feature --- passes/sat/sat.cc | 61 +++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 50 insertions(+), 11 deletions(-) (limited to 'passes') diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index bb82c308..e330dfa6 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -296,6 +296,29 @@ struct SatHelper std::vector modelValues; std::set modelInfo; + void maximize_undefs() + { + log_assert(enable_undef); + std::vector backupValues; + + while (1) + { + std::vector must_undef, maybe_undef; + + for (size_t i = 0; i < modelExpressions.size()/2; i++) + if (modelValues.at(modelExpressions.size()/2 + i)) + must_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i)); + else + 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))) + break; + } + + backupValues.swap(modelValues); + } + void generate_model() { RTLIL::SigSpec modelSig; @@ -458,14 +481,15 @@ struct SatHelper log(" no model variables selected for display.\n"); } - void invalidate_model() + void invalidate_model(bool max_undef) { std::vector clause; if (enable_undef) { for (size_t i = 0; i < modelExpressions.size()/2; i++) { 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); - clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit); + if (!max_undef || !val_undef) + clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit); } } else for (size_t i = 0; i < modelExpressions.size(); i++) @@ -536,6 +560,10 @@ struct SatPass : public Pass { log(" enable modeling of undef value (aka 'x-bits')\n"); log(" this option is implied by -set-def, -set-undef et. cetera\n"); log("\n"); + log(" -max_undef\n"); + log(" maximize the number of undef bits in solutions, giving a better\n"); + log(" picture of which input bits are actually vital to the solution.\n"); + log("\n"); log(" -set \n"); log(" set the specified signal to the specified value.\n"); log("\n"); @@ -609,7 +637,8 @@ struct SatPass : public Pass { std::map> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at; std::vector shows, sets_def, sets_undef, sets_all_undef; int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; - bool verify = false, fail_on_timeout = false, enable_undef = false, ignore_div_by_zero = false, set_init_undef = false; + bool verify = false, fail_on_timeout = false, enable_undef = false; + bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true; log_header("Executing SAT pass (solving SAT problems in the circuit).\n"); @@ -648,6 +677,11 @@ struct SatPass : public Pass { enable_undef = true; continue; } + if (args[argidx] == "-max_undef") { + enable_undef = true; + max_undef = true; + continue; + } if (args[argidx] == "-set" && argidx+2 < args.size()) { std::string lhs = args[++argidx]; std::string rhs = args[++argidx]; @@ -744,8 +778,8 @@ struct SatPass : public Pass { 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"); + if (loopcount > 0 || max_undef) + log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n"); SatHelper basecase(design, module, enable_undef); SatHelper inductstep(design, module, enable_undef); @@ -892,7 +926,7 @@ struct SatPass : public Pass { sathelper.ez.printDIMACS(stdout, true); #endif - bool did_rerun = false; + int rerun_counter = 0; rerun_solver: log("\nSolving problem with %d variables and %d clauses..\n", @@ -900,6 +934,11 @@ struct SatPass : public Pass { if (sathelper.solve()) { + if (max_undef) { + log("SAT model found. maximizing number of undefs.\n"); + sathelper.maximize_undefs(); + } + if (prove.size() == 0) { log("SAT solving finished - model found:\n"); } else { @@ -910,8 +949,8 @@ struct SatPass : public Pass { sathelper.print_model(); if (loopcount != 0) { - loopcount--, did_rerun = true; - sathelper.invalidate_model(); + loopcount--, rerun_counter++; + sathelper.invalidate_model(max_undef); goto rerun_solver; } @@ -924,8 +963,8 @@ struct SatPass : public Pass { { if (sathelper.gotTimeout) goto timeout; - if (did_rerun) - log("SAT solving finished - no more models found.\n"); + if (rerun_counter) + log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter); else if (prove.size() == 0) log("SAT solving finished - no model found.\n"); else { @@ -934,7 +973,7 @@ struct SatPass : public Pass { } } - if (verify && did_rerun) { + if (verify && rerun_counter) { log("\n"); log_error("Called with -verify and proof did fail!\n"); } -- cgit v1.2.3