From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 27 Dec 2013 13:32:42 +0000 (+0100)
Subject: Fixed sat handling of $eqx and $nex cells
X-Git-Tag: yosys-0.2.0~225
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ebf9abfeb6c65821ee4f1ef0f4ab16660348c45f;p=yosys.git

Fixed sat handling of $eqx and $nex cells
---

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<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));