From bbdcc1f9d42618a4a7770868a96e3214dd20f07c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 17 Dec 2017 18:55:17 +0100 Subject: [PATCH] Improve BTOR memory encoding --- backends/btor/btor.cc | 18 ++++++++++++++++-- 1 file 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++; -- 2.30.2