diff options
| author | Jannis Harder <me@jix.one> | 2022-04-20 17:49:48 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-04-20 17:49:48 +0200 |
| commit | c7ef0f2932b9857c26cd61d1c93bb477e4e1aa23 (patch) | |
| tree | f805e5cac90e6e40bf3b6e28618b51db8fd2d905 /backends | |
| parent | 29c0a595892f36ca8755386c448105f8e2f499d6 (diff) | |
| download | yosys-c7ef0f2932b9857c26cd61d1c93bb477e4e1aa23.tar.gz yosys-c7ef0f2932b9857c26cd61d1c93bb477e4e1aa23.tar.bz2 yosys-c7ef0f2932b9857c26cd61d1c93bb477e4e1aa23.zip | |
smt2: Make write port array stores conditional on nonzero write mask
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 6 |
1 files changed, 4 insertions, 2 deletions
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))); } } |