diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-12-17 18:55:17 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-12-17 18:55:17 +0100 |
| commit | bbdcc1f9d42618a4a7770868a96e3214dd20f07c (patch) | |
| tree | 1c0a962bcf275ae62345ccd433c61510d5d4044d /backends | |
| parent | 8e22e8118a2a8b13bb24270862af37d93f53dbe8 (diff) | |
| download | yosys-bbdcc1f9d42618a4a7770868a96e3214dd20f07c.tar.gz yosys-bbdcc1f9d42618a4a7770868a96e3214dd20f07c.tar.bz2 yosys-bbdcc1f9d42618a4a7770868a96e3214dd20f07c.zip | |
Improve BTOR memory encoding
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index b0c51579c..dd041bfaa 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -599,6 +599,7 @@ struct BtorWorker SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN")); int data_sid = get_bv_sid(width); + int bool_sid = get_bv_sid(1); int sid = get_mem_sid(abits, width); int nid = next_nid++; int nid_head = nid; @@ -638,7 +639,13 @@ struct BtorWorker int nid7 = next_nid++; btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - nid_head = nid7; + int nid8 = next_nid++; + btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + + int nid9 = next_nid++; + btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + + nid_head = nid9; } } @@ -977,6 +984,7 @@ struct BtorWorker SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN")); int data_sid = get_bv_sid(width); + int bool_sid = get_bv_sid(1); int sid = get_mem_sid(abits, width); int nid_head = nid; @@ -1008,7 +1016,13 @@ struct BtorWorker int nid7 = next_nid++; btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - nid_head = nid7; + int nid8 = next_nid++; + btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + + int nid9 = next_nid++; + btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + + nid_head = nid9; } int nid2 = next_nid++; |