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

fixed write_smt2 for (non-combinatorial) loops through hierarchical cells

This commit is contained in:
Clifford Wolf 2016-09-10 15:14:41 +02:00
parent 3ceba145d5
commit b582f11074
1 changed files with 34 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
backends/smt2/smt2.cc
View File

@ -37,7 +37,7 @@ struct Smt2Worker
std::vector<std::string> decls, trans, hier;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells, hiercells;
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
@ -581,23 +581,8 @@ struct Smt2Worker
get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
hiercells.insert(cell);
hiercells_queue.insert(cell);
recursive_cells.erase(cell);
for (auto &conn : cell->connections())
{
Wire *w = m->wire(conn.first);
SigSpec sig = sigmap(conn.second);
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(),
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(),
get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
}
}
return;
}
@ -762,6 +747,38 @@ struct Smt2Worker
}
}
if (verbose) log("=> export logic driving hierarchical cells\n");
while (!hiercells_queue.empty())
{
std::set<RTLIL::Cell*> queue;
queue.swap(hiercells_queue);
for (auto cell : queue)
{
string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
Module *m = module->design->module(cell->type);
log_assert(m != nullptr);
for (auto &conn : cell->connections())
{
Wire *w = m->wire(conn.first);
SigSpec sig = sigmap(conn.second);
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(),
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(),
get_id(cell->type), get_id(w), i, cell_state.c_str(), get_id(cell->type), get_id(w), i));
}
}
}
}
if (verbose) log("=> finalizing SMT2 representation of %s.\n", log_id(module));
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)));