diff options
| author | Jannis Harder <me@jix.one> | 2022-11-28 14:48:58 +0100 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-11-28 14:50:52 +0100 |
| commit | ed0e14820ed7790d88504800dc5b59a4194a6992 (patch) | |
| tree | 8cf7d29078353f34019df200bc44b5687c6fc390 /kernel | |
| parent | 23e26ff66153f6c147adee515e547b7d34962347 (diff) | |
| download | yosys-ed0e14820ed7790d88504800dc5b59a4194a6992.tar.gz yosys-ed0e14820ed7790d88504800dc5b59a4194a6992.tar.bz2 yosys-ed0e14820ed7790d88504800dc5b59a4194a6992.zip | |
sat: Add -set-def-formal option to force defined $any* outputs
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/satgen.cc | 27 | ||||
| -rw-r--r-- | kernel/satgen.h | 1 |
2 files changed, 24 insertions, 4 deletions
diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 05eeca76e..2a1fd1711 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1187,6 +1187,10 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) if (timestep == 1) { initial_state.add((*sigmap)(cell->getPort(ID::Q))); + if (model_undef && def_formal) { + std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Q), timestep); + ez->assume(ez->NOT(ez->vec_reduce_or(undef_q))); + } } else { @@ -1254,13 +1258,18 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) if (cell->type == ID($anyconst)) { - if (timestep < 2) + if (timestep < 2) { + if (model_undef && def_formal) { + std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); + ez->assume(ez->NOT(ez->vec_reduce_or(undef_y))); + } return true; + } std::vector<int> d = importDefSigSpec(cell->getPort(ID::Y), timestep-1); std::vector<int> q = importDefSigSpec(cell->getPort(ID::Y), timestep); - std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q; + std::vector<int> qq = (model_undef && !def_formal) ? ez->vec_var(q.size()) : q; ez->assume(ez->vec_eq(d, qq)); if (model_undef) @@ -1268,14 +1277,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) std::vector<int> undef_d = importUndefSigSpec(cell->getPort(ID::Y), timestep-1); std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep); - ez->assume(ez->vec_eq(undef_d, undef_q)); - undefGating(q, qq, undef_q); + if (def_formal) { + for (auto &undef_q_bit : undef_q) + ez->SET(ez->CONST_FALSE, undef_q_bit); + } else { + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } } return true; } if (cell->type == ID($anyseq)) { + if (model_undef && def_formal) { + std::vector<int> undef_q = importUndefSigSpec(cell->getPort(ID::Y), timestep); + for (auto &undef_q_bit : undef_q) + ez->SET(ez->CONST_FALSE, undef_q_bit); + } return true; } diff --git a/kernel/satgen.h b/kernel/satgen.h index da2cec222..8a89ff9db 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -73,6 +73,7 @@ struct SatGen std::map<std::pair<std::string, int>, bool> initstates; bool ignore_div_by_zero; bool model_undef; + bool def_formal = false; SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) : ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false) |