diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/aiger.cc | 38 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 4 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 12 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 29 |
4 files changed, 72 insertions, 11 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index c323691a3..dfe506c66 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -100,7 +100,7 @@ struct AigerWriter return aig_map.at(bit); } - AigerWriter(Module *module, bool zinit_mode) : module(module), zinit_mode(zinit_mode), sigmap(module) + AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module) { pool<SigBit> undriven_bits; pool<SigBit> unused_bits; @@ -293,6 +293,10 @@ struct AigerWriter aig_map[bit] = 2*aig_m; } + if (imode && input_bits.empty()) { + aig_m++, aig_i++; + } + if (zinit_mode) { for (auto it : ff_map) { @@ -371,6 +375,11 @@ struct AigerWriter aig_outputs.push_back(bit2aig(bit)); } + if (omode && output_bits.empty()) { + aig_o++; + aig_outputs.push_back(0); + } + for (auto it : asserts) { aig_b++; int bit_a = bit2aig(it.first); @@ -378,6 +387,11 @@ struct AigerWriter aig_outputs.push_back(mkgate(bit_a^1, bit_en)); } + if (bmode && asserts.empty()) { + aig_b++; + aig_outputs.push_back(0); + } + for (auto it : assumes) { aig_c++; int bit_a = bit2aig(it.first); @@ -689,6 +703,11 @@ struct AigerBackend : public Backend { log(" -vmap <filename>\n"); log(" like -map, but more verbose\n"); log("\n"); + log(" -I, -O, -B\n"); + log(" If the design contains no input/output/assert then create one\n"); + log(" dummy input/output/bad_state pin to make the tools reading the\n"); + log(" AIGER file happy.\n"); + log("\n"); } void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE { @@ -697,6 +716,9 @@ struct AigerBackend : public Backend { bool miter_mode = false; bool symbols_mode = false; bool verbose_map = false; + bool imode = false; + bool omode = false; + bool bmode = false; std::string map_filename; log_header(design, "Executing AIGER backend.\n"); @@ -729,6 +751,18 @@ struct AigerBackend : public Backend { verbose_map = true; continue; } + if (args[argidx] == "-I") { + imode = true; + continue; + } + if (args[argidx] == "-O") { + omode = true; + continue; + } + if (args[argidx] == "-B") { + bmode = true; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -738,7 +772,7 @@ struct AigerBackend : public Backend { if (top_module == nullptr) log_error("Can't find top module in current design!\n"); - AigerWriter writer(top_module, zinit_mode); + AigerWriter writer(top_module, zinit_mode, imode, omode, bmode); writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode); if (!map_filename.empty()) { diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e2777ae04..418f8d766 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -554,7 +554,9 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - /* FIXME */ + return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + "(bvlshr A B) (bvlshr A (bvneg B)))", + GetSize(cell->getPort("\\B")), 0), 's'); } else { return export_bvop(cell, "(bvlshr A B)", 's'); } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 6af2a5ac1..b944ee004 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -1259,7 +1259,11 @@ elif covermode: smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) print_msg("Re-solving with appended steps..") - assert smt_check_sat() == "sat" + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + found_failed_assert = True + retstatus = False + break reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) assert len(reached_covers) == len(cover_desc) @@ -1377,7 +1381,11 @@ else: # not tempind, covermode smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i)) smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i)) smt_assert_consequent(get_constr_expr(constr_assumes, i)) - assert smt_check_sat() == "sat" + print_msg("Re-solving with appended steps..") + if smt_check_sat() == "unsat": + print("%s Cannot appended steps without violating assumptions!" % smt.timestamp()) + retstatus = False + break print_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 3fc823e3e..68783e744 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -31,11 +31,19 @@ from threading import Thread # does not run out of stack frames when parsing large expressions if os.name == "posix": smtio_reclimit = 64 * 1024 - smtio_stacksize = 128 * 1024 * 1024 if sys.getrecursionlimit() < smtio_reclimit: sys.setrecursionlimit(smtio_reclimit) - if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize: - resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1)) + + current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK) + if current_rlimit_stack[0] != resource.RLIM_INFINITY: + smtio_stacksize = 128 * 1024 * 1024 + if os.uname().sysname == "Darwin": + # MacOS has rather conservative stack limits + smtio_stacksize = 16 * 1024 * 1024 + if current_rlimit_stack[1] != resource.RLIM_INFINITY: + smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1]) + if current_rlimit_stack[0] < smtio_stacksize: + resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1])) # currently running solvers (so we can kill them) @@ -158,19 +166,28 @@ class SmtIo: self.unroll = False if self.solver == "yices": - self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['yices-smt2'] + self.solver_opts + else: + self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts if self.solver == "z3": self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts if self.solver == "cvc4": - self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + else: + self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts if self.solver == "mathsat": self.popen_vargs = ['mathsat'] + self.solver_opts if self.solver == "boolector": - self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts + else: + self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.unroll = True if self.solver == "abc": |