diff options
| -rw-r--r-- | backends/btor/btor.cc | 56 | ||||
| -rw-r--r-- | kernel/rtlil.cc | 2 | ||||
| -rw-r--r-- | kernel/rtlil.h | 8 |
3 files changed, 63 insertions, 3 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 53359bd7b..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++) @@ -932,9 +985,8 @@ struct BtorWorker btorf_push(stringf("output %s", log_id(wire))); - int sid = get_bv_sid(GetSize(wire)); int nid = get_sig_nid(wire); - btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire)); + btorf("%d output %d %s\n", next_nid++, nid, log_id(wire)); btorf_pop(stringf("output %s", log_id(wire))); } diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index d0fa88890..b3214579d 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -3237,7 +3237,7 @@ void RTLIL::SigSpec::extend_u0(int width, bool is_signed) remove(width, width_ - width); if (width_ < width) { - RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::S0; + RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::Sx; if (!is_signed) padding = RTLIL::State::S0; while (width_ < width) diff --git a/kernel/rtlil.h b/kernel/rtlil.h index 01323d112..52496e702 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -546,6 +546,14 @@ struct RTLIL::Const return ret; } + void extu(int width) { + bits.resize(width, RTLIL::State::S0); + } + + void exts(int width) { + bits.resize(width, bits.empty() ? RTLIL::State::Sx : bits.back()); + } + inline unsigned int hash() const { unsigned int h = mkhash_init; for (auto b : bits) |