From: Clifford Wolf Date: Fri, 26 Aug 2016 15:33:02 +0000 (+0200) Subject: Various fixes and improvements in smt2 back-end X-Git-Tag: yosys-0.7~103 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=17233b11e185d2c863ccd06830e8cd0d2be38e83;p=yosys.git Various fixes and improvements in smt2 back-end --- diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index aaafc3f9a..af048859c 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -43,13 +43,14 @@ struct Smt2Worker std::map> fcache; std::map memarrays; std::map bvsizes; + std::vector ids; Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose), idcounter(0) { - decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); - decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", log_id(module), log_id(module))); + decls.push_back(stringf("(declare-sort |%s_s| 0)\n", get_id(module))); + decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", get_id(module), get_id(module))); for (auto cell : module->cells()) for (auto &conn : cell->connections()) { @@ -67,6 +68,32 @@ struct Smt2Worker } } + const char *get_id(IdString n) + { + std::string str = log_id(n); + for (int i = 0; i < GetSize(str); i++) { + if (str[i] == '\\') + str[i] = '/'; + } + ids.push_back(str); + return ids.back().c_str(); + } + + const char *get_id(Module *m) + { + return get_id(m->name); + } + + const char *get_id(Cell *c) + { + return get_id(c->name); + } + + const char *get_id(Wire *w) + { + return get_id(w->name); + } + void register_bool(RTLIL::SigBit bit, int id) { if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "", @@ -122,14 +149,14 @@ struct Smt2Worker if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "", log_signal(bit)); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", - log_id(module), idcounter, log_id(module), log_signal(bit))); + get_id(module), idcounter, get_id(module), log_signal(bit))); register_bool(bit, idcounter++); } auto f = fcache.at(bit); if (f.second >= 0) - return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, log_id(module), f.first, state_name); - return stringf("(|%s#%d| %s)", log_id(module), f.first, state_name); + return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name); + return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name); } std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state") @@ -181,10 +208,10 @@ struct Smt2Worker j++; } if (t1.second == 0 && j == bvsizes.at(t1.first)) - subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), t1.first, state_name)); + subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name)); else subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))", - t1.second + j - 1, t1.second, log_id(module), t1.first, state_name)); + t1.second + j - 1, t1.second, get_id(module), t1.first, state_name)); continue; } @@ -197,8 +224,8 @@ struct Smt2Worker for (auto bit : sig.extract(i, j)) log_assert(bit_driver.count(bit) == 0); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", - log_id(module), idcounter, log_id(module), j, log_signal(sig.extract(i, j)))); - subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name)); + get_id(module), idcounter, get_id(module), j, log_signal(sig.extract(i, j)))); + subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name)); register_bv(sig.extract(i, j), idcounter++); } @@ -229,10 +256,11 @@ struct Smt2Worker else processed_expr += ch; } - if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", - log_id(cell)); + if (verbose) + log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", - log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(bit))); + get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit))); register_bool(bit, idcounter++); recursive_cells.erase(cell); } @@ -272,16 +300,16 @@ struct Smt2Worker if (width != GetSize(sig_y) && type != 'b') processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str()); - if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", - log_id(cell)); + if (verbose) + log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); if (type == 'b') { decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", - log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y))); + get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y))); register_boolvec(sig_y, idcounter++); } else { decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - log_id(module), idcounter, log_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y))); + get_id(module), idcounter, get_id(module), GetSize(sig_y), processed_expr.c_str(), log_signal(sig_y))); register_bv(sig_y, idcounter++); } @@ -303,21 +331,23 @@ struct Smt2Worker } else processed_expr += ch; - if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", - log_id(cell)); + if (verbose) + log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", - log_id(module), idcounter, log_id(module), processed_expr.c_str(), log_signal(sig_y))); + get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(sig_y))); register_boolvec(sig_y, idcounter++); recursive_cells.erase(cell); } void export_cell(RTLIL::Cell *cell) { - if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "", - log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new"); + if (verbose) + log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "", + log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new"); if (recursive_cells.count(cell)) - log_error("Found logic loop in module %s! See cell %s.\n", log_id(module), log_id(cell)); + log_error("Found logic loop in module %s! See cell %s.\n", get_id(module), get_id(cell)); if (exported_cells.count(cell)) return; @@ -329,7 +359,7 @@ struct Smt2Worker { SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n", - log_id(module), idcounter, log_id(module), log_id(module), log_signal(bit))); + get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit))); register_bool(bit, idcounter++); recursive_cells.erase(cell); return; @@ -339,7 +369,7 @@ struct Smt2Worker { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", - log_id(module), idcounter, log_id(module), log_signal(cell->getPort("\\Q")))); + get_id(module), idcounter, get_id(module), log_signal(cell->getPort("\\Q")))); register_bool(cell->getPort("\\Q"), idcounter++); recursive_cells.erase(cell); return; @@ -367,7 +397,7 @@ struct Smt2Worker { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", - log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")))); + get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")))); register_bv(cell->getPort("\\Q"), idcounter++); recursive_cells.erase(cell); return; @@ -435,11 +465,12 @@ struct Smt2Worker processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(), get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str()); - if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", - log_id(cell)); + if (verbose) + log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); + RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y")); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig))); + get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig))); register_bv(sig, idcounter++); recursive_cells.erase(cell); return; @@ -458,11 +489,11 @@ struct Smt2Worker int rd_ports = cell->getParam("\\RD_PORTS").as_int(); decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - log_id(module), arrayid, log_id(module), abits, width, log_id(cell))); + get_id(module), arrayid, get_id(module), abits, width, get_id(cell))); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", log_id(cell), abits, width, rd_ports)); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", get_id(cell), abits, width, rd_ports)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n", - log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid)); + get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid)); for (int i = 0; i < rd_ports; i++) { @@ -475,10 +506,10 @@ struct Smt2Worker "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - log_id(module), i, log_id(cell), log_id(module), abits, addr.c_str(), log_signal(addr_sig))); + get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n", - log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, addr.c_str(), log_signal(data_sig))); register_bv(data_sig, idcounter++); } @@ -491,8 +522,8 @@ struct Smt2Worker if (m != nullptr) { - decls.push_back(stringf("; yosys-smt2-cell %s %s\n", log_id(cell->type), log_id(cell->name))); - string cell_state = stringf("(|%s_h %s| state)", log_id(module), log_id(cell->name)); + decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name))); + string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name)); for (auto &conn : cell->connections()) { @@ -503,25 +534,25 @@ struct Smt2Worker if (GetSize(w) > 1) { if (bvmode) { decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", - log_id(module), idcounter, log_id(module), GetSize(w), log_signal(sig))); + get_id(module), idcounter, get_id(module), GetSize(w), log_signal(sig))); register_bv(sig, idcounter++); } else { for (int i = 0; i < GetSize(w); i++) { decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", - log_id(module), idcounter, log_id(module), log_signal(sig[i]))); + get_id(module), idcounter, get_id(module), log_signal(sig[i]))); register_bool(sig[i], idcounter++); } } } else { decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", - log_id(module), idcounter, log_id(module), log_signal(sig))); + get_id(module), idcounter, get_id(module), log_signal(sig))); register_bool(sig, idcounter++); } } } decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n", - log_id(module), log_id(cell->name), log_id(module), log_id(cell->type))); + get_id(module), get_id(cell->name), get_id(module), get_id(cell->type))); hiercells.insert(cell); recursive_cells.erase(cell); @@ -533,11 +564,11 @@ struct Smt2Worker if (bvmode || GetSize(w) == 1) { hier.push_back(stringf(" (= %s (|%s_n %s| %s)) ; %s.%s\n", (GetSize(w) > 1 ? get_bv(sig) : get_bool(sig)).c_str(), - log_id(cell->type), log_id(w), cell_state.c_str(), log_id(cell->type), log_id(w))); + get_id(cell->type), get_id(w), cell_state.c_str(), get_id(cell->type), get_id(w))); } else { for (int i = 0; i < GetSize(w); i++) hier.push_back(stringf(" (= %s (|%s_n %s %d| %s)) ; %s.%s[%d]\n", get_bool(sig[i]).c_str(), - log_id(cell->type), log_id(w), i, cell_state.c_str(), log_id(cell->type), log_id(w), i)); + get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i)); } } @@ -568,24 +599,24 @@ struct Smt2Worker if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) { RTLIL::SigSpec sig = sigmap(wire); if (wire->port_input) - decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width)); + decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); if (wire->port_output) - decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width)); + decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); if (is_register) - decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width)); + decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) - decls.push_back(stringf("; yosys-smt2-wire %s %d\n", log_id(wire), wire->width)); + decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); if (bvmode && GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", - log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str())); + get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); } else { for (int i = 0; i < GetSize(sig); i++) if (GetSize(sig) > 1) decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", - log_id(module), log_id(wire), i, log_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str())); else decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", - log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str())); } } } @@ -599,10 +630,10 @@ struct Smt2Worker Const val = wire->attributes.at("\\init"); val.bits.resize(GetSize(sig)); if (bvmode && GetSize(sig) > 1) { - init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), log_id(wire))); + init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire))); } else { for (int i = 0; i < GetSize(sig); i++) - init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", log_id(wire))); + init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire))); } } @@ -613,14 +644,14 @@ struct Smt2Worker if (cell->type.in("$assert", "$assume")) { string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); - decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, log_id(module), idcounter, - cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : log_id(cell))); + decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, + cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell))); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", - log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell))); + get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); if (cell->type == "$assert") - assert_list.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter++)); + assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); else - assume_list.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter++)); + assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); } for (int iter = 1; !registers.empty(); iter++) @@ -636,14 +667,14 @@ 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(), log_id(cell), log_signal(cell->getPort("\\Q")))); + 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")))); } if (cell->type == "$dff") { 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(), log_id(cell), log_signal(cell->getPort("\\Q")))); + 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")))); } if (cell->type == "$mem") @@ -661,29 +692,29 @@ struct Smt2Worker std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width)); data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", - data.c_str(), mask.c_str(), log_id(module), arrayid, i, addr.c_str(), mask.c_str()); + data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) " "(store (|%s#%d#%d| state) %s %s)) ; %s\n", - log_id(module), arrayid, i+1, log_id(module), abits, width, - log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell))); + get_id(module), arrayid, i+1, get_id(module), abits, width, + get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell))); } - std::string expr_d = stringf("(|%s#%d#%d| state)", log_id(module), arrayid, wr_ports); - std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid); - trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell))); + 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))); } } } - for (auto c : hiercells) - assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", log_id(c->type), log_id(module), log_id(c->name))); - - for (auto c : hiercells) - assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", log_id(c->type), log_id(module), log_id(c->name))); - - for (auto c : hiercells) - init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", log_id(c->type), log_id(module), log_id(c->name))); + for (auto c : hiercells) { + assert_list.push_back(stringf("(|%s_a| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); + assume_list.push_back(stringf("(|%s_u| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); + init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", get_id(c->type), get_id(module), get_id(c->name))); + 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))); + } string assert_expr = assert_list.empty() ? "true" : "(and"; if (!assert_list.empty()) { @@ -692,7 +723,7 @@ struct Smt2Worker assert_expr += "\n)"; } decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n", - log_id(module), log_id(module), assert_expr.c_str())); + get_id(module), get_id(module), assert_expr.c_str())); string assume_expr = assume_list.empty() ? "true" : "(and"; if (!assume_list.empty()) { @@ -701,7 +732,7 @@ struct Smt2Worker assume_expr += "\n)"; } decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n", - log_id(module), log_id(module), assume_expr.c_str())); + get_id(module), get_id(module), assume_expr.c_str())); string init_expr = init_list.empty() ? "true" : "(and"; if (!init_list.empty()) { @@ -710,17 +741,17 @@ struct Smt2Worker init_expr += "\n)"; } decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n", - log_id(module), log_id(module), init_expr.c_str())); + get_id(module), get_id(module), init_expr.c_str())); } void write(std::ostream &f) { - f << stringf("; yosys-smt2-module %s\n", log_id(module)); + f << stringf("; yosys-smt2-module %s\n", get_id(module)); for (auto it : decls) f << it; - f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", log_id(module), log_id(module)); + f << stringf("(define-fun |%s_h| ((state |%s_s|)) Bool ", get_id(module), get_id(module)); if (GetSize(hier) > 1) { f << "(and\n"; for (auto it : hier) @@ -732,7 +763,7 @@ struct Smt2Worker else f << "true)\n"; - f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module)); + f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", get_id(module), get_id(module), get_id(module)); if (GetSize(trans) > 1) { f << "(and\n"; for (auto it : trans) @@ -743,7 +774,7 @@ struct Smt2Worker f << "\n" + trans.front() + ")"; else f << "true)"; - f << stringf(" ; end of module %s\n", log_id(module)); + f << stringf(" ; end of module %s\n", get_id(module)); } }; @@ -937,6 +968,9 @@ struct Smt2Backend : public Backend { module_deps.erase(sorted_modules.at(sorted_modules_idx++)); } + Module *topmod = design->top_module(); + std::string topmod_id; + for (auto module : sorted_modules) { if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn()) @@ -947,11 +981,13 @@ struct Smt2Backend : public Backend { Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose); worker.run(); worker.write(*f); + + if (module == topmod) + topmod_id = worker.get_id(module); } - Module *topmod = design->top_module(); if (topmod) - *f << stringf("; yosys-smt2-topmod %s\n", log_id(topmod)); + *f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str()); *f << stringf("; end of yosys output\n"); diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 0b2263338..da9d4830f 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -375,7 +375,7 @@ class smtio: nextmod = self.modinfo[mod].cells[path[0]] nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) - return self.mem_expr(nextmod, nextbase, path[1:]) + return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode) def mem_info(self, mod, base, path): return self.mem_expr(mod, base, path, infomode=True)