From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 26 Feb 2014 20:31:34 +0000 (+0100)
Subject: Added support for $bu0 to SatGen
X-Git-Tag: yosys-0.3.0~106
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aaaa604853caaecf8dcbfa928914495efb5556c6;p=yosys.git

Added support for $bu0 to SatGen
---

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 539210442..d9bcb4250 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -385,7 +385,7 @@ struct SatGen
 			return true;
 		}
 
-		if (cell->type == "$pos" || cell->type == "$neg")
+		if (cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg")
 		{
 			std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
 			std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
@@ -393,7 +393,7 @@ struct SatGen
 
 			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 
-			if (cell->type == "$pos") {
+			if (cell->type == "$pos" || cell->type == "$bu0") {
 				ez->assume(ez->vec_eq(a, yy));
 			} else {
 				std::vector<int> zero(a.size(), ez->FALSE);
@@ -404,9 +404,9 @@ struct SatGen
 			{
 				std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
-				extendSignalWidthUnary(undef_a, undef_y, cell, true);
+				extendSignalWidthUnary(undef_a, undef_y, cell, cell->type != "$bu0");
 
-				if (cell->type == "$pos") {
+				if (cell->type == "$pos" || cell->type == "$bu0") {
 					ez->assume(ez->vec_eq(undef_a, undef_y));
 				} else {
 					int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);