From: Jannis Harder <me@jix.one>
Date: Wed, 20 Apr 2022 15:49:48 +0000 (+0200)
Subject: smt2: Make write port array stores conditional on nonzero write mask
X-Git-Tag: yosys-0.17~20^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c7ef0f2932b9857c26cd61d1c93bb477e4e1aa23;p=yosys.git

smt2: Make write port array stores conditional on nonzero write mask
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9bf0de03e..a3628197e 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1185,10 +1185,12 @@ struct Smt2Worker
 						data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
 								data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
 
+						string empty_mask(mem->width, '0');
+
 						decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
-								"(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+								"(ite (= %s #b%s) (|%s#%d#%d| state) (store (|%s#%d#%d| state) %s %s))) ; %s\n",
 								get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
-								get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
+								mask.c_str(), empty_mask.c_str(), get_id(module), arrayid, i, get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
 					}
 				}