diff options
| author | Jannis Harder <me@jix.one> | 2022-10-12 20:50:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-12 20:50:00 +0200 |
| commit | 33a2773de0605cb19e26fc6675fb3e86273c5087 (patch) | |
| tree | 54858b2035152d683f0b3d00c10f6dbe7d97430a /backends/smt2/smt2.cc | |
| parent | f35c062354668b817a0f911fe9158b6b1e150617 (diff) | |
| parent | 4d334fd3e352f86e46e5810ae021b9ba0bf03752 (diff) | |
| download | yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.gz yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.bz2 yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.zip | |
Merge pull request #3510 from jix/ff_witness_fixes
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 54783cf1b..7434b13da 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -559,6 +559,9 @@ struct Smt2Worker if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { registers.insert(cell); + SigBit q_bit = cell->getPort(ID::Q); + if (q_bit.is_wire()) + decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire)); makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q))); register_bool(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -589,9 +592,12 @@ struct Smt2Worker if (cell->type.in(ID($ff), ID($dff))) { registers.insert(cell); - for (auto chunk : cell->getPort(ID::Q).chunks()) + int smtoffset = 0; + for (auto chunk : cell->getPort(ID::Q).chunks()) { if (chunk.is_wire()) - decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire)); + decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset)); + smtoffset += chunk.width; + } makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); register_bv(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -1490,7 +1496,7 @@ struct Smt2Worker return path; } - std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire) + std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0) { std::vector<std::string> hiername; const char *wire_name = wire->name.c_str(); @@ -1508,6 +1514,7 @@ struct Smt2Worker { "offset", offset }, { "width", width }, { "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) }, + { "smtoffset", smtoffset }, { "path", witness_path(wire) }, }}).dump(line); line += "\n"; |