mirror of https://github.com/YosysHQ/yosys.git
Added "sat -tempinduct-baseonly -tempinduct-inductonly"
This commit is contained in:
Clifford Wolf
parent
dcbd00c101
commit
1688b9b464
|
|
@ -984,6 +984,12 @@ struct SatPass : public Pass {
|
||||||
log(" Perform a temporal induction proof. Assume an initial state with all\n");
|
log(" Perform a temporal induction proof. Assume an initial state with all\n");
|
||||||
log(" registers set to defined values for the induction step.\n");
|
log(" registers set to defined values for the induction step.\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
|
log(" -tempinduct-baseonly\n");
|
||||||
|
log(" Run only the basecase half of temporal induction (requires -maxsteps)\n");
|
||||||
|
log("\n");
|
||||||
|
log(" -tempinduct-inductonly\n");
|
||||||
|
log(" Run only the induction half of temporal induction\n");
|
||||||
|
log("\n");
|
||||||
log(" -prove <signal> <value>\n");
|
log(" -prove <signal> <value>\n");
|
||||||
log(" Attempt to proof that <signal> is always <value>.\n");
|
log(" Attempt to proof that <signal> is always <value>.\n");
|
||||||
log("\n");
|
log("\n");
|
||||||
|
|
@ -1030,6 +1036,7 @@ struct SatPass : public Pass {
|
||||||
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
|
bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
|
||||||
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
|
bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
|
||||||
bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
|
bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
|
||||||
|
bool tempinduct_baseonly = false, tempinduct_inductonly = false;
|
||||||
std::string vcd_file_name, json_file_name, cnf_file_name;
|
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("Executing SAT pass (solving SAT problems in the circuit).\n");
|
||||||
|
|
@ -1122,6 +1129,16 @@ struct SatPass : public Pass {
|
||||||
tempinduct_def = true;
|
tempinduct_def = true;
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
if (args[argidx] == "-tempinduct-baseonly") {
|
||||||
|
tempinduct = true;
|
||||||
|
tempinduct_baseonly = true;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
if (args[argidx] == "-tempinduct-inductonly") {
|
||||||
|
tempinduct = true;
|
||||||
|
tempinduct_inductonly = true;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
if (args[argidx] == "-prove" && argidx+2 < args.size()) {
|
if (args[argidx] == "-prove" && argidx+2 < args.size()) {
|
||||||
std::string lhs = args[++argidx];
|
std::string lhs = args[++argidx];
|
||||||
std::string rhs = args[++argidx];
|
std::string rhs = args[++argidx];
|
||||||
|
|
@ -1305,7 +1322,8 @@ struct SatPass : public Pass {
|
||||||
basecase.ignore_unknown_cells = ignore_unknown_cells;
|
basecase.ignore_unknown_cells = ignore_unknown_cells;
|
||||||
|
|
||||||
for (int timestep = 1; timestep <= seq_len; timestep++)
|
for (int timestep = 1; timestep <= seq_len; timestep++)
|
||||||
basecase.setup(timestep);
|
if (!tempinduct_inductonly)
|
||||||
|
basecase.setup(timestep);
|
||||||
|
|
||||||
inductstep.sets = sets;
|
inductstep.sets = sets;
|
||||||
inductstep.prove = prove;
|
inductstep.prove = prove;
|
||||||
|
|
@ -1319,8 +1337,10 @@ struct SatPass : public Pass {
|
||||||
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
|
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
|
||||||
inductstep.ignore_unknown_cells = ignore_unknown_cells;
|
inductstep.ignore_unknown_cells = ignore_unknown_cells;
|
||||||
|
|
||||||
inductstep.setup(1);
|
if (!tempinduct_baseonly) {
|
||||||
inductstep.ez->assume(inductstep.setup_proof(1));
|
inductstep.setup(1);
|
||||||
|
inductstep.ez->assume(inductstep.setup_proof(1));
|
||||||
|
}
|
||||||
|
|
||||||
if (tempinduct_def) {
|
if (tempinduct_def) {
|
||||||
std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
|
std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
|
||||||
|
|
@ -1333,82 +1353,88 @@ struct SatPass : public Pass {
|
||||||
|
|
||||||
// phase 1: proving base case
|
// phase 1: proving base case
|
||||||
|
|
||||||
basecase.setup(seq_len + inductlen);
|
if (!tempinduct_inductonly)
|
||||||
int property = basecase.setup_proof(seq_len + inductlen);
|
{
|
||||||
basecase.generate_model();
|
basecase.setup(seq_len + inductlen);
|
||||||
|
int property = basecase.setup_proof(seq_len + inductlen);
|
||||||
|
basecase.generate_model();
|
||||||
|
|
||||||
if (basecase_setup_init) {
|
if (basecase_setup_init) {
|
||||||
basecase.setup_init();
|
basecase.setup_init();
|
||||||
basecase_setup_init = false;
|
basecase_setup_init = false;
|
||||||
|
}
|
||||||
|
|
||||||
|
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();
|
||||||
|
if(!vcd_file_name.empty())
|
||||||
|
basecase.dump_model_to_vcd(vcd_file_name);
|
||||||
|
if(!json_file_name.empty())
|
||||||
|
basecase.dump_model_to_json(json_file_name);
|
||||||
|
goto tip_failed;
|
||||||
|
}
|
||||||
|
|
||||||
|
if (basecase.gotTimeout)
|
||||||
|
goto timeout;
|
||||||
|
|
||||||
|
log("Base case for induction length %d proven.\n", inductlen);
|
||||||
|
basecase.ez->assume(property);
|
||||||
}
|
}
|
||||||
|
|
||||||
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();
|
|
||||||
if(!vcd_file_name.empty())
|
|
||||||
basecase.dump_model_to_vcd(vcd_file_name);
|
|
||||||
if(!json_file_name.empty())
|
|
||||||
basecase.dump_model_to_json(json_file_name);
|
|
||||||
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
|
// phase 2: proving induction step
|
||||||
|
|
||||||
inductstep.setup(inductlen + 1);
|
if (!tempinduct_baseonly)
|
||||||
property = inductstep.setup_proof(inductlen + 1);
|
|
||||||
inductstep.generate_model();
|
|
||||||
|
|
||||||
if (inductlen > 1)
|
|
||||||
inductstep.force_unique_state(1, inductlen + 1);
|
|
||||||
|
|
||||||
if (inductlen < initsteps)
|
|
||||||
{
|
{
|
||||||
log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
|
inductstep.setup(inductlen + 1);
|
||||||
inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
|
int property = inductstep.setup_proof(inductlen + 1);
|
||||||
inductstep.ez->assume(property);
|
inductstep.generate_model();
|
||||||
}
|
|
||||||
else
|
if (inductlen > 1)
|
||||||
{
|
inductstep.force_unique_state(1, inductlen + 1);
|
||||||
if (!cnf_file_name.empty())
|
|
||||||
|
if (inductlen < initsteps)
|
||||||
{
|
{
|
||||||
FILE *f = fopen(cnf_file_name.c_str(), "w");
|
log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
|
||||||
if (!f)
|
inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
|
||||||
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
|
inductstep.ez->assume(property);
|
||||||
|
|
||||||
log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
|
|
||||||
cnf_file_name.clear();
|
|
||||||
|
|
||||||
inductstep.ez->printDIMACS(f, false);
|
|
||||||
fclose(f);
|
|
||||||
}
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
if (!cnf_file_name.empty())
|
||||||
|
{
|
||||||
|
FILE *f = fopen(cnf_file_name.c_str(), "w");
|
||||||
|
if (!f)
|
||||||
|
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
|
||||||
|
|
||||||
log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
|
log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
|
||||||
inductstep.ez->numCnfVariables(), inductstep.ez->numCnfClauses());
|
cnf_file_name.clear();
|
||||||
|
|
||||||
if (!inductstep.solve(inductstep.ez->NOT(property))) {
|
inductstep.ez->printDIMACS(f, false);
|
||||||
if (inductstep.gotTimeout)
|
fclose(f);
|
||||||
goto timeout;
|
}
|
||||||
log("Induction step proven: SUCCESS!\n");
|
|
||||||
print_qed();
|
log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
|
||||||
goto tip_success;
|
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("Induction step failed. Incrementing induction length.\n");
|
|
||||||
inductstep.ez->assume(property);
|
|
||||||
inductstep.print_model();
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue