Add support for memory initialization to write_btor

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 96044e3395e9198621614743738e631bf29614ad..55c494996463c0bc14118f29a9de80af1d4dde81 100644 (file)
--- 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++)