diff options
author | Clifford Wolf <clifford@clifford.at> | 2016-07-27 15:52:20 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2016-07-27 15:52:20 +0200 |
commit | 8d88fcb27011a6f8f47a8615c30ab658fafab0f2 (patch) | |
tree | bd88fec1a0e3a1928d00cbfb42a47d2d8779accd /kernel/satgen.h | |
parent | 9540be1d45cce45d0008a4160bc4aa70ff0dfe1d (diff) | |
download | yosys-8d88fcb27011a6f8f47a8615c30ab658fafab0f2.tar.gz yosys-8d88fcb27011a6f8f47a8615c30ab658fafab0f2.tar.bz2 yosys-8d88fcb27011a6f8f47a8615c30ab658fafab0f2.zip |
Added SatGen support for $anyconst
Diffstat (limited to 'kernel/satgen.h')
-rw-r--r-- | kernel/satgen.h | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index fdd2ce8b1..0a65b490c 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -1319,6 +1319,28 @@ struct SatGen return true; } + if (cell->type == "$anyconst") + { + if (timestep < 2) + return true; + + std::vector<int> d = importDefSigSpec(cell->getPort("\\Y"), timestep-1); + std::vector<int> q = importDefSigSpec(cell->getPort("\\Y"), timestep); + + std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q; + ez->assume(ez->vec_eq(d, qq)); + + if (model_undef) + { + std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1); + std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep); + + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } + return true; + } + if (cell->type == "$_BUF_" || cell->type == "$equiv") { std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep); |