riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Gracefully report error when module has nothing to prove.

This commit is contained in:
Alberto Gonzalez 2020-04-01 21:33:54 +00:00
parent 8f0f13cad2
commit 1db73e8dd2
No known key found for this signature in database
GPG Key ID: 8395A8BA109708B2
1 changed files with 8 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
passes/sat/qbfsat.cc
View File

@ -300,10 +300,11 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
return ret; return ret;
} }
std::set<std::string> validate_design_and_get_inputs(RTLIL::Module *module) { std::set<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
bool found_input = false; bool found_input = false;
bool found_hole = false; bool found_hole = false;
bool found_1bit_output = false; bool found_1bit_output = false;
bool found_assert_assume = false;
std::set<std::string> input_wires; std::set<std::string> input_wires;
for (auto wire : module->wires()) { for (auto wire : module->wires()) {
if (wire->port_input) { if (wire->port_input) {
@ -319,14 +320,16 @@ std::set<std::string> validate_design_and_get_inputs(RTLIL::Module *module) {
if (cell->type == "$anyconst") if (cell->type == "$anyconst")
found_hole = true; found_hole = true;
if (cell->type.in("$assert", "$assume")) if (cell->type.in("$assert", "$assume"))
found_1bit_output = true; found_assert_assume = true;
} }
if (!found_input) if (!found_input)
log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n"); log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
if (!found_hole) if (!found_hole)
log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n"); log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
if (!found_1bit_output) if (!found_1bit_output && !found_assert_assume)
log_cmd_error("Did not find any single-bit outputs, assert()s, or assume()s. Is this a miter circuit?\n"); log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
if (!found_assert_assume && !opt.assume_outputs)
log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
return input_wires; return input_wires;
} }
@ -485,7 +488,7 @@ struct QbfSatPass : public Pass {
Pass::call(design, "design -duplicate"); Pass::call(design, "design -duplicate");
//Replace input wires with wires assigned $allconst cells. //Replace input wires with wires assigned $allconst cells.
std::set<std::string> input_wires = validate_design_and_get_inputs(module); std::set<std::string> input_wires = validate_design_and_get_inputs(module, opt);
allconstify_inputs(module, input_wires); allconstify_inputs(module, input_wires);
if (opt.assume_outputs) if (opt.assume_outputs)
assume_miter_outputs(module); assume_miter_outputs(module);