diff options
Diffstat (limited to 'backends/btor')
| -rw-r--r-- | backends/btor/btor.cc | 30 | ||||
| -rwxr-xr-x[-rw-r--r--] | backends/btor/test_cells.sh | 4 |
2 files changed, 21 insertions, 13 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9ac312480..5abab8978 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -205,9 +205,8 @@ struct BtorWorker if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort(ID::Y)); - width = std::max(width, GetSize(cell->getPort(ID::A))); - width = std::max(width, GetSize(cell->getPort(ID::B))); + int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); + int width = std::max(width_ay, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; @@ -224,11 +223,23 @@ struct BtorWorker int sid = get_bv_sid(width); int nid; + int nid_a; + if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) { + // sign-extend A up to the width of Y + int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed); + + // zero-extend the rest + int zeroes = get_sig_nid(Const(0, width-width_ay)); + nid_a = next_nid++; + btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded); + } else { + nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + } + + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); + if (btor_op == "shift") { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, false); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - int nid_r = next_nid++; btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); @@ -248,9 +259,6 @@ struct BtorWorker } else { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - nid = next_nid++; btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } @@ -1335,7 +1343,7 @@ struct BtorWorker struct BtorBackend : public Backend { BtorBackend() : Backend("btor", "write design to BTOR file") { } - void help() YS_OVERRIDE + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); @@ -1359,7 +1367,7 @@ struct BtorBackend : public Backend { log(" Output symbols for internal netnames (starting with '$')\n"); log("\n"); } - void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE + void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override { bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false; string info_filename; diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh index 3f077201a..0a011932d 100644..100755 --- a/backends/btor/test_cells.sh +++ b/backends/btor/test_cells.sh @@ -6,7 +6,7 @@ rm -rf test_cells.tmp mkdir -p test_cells.tmp cd test_cells.tmp -../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor' +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx' for fn in test_*.il; do ../../../yosys -p " @@ -19,7 +19,7 @@ for fn in test_*.il; do hierarchy -top main write_btor ${fn%.il}.btor " - boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out + btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out if grep " SATISFIABLE" ${fn%.il}.out; then echo "Check failed for ${fn%.il}." exit 1 |