From b13e6bd375dc19fc2d6a3e67cdc6c045da732200 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 23 Feb 2018 19:33:30 +0100 Subject: [PATCH] Add smtbmc support for exist-forall problems Signed-off-by: Clifford Wolf --- backends/smt2/smt2.cc | 82 +++++++++-- backends/smt2/smtbmc.py | 282 +++++++++++++++++++++++++++---------- backends/smt2/smtio.py | 57 +++++++- examples/smtbmc/.gitignore | 2 + examples/smtbmc/Makefile | 11 +- examples/smtbmc/demo8.v | 12 ++ 6 files changed, 357 insertions(+), 89 deletions(-) create mode 100644 examples/smtbmc/demo8.v diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a401cacb7..124364120 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -32,9 +32,9 @@ struct Smt2Worker CellTypes ct; SigMap sigmap; RTLIL::Module *module; - bool bvmode, memmode, wiresmode, verbose, statebv, statedt; + bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode; dict &mod_stbv_width; - int idcounter, statebv_width; + int idcounter = 0, statebv_width = 0; std::vector decls, trans, hier, dtmembers; std::map bit_driver; @@ -42,6 +42,7 @@ struct Smt2Worker pool recursive_cells, registers; pool clock_posedge, clock_negedge; + vector ex_state_eq, ex_input_eq; std::map> fcache; std::map memarrays; @@ -106,10 +107,10 @@ struct Smt2Worker decls.push_back(decl_str + "\n"); } - Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode, dict &mod_stbv_width, dict>> &mod_clk_cache) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), - verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0) + verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width) { pool noclock; @@ -507,14 +508,16 @@ struct Smt2Worker return; } - if (cell->type.in("$anyconst", "$anyseq")) + if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq")) { registers.insert(cell); string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell); if (cell->attributes.count("\\reg")) infostr += " " + cell->attributes.at("\\reg").decode_string(); - decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str())); + decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str())); makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))); + if (cell->type == "$anyseq") + ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter)); register_bv(cell->getPort("\\Y"), idcounter++); recursive_cells.erase(cell); return; @@ -787,14 +790,24 @@ struct Smt2Worker if (bvmode && GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); + if (wire->port_input) + ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", + get_id(module), get_id(wire), get_id(module), get_id(wire))); } else { for (int i = 0; i < GetSize(sig); i++) - if (GetSize(sig) > 1) + if (GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str())); - else + if (wire->port_input) + ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", + get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); + } else { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str())); + if (wire->port_input) + ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", + get_id(module), get_id(wire), get_id(module), get_id(wire))); + } } } } @@ -919,6 +932,7 @@ struct Smt2Worker std::string expr_d = get_bool(cell->getPort("\\D")); std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); + ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str())); } if (cell->type.in("$ff", "$dff")) @@ -926,13 +940,16 @@ struct Smt2Worker std::string expr_d = get_bv(cell->getPort("\\D")); std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); + ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str())); } - if (cell->type == "$anyconst") + if (cell->type.in("$anyconst", "$allconst")) { std::string expr_d = get_bv(cell->getPort("\\Y")); std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y")))); + if (cell->type == "$anyconst") + ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str())); } if (cell->type == "$mem") @@ -1044,6 +1061,7 @@ struct Smt2Worker std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports); std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell))); + ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); if (async_read) hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); @@ -1086,6 +1104,37 @@ struct Smt2Worker hier.push_back(stringf(" (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name))); trans.push_back(stringf(" (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n", get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name))); + ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n", + get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name))); + } + + if (forallmode) + { + string expr = ex_state_eq.empty() ? "true" : "(and"; + if (!ex_state_eq.empty()) { + if (GetSize(ex_state_eq) == 1) { + expr = "\n " + ex_state_eq.front() + "\n"; + } else { + for (auto &str : ex_state_eq) + expr += stringf("\n %s", str.c_str()); + expr += "\n)"; + } + } + decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n", + get_id(module), get_id(module), get_id(module), expr.c_str())); + + expr = ex_input_eq.empty() ? "true" : "(and"; + if (!ex_input_eq.empty()) { + if (GetSize(ex_input_eq) == 1) { + expr = "\n " + ex_input_eq.front() + "\n"; + } else { + for (auto &str : ex_input_eq) + expr += stringf("\n %s", str.c_str()); + expr += "\n)"; + } + } + decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n", + get_id(module), get_id(module), get_id(module), expr.c_str())); } string assert_expr = assert_list.empty() ? "true" : "(and"; @@ -1336,6 +1385,7 @@ struct Smt2Backend : public Backend { { std::ifstream template_f; bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false; + bool forallmode = false; log_header(design, "Executing SMT2 backend.\n"); @@ -1443,6 +1493,18 @@ struct Smt2Backend : public Backend { Module *topmod = design->top_module(); std::string topmod_id; + for (auto module : sorted_modules) + for (auto cell : module->cells()) + if (cell->type.in("$allconst", "$allseq")) + goto found_forall; + if (0) { + found_forall: + forallmode = true; + *f << stringf("; yosys-smt2-forall\n"); + if (!statebv && !statedt) + log_error("Forall-exists problems are only supported in -stbv or -stdt mode.\n"); + } + for (auto module : sorted_modules) { if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn()) @@ -1450,7 +1512,7 @@ struct Smt2Backend : public Backend { log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); - Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width, mod_clk_cache); + Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode, mod_stbv_width, mod_clk_cache); worker.run(); worker.write(*f); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 047fb6cde..4ad940551 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -983,7 +983,7 @@ def print_anyconsts_worker(mod, state, path): for fun, info in smt.modinfo[mod].anyconsts.items(): if info[1] is None: - print_msg("Value for anyconst in %s (%s): %d" % (path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) + print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) else: print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state))))) @@ -1010,24 +1010,160 @@ def get_cover_list(mod, base): return cover_expr, cover_desc +states = list() +asserts_antecedent_cache = [list()] +asserts_consequent_cache = [list()] +asserts_cache_dirty = False + +def smt_state(step): + smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) + states.append("s%d" % step) + +def smt_assert_antecedent(expr): + if expr == "true": + return + + smt.write("(assert %s)" % expr) + + global asserts_cache_dirty + asserts_cache_dirty = True + asserts_antecedent_cache[-1].append(expr) + +def smt_assert_consequent(expr): + if expr == "true": + return + + smt.write("(assert %s)" % expr) + + global asserts_cache_dirty + asserts_cache_dirty = True + asserts_consequent_cache[-1].append(expr) + +def smt_forall_assert(): + if not smt.forall: + return + + global asserts_cache_dirty + asserts_cache_dirty = False + + def make_assert_expr(asserts_cache): + expr = list() + for lst in asserts_cache: + expr += lst + + assert len(expr) != 0 + + if len(expr) == 1: + expr = expr[0] + else: + expr = "(and %s)" % (" ".join(expr)) + return expr + + antecedent_expr = make_assert_expr(asserts_antecedent_cache) + consequent_expr = make_assert_expr(asserts_consequent_cache) + + states_db = set(states) + used_states_db = set() + new_antecedent_expr = list() + new_consequent_expr = list() + assert_expr = list() + + def make_new_expr(new_expr, expr): + cursor = 0 + while cursor < len(expr): + l = 1 + if expr[cursor] in '|"': + while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]: + l += 1 + l += 1 + elif expr[cursor] not in '() ': + while cursor+l < len(expr) and expr[cursor+l] not in '|"() ': + l += 1 + + word = expr[cursor:cursor+l] + if word in states_db: + used_states_db.add(word) + word += "_" + + new_expr.append(word) + cursor += l + + make_new_expr(new_antecedent_expr, antecedent_expr) + make_new_expr(new_consequent_expr, consequent_expr) + + new_antecedent_expr = ["".join(new_antecedent_expr)] + new_consequent_expr = ["".join(new_consequent_expr)] + + if states[0] in used_states_db: + new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0])) + for s in states: + if s in used_states_db: + new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s)) + + if len(new_antecedent_expr) == 0: + new_antecedent_expr = "true" + elif len(new_antecedent_expr) == 1: + new_antecedent_expr = new_antecedent_expr[0] + else: + new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr)) + + if len(new_consequent_expr) == 0: + new_consequent_expr = "true" + elif len(new_consequent_expr) == 1: + new_consequent_expr = new_consequent_expr[0] + else: + new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr)) + + assert_expr.append("(assert (forall (") + first_state = True + for s in states: + if s in used_states_db: + assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod)) + first_state = False + assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr)) + + smt.write("".join(assert_expr)) + +def smt_push(): + global asserts_cache_dirty + asserts_cache_dirty = True + asserts_antecedent_cache.append(list()) + asserts_consequent_cache.append(list()) + smt.write("(push 1)") + +def smt_pop(): + global asserts_cache_dirty + asserts_cache_dirty = True + asserts_antecedent_cache.pop() + asserts_consequent_cache.pop() + smt.write("(pop 1)") + +def smt_check_sat(): + if asserts_cache_dirty: + smt_forall_assert() + return smt.check_sat() if tempind: retstatus = False skip_counter = step_size for step in range(num_steps, -1, -1): - smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) - smt.write("(assert (|%s_u| s%d))" % (topmod, step)) - smt.write("(assert (|%s_h| s%d))" % (topmod, step)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) + if smt.forall: + print_msg("Temporal induction not supported for exists-forall problems.") + break + + smt_state(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) + smt_assert_consequent(get_constr_expr(constr_assumes, step)) if step == num_steps: - smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step))) + smt_assert_consequent("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step))) else: - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1)) - smt.write("(assert (|%s_a| s%d))" % (topmod, step)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) + smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1)) + smt_assert_consequent("(|%s_a| s%d)" % (topmod, step)) + smt_assert_consequent(get_constr_expr(constr_asserts, step)) if step > num_steps-skip_steps: print_msg("Skipping induction in step %d.." % (step)) @@ -1041,9 +1177,9 @@ if tempind: skip_counter = 0 print_msg("Trying induction in step %d.." % (step)) - if smt.check_sat() == "sat": + if smt_check_sat() == "sat": if step == 0: - print("%s Temporal induction failed!" % smt.timestamp()) + print_msg("Temporal induction failed!") print_anyconsts(num_steps) print_failed_asserts(num_steps) write_trace(step, num_steps+1, '%') @@ -1054,7 +1190,7 @@ if tempind: write_trace(step, num_steps+1, "%d" % step) else: - print("%s Temporal induction successful." % smt.timestamp()) + print_msg("Temporal induction successful.") retstatus = True break @@ -1079,42 +1215,42 @@ elif covermode: assert step_size == 1 while step < num_steps: - smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) - smt.write("(assert (|%s_u| s%d))" % (topmod, step)) - smt.write("(assert (|%s_h| s%d))" % (topmod, step)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) + smt_state(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) + smt_assert_consequent(get_constr_expr(constr_assumes, step)) if step == 0: if noinit: - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) else: - smt.write("(assert (|%s_i| s0))" % (topmod)) - smt.write("(assert (|%s_is| s0))" % (topmod)) + smt_assert_antecedent("(|%s_i| s0)" % (topmod)) + smt_assert_antecedent("(|%s_is| s0)" % (topmod)) else: - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step)) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) while "1" in cover_mask: print_msg("Checking cover reachability in step %d.." % (step)) - smt.write("(push 1)") - smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc))) + smt_push() + smt_assert_antecedent("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc))) - if smt.check_sat() == "unsat": - smt.write("(pop 1)") + if smt_check_sat() == "unsat": + smt_pop() break if append_steps > 0: for i in range(step+1, step+1+append_steps): print_msg("Appending additional step %d." % i) - smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i)) - smt.write("(assert (|%s_u| s%d))" % (topmod, i)) - smt.write("(assert (|%s_h| s%d))" % (topmod, i)) - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, i)) + smt_state(i) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + 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)) print_msg("Re-solving with appended steps..") - assert smt.check_sat() == "sat" + assert smt_check_sat() == "sat" reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) assert len(reached_covers) == len(cover_desc) @@ -1141,7 +1277,7 @@ elif covermode: break coveridx += 1 - smt.write("(pop 1)") + smt_pop() smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask)) if found_failed_assert: @@ -1162,27 +1298,27 @@ else: # not tempind, covermode step = 0 retstatus = True while step < num_steps: - smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) - smt.write("(assert (|%s_u| s%d))" % (topmod, step)) - smt.write("(assert (|%s_h| s%d))" % (topmod, step)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) + smt_state(step) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step)) + smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step)) + smt_assert_consequent(get_constr_expr(constr_assumes, step)) if step == 0: if noinit: - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) else: - smt.write("(assert (|%s_i| s0))" % (topmod)) - smt.write("(assert (|%s_is| s0))" % (topmod)) + smt_assert_antecedent("(|%s_i| s0)" % (topmod)) + smt_assert_antecedent("(|%s_is| s0)" % (topmod)) else: - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step)) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step)) if step < skip_steps: if assume_skipped is not None and step >= assume_skipped: print_msg("Skipping step %d (and assuming pass).." % (step)) - smt.write("(assert (|%s_a| s%d))" % (topmod, step)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) + smt_assert_consequent("(|%s_a| s%d)" % (topmod, step)) + smt_assert_consequent(get_constr_expr(constr_asserts, step)) else: print_msg("Skipping step %d.." % (step)) step += 1 @@ -1191,12 +1327,12 @@ else: # not tempind, covermode last_check_step = step for i in range(1, step_size): if step+i < num_steps: - smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step+i)) - smt.write("(assert (|%s_u| s%d))" % (topmod, step+i)) - smt.write("(assert (|%s_h| s%d))" % (topmod, step+i)) - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i)) + smt_state(step+i) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i)) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i)) + smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i)) + smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i)) + smt_assert_consequent(get_constr_expr(constr_assumes, step+i)) last_check_step = step+i if not gentrace: @@ -1206,7 +1342,7 @@ else: # not tempind, covermode else: print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step)) - if smt.check_sat() == "unsat": + if smt_check_sat() == "unsat": print("%s Warmup failed!" % smt.timestamp()) retstatus = False break @@ -1216,23 +1352,23 @@ else: # not tempind, covermode print_msg("Checking assertions in step %d.." % (step)) else: print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step)) - smt.write("(push 1)") + smt_push() - smt.write("(assert (not (and %s)))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] + + smt_assert_consequent("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] + [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)])) - if smt.check_sat() == "sat": + if smt_check_sat() == "sat": print("%s BMC failed!" % smt.timestamp()) if append_steps > 0: for i in range(last_check_step+1, last_check_step+1+append_steps): print_msg("Appending additional step %d." % i) - smt.write("(declare-fun s%d () |%s_s|)" % (i, topmod)) - smt.write("(assert (not (|%s_is| s%d)))" % (topmod, i)) - smt.write("(assert (|%s_u| s%d))" % (topmod, i)) - smt.write("(assert (|%s_h| s%d))" % (topmod, i)) - smt.write("(assert (|%s_t| s%d s%d))" % (topmod, i-1, i)) - smt.write("(assert %s)" % get_constr_expr(constr_assumes, i)) - assert smt.check_sat() == "sat" + smt_state(i) + smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i)) + smt_assert_consequent("(|%s_u| s%d)" % (topmod, i)) + 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_anyconsts(step) for i in range(step, last_check_step+1): print_failed_asserts(i) @@ -1240,12 +1376,12 @@ else: # not tempind, covermode retstatus = False break - smt.write("(pop 1)") + smt_pop() if (constr_final_start is not None) or (last_check_step+1 != num_steps): for i in range(step, last_check_step+1): - smt.write("(assert (|%s_a| s%d))" % (topmod, i)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) + smt_assert_consequent("(|%s_a| s%d)" % (topmod, i)) + smt_assert_consequent(get_constr_expr(constr_asserts, i)) if constr_final_start is not None: for i in range(step, last_check_step+1): @@ -1253,12 +1389,12 @@ else: # not tempind, covermode continue print_msg("Checking final constraints in step %d.." % (i)) - smt.write("(push 1)") + smt_push() - smt.write("(assert %s)" % get_constr_expr(constr_assumes, i, final=True)) - smt.write("(assert (not %s))" % get_constr_expr(constr_asserts, i, final=True)) + smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True)) + smt_assert_consequent("(not %s)" % get_constr_expr(constr_asserts, i, final=True)) - if smt.check_sat() == "sat": + if smt_check_sat() == "sat": print("%s BMC failed!" % smt.timestamp()) print_anyconsts(i) print_failed_asserts(i, final=True) @@ -1266,17 +1402,17 @@ else: # not tempind, covermode retstatus = False break - smt.write("(pop 1)") + smt_pop() if not retstatus: break else: # gentrace for i in range(step, last_check_step+1): - smt.write("(assert (|%s_a| s%d))" % (topmod, i)) - smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) + smt_assert_consequent("(|%s_a| s%d)" % (topmod, i)) + smt_assert_consequent(get_constr_expr(constr_asserts, i)) print_msg("Solving for step %d.." % (last_check_step)) - if smt.check_sat() != "sat": + if smt_check_sat() != "sat": print("%s No solution found!" % smt.timestamp()) retstatus = False break diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 7af37bca2..4e5359795 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -59,6 +59,9 @@ class SmtModInfo: self.covers = dict() self.anyconsts = dict() self.anyseqs = dict() + self.allconsts = dict() + self.allseqs = dict() + self.asize = dict() class SmtIo: @@ -69,6 +72,7 @@ class SmtIo: self.logic_uf = True self.logic_bv = True self.logic_dt = False + self.forall = False self.produce_models = True self.smt2cache = [list()] self.p = None @@ -108,6 +112,9 @@ class SmtIo: def setup(self): assert not self.setup_done + if self.forall: + self.unroll = False + if self.solver == "yices": self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts @@ -143,6 +150,7 @@ class SmtIo: self.p_open() if self.unroll: + assert not self.forall self.logic_uf = False self.unroll_idcnt = 0 self.unroll_buffer = "" @@ -376,6 +384,11 @@ class SmtIo: if self.logic is None: self.logic_dt = True + if fields[1] == "yosys-smt2-forall": + if self.logic is None: + self.logic_qf = False + self.forall = True + if fields[1] == "yosys-smt2-module": self.curmod = fields[2] self.modinfo[self.curmod] = SmtModInfo() @@ -419,10 +432,20 @@ class SmtIo: self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-anyconst": - self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4]) + self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) + self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) if fields[1] == "yosys-smt2-anyseq": - self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4]) + self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) + self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) + + if fields[1] == "yosys-smt2-allconst": + self.modinfo[self.curmod].allconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) + self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) + + if fields[1] == "yosys-smt2-allseq": + self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5]) + self.modinfo[self.curmod].asize[fields[2]] = int(fields[3]) def hiernets(self, top, regs_only=False): def hiernets_worker(nets, mod, cursor): @@ -439,7 +462,8 @@ class SmtIo: def hieranyconsts(self, top): def worker(results, mod, cursor): for name, value in sorted(self.modinfo[mod].anyconsts.items()): - results.append((cursor, name, value[0], value[1])) + width = self.modinfo[mod].asize[name] + results.append((cursor, name, value[0], value[1], width)) for cellname, celltype in sorted(self.modinfo[mod].cells.items()): worker(results, celltype, cursor + [cellname]) @@ -450,7 +474,32 @@ class SmtIo: def hieranyseqs(self, top): def worker(results, mod, cursor): for name, value in sorted(self.modinfo[mod].anyseqs.items()): - results.append((cursor, name, value[0], value[1])) + width = self.modinfo[mod].asize[name] + results.append((cursor, name, value[0], value[1], width)) + for cellname, celltype in sorted(self.modinfo[mod].cells.items()): + worker(results, celltype, cursor + [cellname]) + + results = list() + worker(results, top, []) + return results + + def hierallconsts(self, top): + def worker(results, mod, cursor): + for name, value in sorted(self.modinfo[mod].allconsts.items()): + width = self.modinfo[mod].asize[name] + results.append((cursor, name, value[0], value[1], width)) + for cellname, celltype in sorted(self.modinfo[mod].cells.items()): + worker(results, celltype, cursor + [cellname]) + + results = list() + worker(results, top, []) + return results + + def hierallseqs(self, top): + def worker(results, mod, cursor): + for name, value in sorted(self.modinfo[mod].allseqs.items()): + width = self.modinfo[mod].asize[name] + results.append((cursor, name, value[0], value[1], width)) for cellname, celltype in sorted(self.modinfo[mod].cells.items()): worker(results, celltype, cursor + [cellname]) diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore index a3f4f0f24..278f5ebf7 100644 --- a/examples/smtbmc/.gitignore +++ b/examples/smtbmc/.gitignore @@ -20,3 +20,5 @@ demo6.smt2 demo6.yslog demo7.smt2 demo7.yslog +demo8.smt2 +demo8.yslog diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index 2f7060bda..96fa058d6 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -1,5 +1,5 @@ -all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 +all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo1: demo1.smt2 yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 @@ -25,6 +25,9 @@ demo6: demo6.smt2 demo7: demo7.smt2 yosys-smtbmc -t 10 demo7.smt2 +demo8: demo8.smt2 + yosys-smtbmc -s z3 -t 1 -g demo8.smt2 + demo1.smt2: demo1.v yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2' @@ -46,6 +49,9 @@ demo6.smt2: demo6.v demo7.smt2: demo7.v yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2' +demo8.smt2: demo8.v + yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2' + clean: rm -f demo1.yslog demo1.smt2 demo1.vcd rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd @@ -54,6 +60,7 @@ clean: rm -f demo5.yslog demo5.smt2 demo5.vcd rm -f demo6.yslog demo6.smt2 rm -f demo7.yslog demo7.smt2 + rm -f demo8.yslog demo8.smt2 -.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 clean +.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 clean diff --git a/examples/smtbmc/demo8.v b/examples/smtbmc/demo8.v new file mode 100644 index 000000000..c4c396cde --- /dev/null +++ b/examples/smtbmc/demo8.v @@ -0,0 +1,12 @@ +// Simple exists-forall demo + +module demo8; + wire [7:0] prime = $anyconst; + wire [3:0] factor = $allconst; + + always @* begin + if (1 < factor && factor < prime) + assume((prime % factor) != 0); + assume(prime > 1); + end +endmodule -- 2.30.2