Various equiv_simple improvements

1 files changed, 19 insertions, 0 deletions

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 2c69663c4..c874099b7 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -1163,6 +1163,25 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$_BUF_" || cell->type == "$equiv")
+		{
+			std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+			std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+			extendSignalWidthUnary(a, y, cell);
+
+			std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+			ez->assume(ez->vec_eq(a, yy));
+
+			if (model_undef) {
+				std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+				std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+				extendSignalWidthUnary(undef_a, undef_y, cell, false);
+				ez->assume(ez->vec_eq(undef_a, undef_y));
+				undefGating(y, yy, undef_y);
+			}
+			return true;
+		}
+
 		if (cell->type == "$assert")
 		{
 			std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));