aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/satgen.h
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-07-27 15:52:20 +0200
committerClifford Wolf <clifford@clifford.at>2016-07-27 15:52:20 +0200
commit8d88fcb27011a6f8f47a8615c30ab658fafab0f2 (patch)
treebd88fec1a0e3a1928d00cbfb42a47d2d8779accd /kernel/satgen.h
parent9540be1d45cce45d0008a4160bc4aa70ff0dfe1d (diff)
downloadyosys-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.h22
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);