From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 30 Aug 2016 09:26:10 +0000 (+0200)
Subject: Added $anyconst support to smt2 back-end
X-Git-Tag: yosys-0.7~91
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39e4faa2e4c51c9588df233c795b4e85523879cf;p=yosys.git

Added $anyconst support to smt2 back-end
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index af048859c..43601cd24 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -403,6 +403,16 @@ struct Smt2Worker
 				return;
 			}
 
+			if (cell->type == "$anyconst")
+			{
+				registers.insert(cell);
+				decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+						get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
+				register_bv(cell->getPort("\\Y"), idcounter++);
+				recursive_cells.erase(cell);
+				return;
+			}
+
 			if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
 			if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
 			if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
@@ -677,6 +687,13 @@ struct Smt2Worker
 					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
 				}
 
+				if (cell->type == "$anyconst")
+				{
+					std::string expr_d = get_bv(cell->getPort("\\Y"));
+					std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
+					trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
+				}
+
 				if (cell->type == "$mem")
 				{
 					int arrayid = memarrays.at(cell);