summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-03 16:26:10 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-03 16:26:10 +0100
commit9e350215857b56fa990dc8a0eabfd2087f9dc39a (patch)
tree304144f06c0fdaa2d15734ee3e79e7636a94f2d4 /passes/sat
parenta6750b375301f2c2ebb51a2496cdf2c820b2546b (diff)
Addred sat option -ignore_unknown_cells
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/sat.cc20
1 files changed, 17 insertions, 3 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index f5c8f50b..389d01b9 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -50,7 +50,7 @@ struct SatHelper
bool prove_asserts;
// undef constraints
- bool enable_undef, set_init_undef;
+ bool enable_undef, set_init_undef, ignore_unknown_cells;
std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
@@ -67,6 +67,7 @@ struct SatHelper
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
set_init_undef = false;
+ ignore_unknown_cells = false;
max_timestep = -1;
timeout = 0;
gotTimeout = false;
@@ -277,8 +278,10 @@ struct SatHelper
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));
+ } 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));
+ else
+ log_error("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);
}
@@ -699,6 +702,9 @@ struct SatPass : public Pass {
log(" -ignore_div_by_zero\n");
log(" ignore all solutions that involve a division by zero\n");
log("\n");
+ log(" -ignore_unknown_cells\n");
+ log(" ignore all cells that can not be matched to a SAT model\n");
+ log("\n");
log("The following options can be used to set up a sequential problem:\n");
log("\n");
log(" -seq <N>\n");
@@ -762,6 +768,7 @@ 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, max_undef = false;
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
+ bool ignore_unknown_cells = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -909,6 +916,10 @@ struct SatPass : public Pass {
show_outputs = true;
continue;
}
+ if (args[argidx] == "-ignore_unknown_cells") {
+ ignore_unknown_cells = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -976,6 +987,7 @@ struct SatPass : public Pass {
basecase.sets_init = sets_init;
basecase.set_init_undef = set_init_undef;
basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
+ basecase.ignore_unknown_cells = ignore_unknown_cells;
for (int timestep = 1; timestep <= seq_len; timestep++)
basecase.setup(timestep);
@@ -991,6 +1003,7 @@ struct SatPass : public Pass {
inductstep.sets_any_undef = sets_any_undef;
inductstep.sets_all_undef = sets_all_undef;
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));
@@ -1085,6 +1098,7 @@ struct SatPass : public Pass {
sathelper.sets_init = sets_init;
sathelper.set_init_undef = set_init_undef;
sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
+ sathelper.ignore_unknown_cells = ignore_unknown_cells;
if (seq_len == 0) {
sathelper.setup();