summaryrefslogtreecommitdiff
path: root/kernel/satgen.h
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-12-27 14:32:42 +0100
committerClifford Wolf <clifford@clifford.at>2013-12-27 14:32:42 +0100
commitebf9abfeb6c65821ee4f1ef0f4ab16660348c45f (patch)
treedd45bd340b25775211794916b2b5a0ce6cf8c74c /kernel/satgen.h
parent7b02a44efbb81ce2c97dcb87f1d8ca016c14ba76 (diff)
Fixed sat handling of $eqx and $nex cells
Diffstat (limited to 'kernel/satgen.h')
-rw-r--r--kernel/satgen.h13
1 files changed, 12 insertions, 1 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h
index c0807f55..8fb8e818 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -461,6 +461,13 @@ struct SatGen
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
+ std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
+ a = ez->vec_or(a, undef_a);
+ b = ez->vec_or(b, undef_b);
+ }
+
if (cell->type == "$lt")
ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
if (cell->type == "$le")
@@ -481,7 +488,11 @@ struct SatGen
std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
- yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+
+ if (cell->type == "$eqx")
+ yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+ else
+ yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
for (size_t i = 0; i < y.size(); i++)
ez->SET(ez->FALSE, undef_y.at(i));