From 1eff8be8f018bd6b94efd14a959d6f1807dd056d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 23 Mar 2019 14:40:01 +0100 Subject: [PATCH] Add support for memory initialization to write_btor Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 53 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 96044e339..55c494996 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -615,6 +615,7 @@ struct BtorWorker { int abits = cell->getParam("\\ABITS").as_int(); int width = cell->getParam("\\WIDTH").as_int(); + int nwords = cell->getParam("\\SIZE").as_int(); int rdports = cell->getParam("\\RD_PORTS").as_int(); int wrports = cell->getParam("\\WR_PORTS").as_int(); @@ -641,6 +642,52 @@ struct BtorWorker int data_sid = get_bv_sid(width); int bool_sid = get_bv_sid(1); int sid = get_mem_sid(abits, width); + + Const initdata = cell->getParam("\\INIT"); + initdata.exts(nwords*width); + int nid_init_val = -1; + + if (!initdata.is_fully_undef()) + { + bool constword = true; + Const firstword = initdata.extract(0, width); + + for (int i = 1; i < nwords; i++) { + Const thisword = initdata.extract(i*width, width); + if (thisword != firstword) { + constword = false; + break; + } + } + + if (constword) + { + if (verbose) + btorf("; initval = %s\n", log_signal(firstword)); + nid_init_val = get_sig_nid(firstword); + } + else + { + int nid_init_val = next_nid++; + btorf("%d state %d\n", nid_init_val, sid); + + for (int i = 0; i < nwords; i++) { + Const thisword = initdata.extract(i*width, width); + if (thisword.is_fully_undef()) + continue; + Const thisaddr(i, abits); + int nid_thisword = get_sig_nid(thisword); + int nid_thisaddr = get_sig_nid(thisaddr); + int last_nid_init_val = nid_init_val; + nid_init_val = next_nid++; + if (verbose) + btorf("; initval[%d] = %s\n", i, log_signal(thisword)); + btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword); + } + } + } + + int nid = next_nid++; int nid_head = nid; @@ -649,6 +696,12 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(cell)); + if (nid_init_val >= 0) + { + int nid_init = next_nid++; + btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); + } + if (asyncwr) { for (int port = 0; port < wrports; port++) -- 2.30.2