aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smt2.cc196
-rw-r--r--backends/smt2/smtbmc.py159
-rw-r--r--backends/smt2/smtio.py2
3 files changed, 210 insertions, 147 deletions
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<RTLIL::SigBit, std::pair<int, int>> fcache;
std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes;
+ std::vector<string> 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/smtbmc.py b/backends/smt2/smtbmc.py
index 498621612..9dba68b2a 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -20,6 +20,7 @@
import os, sys, getopt, re
##yosys-sys-path##
from smtio import smtio, smtopts, mkvcd
+from collections import defaultdict
skip_steps = 0
step_size = 1
@@ -58,7 +59,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
-m <module_name>
name of the top module
- --constr <constr_filename>
+ --smtc <constr_filename>
read constraints file
--dump-vcd <vcd_filename>
@@ -69,14 +70,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
--dump-vlogtb <verilog_filename>
write trace as Verilog test bench
- --dump-constr <constr_filename>
+ --dump-smtc <constr_filename>
write trace as constraints file
""" + so.helpmsg())
sys.exit(1)
try:
- opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["constr=", "dump-vcd=", "dump-vlogtb=", "dump-constr="])
+ opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc="])
except:
usage()
@@ -92,13 +93,13 @@ for o, a in opts:
assume_skipped = int(a)
elif o == "-S":
step_size = int(a)
- elif o == "--constr":
+ elif o == "--smtc":
inconstr.append(a)
elif o == "--dump-vcd":
vcdfile = a
elif o == "--dump-vlogtb":
vlogtbfile = a
- elif o == "--dump-constr":
+ elif o == "--dump-smtc":
outconstr = a
elif o == "-i":
tempind = True
@@ -116,47 +117,74 @@ if len(args) != 1:
if tempind and len(inconstr) != 0:
- print("Error: options -i and --constr are exclusive.");
+ print("Error: options -i and --smtc are exclusive.");
sys.exit(1)
-constr_asserts = dict()
-constr_assumes = dict()
+constr_asserts = defaultdict(list)
+constr_assumes = defaultdict(list)
for fn in inconstr:
- current_state = None
+ current_states = None
with open(fn, "r") as f:
for line in f:
+ if line.startswith("#"):
+ continue
+
tokens = line.split()
if len(tokens) == 0:
continue
if tokens[0] == "initial":
- current_state = 0
+ current_states = set()
+ current_states.add(0)
continue
if tokens[0] == "state":
- current_state = int(tokens[1])
+ current_states = set()
+ for token in tokens[1:]:
+ tok = token.split(":")
+ if len(tok) == 1:
+ current_states.add(int(token))
+ elif len(tok) == 2:
+ lower = int(tok[0])
+ if tok[1] == "*":
+ upper = num_steps
+ else:
+ upper = int(tok[1])
+ for i in range(lower, upper+1):
+ current_states.add(i)
+ else:
+ assert 0
+ continue
+
+ if tokens[0] == "always":
+ if len(tokens) == 1:
+ current_states = set(range(0, num_steps+1))
+ elif len(tokens) == 2:
+ i = int(tokens[1])
+ assert i < 0
+ current_states = set(range(-i, num_steps+1))
+ else:
+ assert 0
continue
if tokens[0] == "assert":
- assert current_state is not None
+ assert current_states is not None
- if current_state not in constr_asserts:
- constr_asserts[current_state] = list()
+ for state in current_states:
+ constr_asserts[state].append(" ".join(tokens[1:]))
- constr_asserts[current_state].append(" ".join(tokens[1:]))
continue
if tokens[0] == "assume":
- assert current_state is not None
+ assert current_states is not None
- if current_state not in constr_assumes:
- constr_assumes[current_state] = list()
+ for state in current_states:
+ constr_assumes[state].append(" ".join(tokens[1:]))
- constr_assumes[current_state].append(" ".join(tokens[1:]))
continue
assert 0
@@ -166,9 +194,25 @@ def get_constr_expr(db, state):
if state not in db:
return "true"
+ netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]+)\](?=[ )]|$)')
+
+ def replace_netref(match):
+ state_sel = match.group(2)
+
+ if state_sel == "":
+ st = state
+ elif state_sel[0] == "-":
+ st = state + int(state_sel[:-1])
+ else:
+ st = int(state_sel[:-1])
+
+ expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3)))
+
+ return match.group(1) + expr
+
expr_list = list()
for expr in db[state]:
- expr = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr)
+ expr = netref_regex.sub(replace_netref, expr)
expr_list.append(expr)
if len(expr_list) == 0:
@@ -430,35 +474,7 @@ if tempind:
break
-elif gentrace:
- retstatus = True
- for step in range(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_a s%d))" % (topmod, step))
- smt.write("(assert (%s_h s%d))" % (topmod, step))
- smt.write("(assert %s)" % get_constr_expr(constr_asserts, step))
- smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
-
- if step == 0:
- smt.write("(assert (%s_i s0))" % (topmod))
- smt.write("(assert (%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))
-
- print("%s Creating trace of length %d.." % (smt.timestamp(), num_steps))
-
- if smt.check_sat() == "sat":
- write_trace(num_steps)
-
- else:
- print("%s Creating trace failed!" % smt.timestamp())
- retstatus = False
-
-
-else: # not tempind, not gentrace
+else: # not tempind
step = 0
retstatus = True
while step < num_steps:
@@ -495,30 +511,41 @@ else: # not tempind, not gentrace
smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i))
last_check_step = step+i
- if last_check_step == step:
- print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
- else:
- print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
- smt.write("(push 1)")
+ if not gentrace:
+ if last_check_step == step:
+ print("%s Checking asserts in step %d.." % (smt.timestamp(), step))
+ else:
+ print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step))
+ smt.write("(push 1)")
- smt.write("(assert (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)]))
+ smt.write("(assert (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":
- print("%s BMC failed!" % smt.timestamp())
- print_failed_asserts(topmod, "s%d" % step, topmod)
- write_trace(step+step_size)
- retstatus = False
- break
+ if smt.check_sat() == "sat":
+ print("%s BMC failed!" % smt.timestamp())
+ print_failed_asserts(topmod, "s%d" % step, topmod)
+ write_trace(step+step_size)
+ retstatus = False
+ break
- else: # unsat
smt.write("(pop 1)")
- 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))
+
+ 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))
+
+ if gentrace:
+ print("%s Solving for step %d.." % (smt.timestamp(), step))
+ if smt.check_sat() != "sat":
+ print("%s No solution found!" % smt.timestamp())
+ retstatus = False
+ break
step += step_size
+ if gentrace:
+ write_trace(num_steps)
+
smt.write("(exit)")
smt.wait()
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)
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-25 00:50:24 +0000