projects
/
yosys.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
29c0a59
)
smt2: Make write port array stores conditional on nonzero write mask
author
Jannis Harder
<me@jix.one>
Wed, 20 Apr 2022 15:49:48 +0000
(17:49 +0200)
committer
Jannis Harder
<me@jix.one>
Wed, 20 Apr 2022 15:49:48 +0000
(17:49 +0200)
backends/smt2/smt2.cc
patch
|
blob
|
history
diff --git
a/backends/smt2/smt2.cc
b/backends/smt2/smt2.cc
index 9bf0de03ed3a1da647d91c82b11c800f245bb995..a3628197ec64a0b027331e8a0cdd2716284793e9 100644
(file)
--- 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());
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)) "
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+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)));
}
}
}
}