From ebf9abfeb6c65821ee4f1ef0f4ab16660348c45f Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 27 Dec 2013 14:32:42 +0100 Subject: [PATCH] Fixed sat handling of $eqx and $nex cells --- kernel/satgen.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index c0807f550..8fb8e818a 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -461,6 +461,13 @@ struct SatGen std::vector yy = model_undef ? ez->vec_var(y.size()) : y; + if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) { + std::vector undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep); + std::vector 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 undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep); std::vector undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep); std::vector 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)); -- 2.30.2