diff options
Diffstat (limited to 'backends/btor/btor.cc')
| -rw-r--r-- | backends/btor/btor.cc | 118 |
1 files changed, 105 insertions, 13 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 58d2a862..55c49499 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -133,12 +133,13 @@ struct BtorWorker cell_recursion_guard.insert(cell); btorf_push(log_id(cell)); - if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", - "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) + if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", + "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) { string btor_op; if (cell->type == "$add") btor_op = "add"; if (cell->type == "$sub") btor_op = "sub"; + if (cell->type == "$mul") btor_op = "mul"; if (cell->type.in("$shl", "$sshl")) btor_op = "sll"; if (cell->type == "$shr") btor_op = "srl"; if (cell->type == "$sshr") btor_op = "sra"; @@ -146,6 +147,7 @@ struct BtorWorker if (cell->type.in("$and", "$_AND_")) btor_op = "and"; if (cell->type.in("$or", "$_OR_")) btor_op = "or"; if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor"; + if (cell->type == "$concat") btor_op = "concat"; if (cell->type == "$_NAND_") btor_op = "nand"; if (cell->type == "$_NOR_") btor_op = "nor"; if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor"; @@ -214,6 +216,40 @@ struct BtorWorker goto okay; } + if (cell->type.in("$div", "$mod")) + { + string btor_op; + if (cell->type == "$div") btor_op = "div"; + if (cell->type == "$mod") btor_op = "rem"; + log_assert(!btor_op.empty()); + + int width = GetSize(cell->getPort("\\Y")); + width = std::max(width, GetSize(cell->getPort("\\A"))); + width = std::max(width, GetSize(cell->getPort("\\B"))); + + bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; + bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; + + int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); + int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + + int sid = get_bv_sid(width); + int nid = next_nid++; + btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b); + + SigSpec sig = sigmap(cell->getPort("\\Y")); + + if (GetSize(sig) < width) { + int sid = get_bv_sid(GetSize(sig)); + int nid2 = next_nid++; + btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1); + nid = nid2; + } + + add_nid_sig(nid, sig); + goto okay; + } + if (cell->type.in("$_ANDNOT_", "$_ORNOT_")) { int sid = get_bv_sid(1); @@ -506,6 +542,18 @@ struct BtorWorker } } + Const initval; + for (int i = 0; i < GetSize(sig_q); i++) + if (initbits.count(sig_q[i])) + initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); + else + initval.bits.push_back(State::Sx); + + int nid_init_val = -1; + + if (!initval.is_fully_undef()) + nid_init_val = get_sig_nid(initval); + int sid = get_bv_sid(GetSize(sig_q)); int nid = next_nid++; @@ -514,15 +562,7 @@ struct BtorWorker else btorf("%d state %d %s\n", nid, sid, log_id(symbol)); - Const initval; - for (int i = 0; i < GetSize(sig_q); i++) - if (initbits.count(sig_q[i])) - initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); - else - initval.bits.push_back(State::Sx); - - if (!initval.is_fully_undef()) { - int nid_init_val = get_sig_nid(initval); + if (nid_init_val >= 0) { int nid_init = next_nid++; if (verbose) btorf("; initval = %s\n", log_signal(initval)); @@ -575,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(); @@ -601,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; @@ -609,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++) @@ -892,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))); } |