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

Various fixes and improvements in smt2 back-end

This commit is contained in:
Clifford Wolf 2016-08-26 17:33:02 +02:00
parent 4be4969bae
commit 17233b11e1
2 changed files with 117 additions and 81 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

196
backends/smt2/smt2.cc
View File

@ -43,13 +43,14 @@ struct Smt2Worker
std::map<RTLIL::SigBit, std::pair<int, int>> fcache; std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
std::map<Cell*, int> memarrays; std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes; std::map<int, int> bvsizes;
std::vector<string> ids;
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) : Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) :
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
wiresmode(wiresmode), verbose(verbose), idcounter(0) wiresmode(wiresmode), verbose(verbose), idcounter(0)
{ {
decls.push_back(stringf("(declare-sort |%s_s| 0)\n", 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", log_id(module), log_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 cell : module->cells())
for (auto &conn : cell->connections()) { 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) void register_bool(RTLIL::SigBit bit, int id)
{ {
if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "", 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), "", if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
log_signal(bit)); log_signal(bit));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", 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++); register_bool(bit, idcounter++);
} }
auto f = fcache.at(bit); auto f = fcache.at(bit);
if (f.second >= 0) 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("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name);
return stringf("(|%s#%d| %s)", log_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") std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state")
@ -181,10 +208,10 @@ struct Smt2Worker
j++; j++;
} }
if (t1.second == 0 && j == bvsizes.at(t1.first)) 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 else
subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))", 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; continue;
} }
@ -197,8 +224,8 @@ struct Smt2Worker
for (auto bit : sig.extract(i, j)) for (auto bit : sig.extract(i, j))
log_assert(bit_driver.count(bit) == 0); log_assert(bit_driver.count(bit) == 0);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", 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)))); get_id(module), idcounter, get_id(module), j, log_signal(sig.extract(i, j))));
subexpr.push_back(stringf("(|%s#%d| %s)", log_id(module), idcounter, state_name)); subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name));
register_bv(sig.extract(i, j), idcounter++); register_bv(sig.extract(i, j), idcounter++);
} }
@ -229,10 +256,11 @@ struct Smt2Worker
else processed_expr += ch; else processed_expr += ch;
} }
if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", if (verbose)
log_id(cell)); 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", 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++); register_bool(bit, idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
} }
@ -272,16 +300,16 @@ struct Smt2Worker
if (width != GetSize(sig_y) && type != 'b') if (width != GetSize(sig_y) && type != 'b')
processed_expr = stringf("((_ extract %d 0) %s)", GetSize(sig_y)-1, processed_expr.c_str()); 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), "", if (verbose)
log_id(cell)); log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
if (type == 'b') { if (type == 'b') {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", 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++); register_boolvec(sig_y, idcounter++);
} else { } else {
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 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++); register_bv(sig_y, idcounter++);
} }
@ -303,21 +331,23 @@ struct Smt2Worker
} else } else
processed_expr += ch; processed_expr += ch;
if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", if (verbose)
log_id(cell)); 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", 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++); register_boolvec(sig_y, idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
} }
void export_cell(RTLIL::Cell *cell) void export_cell(RTLIL::Cell *cell)
{ {
if (verbose) log("%*s=> export_cell %s (%s) [%s]\n", 2+2*GetSize(recursive_cells), "", if (verbose)
log_id(cell), log_id(cell->type), exported_cells.count(cell) ? "old" : "new"); 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)) 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)) if (exported_cells.count(cell))
return; return;
@ -329,7 +359,7 @@ struct Smt2Worker
{ {
SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); 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", 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++); register_bool(bit, idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
return; return;
@ -339,7 +369,7 @@ struct Smt2Worker
{ {
registers.insert(cell); registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", 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++); register_bool(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
return; return;
@ -367,7 +397,7 @@ struct Smt2Worker
{ {
registers.insert(cell); registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", 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++); register_bv(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
return; return;
@ -435,11 +465,12 @@ struct Smt2Worker
processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(), 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()); 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), "", if (verbose)
log_id(cell)); log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y")); RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", 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++); register_bv(sig, idcounter++);
recursive_cells.erase(cell); recursive_cells.erase(cell);
return; return;
@ -458,11 +489,11 @@ struct Smt2Worker
int rd_ports = cell->getParam("\\RD_PORTS").as_int(); 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", 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", 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++) 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)); "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", 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", 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++); register_bv(data_sig, idcounter++);
} }
@ -491,8 +522,8 @@ struct Smt2Worker
if (m != nullptr) if (m != nullptr)
{ {
decls.push_back(stringf("; yosys-smt2-cell %s %s\n", log_id(cell->type), 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)", log_id(module), log_id(cell->name)); string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
for (auto &conn : cell->connections()) for (auto &conn : cell->connections())
{ {
@ -503,25 +534,25 @@ struct Smt2Worker
if (GetSize(w) > 1) { if (GetSize(w) > 1) {
if (bvmode) { if (bvmode) {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", 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++); register_bv(sig, idcounter++);
} else { } else {
for (int i = 0; i < GetSize(w); i++) { for (int i = 0; i < GetSize(w); i++) {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", 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++); register_bool(sig[i], idcounter++);
} }
} }
} else { } else {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", 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++); register_bool(sig, idcounter++);
} }
} }
} }
decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n", 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); hiercells.insert(cell);
recursive_cells.erase(cell); recursive_cells.erase(cell);
@ -533,11 +564,11 @@ struct Smt2Worker
if (bvmode || GetSize(w) == 1) { 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(), 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 { } else {
for (int i = 0; i < GetSize(w); i++) 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(), 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] == '\\')) { if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire); RTLIL::SigSpec sig = sigmap(wire);
if (wire->port_input) 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) 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) 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] == '\\')) 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) { if (bvmode && GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", 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 { } else {
for (int i = 0; i < GetSize(sig); i++) 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", 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 else
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", 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"); Const val = wire->attributes.at("\\init");
val.bits.resize(GetSize(sig)); val.bits.resize(GetSize(sig));
if (bvmode && GetSize(sig) > 1) { 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 { } else {
for (int i = 0; i < GetSize(sig); i++) 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")) { if (cell->type.in("$assert", "$assume")) {
string name_a = get_bool(cell->getPort("\\A")); string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN")); 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, 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() : log_id(cell))); 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", 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") 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 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++) 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_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state"); 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") if (cell->type == "$dff")
{ {
std::string expr_d = get_bv(cell->getPort("\\D")); std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state"); 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") if (cell->type == "$mem")
@ -661,29 +692,29 @@ struct Smt2Worker
std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width)); 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 = 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)) " 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", "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
log_id(module), arrayid, i+1, log_id(module), abits, width, get_id(module), arrayid, i+1, get_id(module), abits, width,
log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell))); 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_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid); 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(), log_id(cell))); trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
} }
} }
} }
for (auto c : hiercells) 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))); 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)));
for (auto c : hiercells) init_list.push_back(stringf("(|%s_i| (|%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))", log_id(c->type), log_id(module), log_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",
for (auto c : hiercells) get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
init_list.push_back(stringf("(|%s_i| (|%s_h %s| state))", log_id(c->type), log_id(module), log_id(c->name))); }
string assert_expr = assert_list.empty() ? "true" : "(and"; string assert_expr = assert_list.empty() ? "true" : "(and";
if (!assert_list.empty()) { if (!assert_list.empty()) {
@ -692,7 +723,7 @@ struct Smt2Worker
assert_expr += "\n)"; assert_expr += "\n)";
} }
decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\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"; string assume_expr = assume_list.empty() ? "true" : "(and";
if (!assume_list.empty()) { if (!assume_list.empty()) {
@ -701,7 +732,7 @@ struct Smt2Worker
assume_expr += "\n)"; assume_expr += "\n)";
} }
decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\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"; string init_expr = init_list.empty() ? "true" : "(and";
if (!init_list.empty()) { if (!init_list.empty()) {
@ -710,17 +741,17 @@ struct Smt2Worker
init_expr += "\n)"; init_expr += "\n)";
} }
decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\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) 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) for (auto it : decls)
f << it; 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) { if (GetSize(hier) > 1) {
f << "(and\n"; f << "(and\n";
for (auto it : hier) for (auto it : hier)
@ -732,7 +763,7 @@ struct Smt2Worker
else else
f << "true)\n"; 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) { if (GetSize(trans) > 1) {
f << "(and\n"; f << "(and\n";
for (auto it : trans) for (auto it : trans)
@ -743,7 +774,7 @@ struct Smt2Worker
f << "\n" + trans.front() + ")"; f << "\n" + trans.front() + ")";
else else
f << "true)"; 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_deps.erase(sorted_modules.at(sorted_modules_idx++));
} }
Module *topmod = design->top_module();
std::string topmod_id;
for (auto module : sorted_modules) for (auto module : sorted_modules)
{ {
if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn()) 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); Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose);
worker.run(); worker.run();
worker.write(*f); worker.write(*f);
if (module == topmod)
topmod_id = worker.get_id(module);
} }
Module *topmod = design->top_module();
if (topmod) 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"); *f << stringf("; end of yosys output\n");

2
backends/smt2/smtio.py
View File

@ -375,7 +375,7 @@ class smtio:
nextmod = self.modinfo[mod].cells[path[0]] nextmod = self.modinfo[mod].cells[path[0]]
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) 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): def mem_info(self, mod, base, path):
return self.mem_expr(mod, base, path, infomode=True) return self.mem_expr(mod, base, path, infomode=True)