From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 21 Jul 2014 10:03:41 +0000 (+0200)
Subject: Bugfix in satgen for cells with wider in- than outputs.
X-Git-Tag: yosys-0.4~506
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c54d1f2ad1a781363f9c35e4f7266f4560a6aba8;p=yosys.git

Bugfix in satgen for cells with wider in- than outputs.
---

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 81d029295..281d2b26f 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -166,7 +166,15 @@ struct SatGen
 	void undefGating(std::vector<int> &vec_y, std::vector<int> &vec_yy, std::vector<int> &vec_undef)
 	{
 		assert(model_undef);
-		ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy))));
+		assert(vec_y.size() == vec_yy.size());
+		if (vec_y.size() > vec_undef.size()) {
+			std::vector<int> trunc_y(vec_y.begin(), vec_y.begin() + vec_undef.size());
+			std::vector<int> trunc_yy(vec_yy.begin(), vec_yy.begin() + vec_undef.size());
+			ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(trunc_y, trunc_yy))));
+		} else {
+			assert(vec_y.size() == vec_undef.size());
+			ez->assume(ez->expression(ezSAT::OpAnd, ez->vec_or(vec_undef, ez->vec_iff(vec_y, vec_yy))));
+		}
 	}
 
 	bool importCell(RTLIL::Cell *cell, int timestep = -1)