From 8d88fcb27011a6f8f47a8615c30ab658fafab0f2 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 27 Jul 2016 15:52:20 +0200
Subject: Added SatGen support for $anyconst

---
 kernel/satgen.h | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'kernel')

diff --git a/kernel/satgen.h b/kernel/satgen.h
index fdd2ce8b1..0a65b490c 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -1319,6 +1319,28 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$anyconst")
+		{
+			if (timestep < 2)
+				return true;
+
+			std::vector<int> d = importDefSigSpec(cell->getPort("\\Y"), timestep-1);
+			std::vector<int> q = importDefSigSpec(cell->getPort("\\Y"), timestep);
+
+			std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q;
+			ez->assume(ez->vec_eq(d, qq));
+
+			if (model_undef)
+			{
+				std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1);
+				std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep);
+
+				ez->assume(ez->vec_eq(undef_d, undef_q));
+				undefGating(q, qq, undef_q);
+			}
+			return true;
+		}
+
 		if (cell->type == "$_BUF_" || cell->type == "$equiv")
 		{
 			std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
-- 
cgit v1.2.3