diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-12-11 14:24:19 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-12-11 14:24:19 +0100 |
| commit | 82d1fd77de31aece7b8a4f31fa53cb9dda2ec5f6 (patch) | |
| tree | 9ca6792bf3517a9aecf7819971b9d369e6a804b0 /backends/btor | |
| parent | cc119b5232a7f9aa201595d32b08e4e6f519dd3c (diff) | |
| download | yosys-82d1fd77de31aece7b8a4f31fa53cb9dda2ec5f6.tar.gz yosys-82d1fd77de31aece7b8a4f31fa53cb9dda2ec5f6.tar.bz2 yosys-82d1fd77de31aece7b8a4f31fa53cb9dda2ec5f6.zip | |
Add btor $shift/$shiftx support
Diffstat (limited to 'backends/btor')
| -rw-r--r-- | backends/btor/btor.cc | 40 | ||||
| -rw-r--r-- | backends/btor/test_cells.sh | 4 |
2 files changed, 37 insertions, 7 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index cd6430090..7b80427b8 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -123,7 +123,7 @@ struct BtorWorker if (cell->type.in("$shl", "$sshl")) btor_op = "sll"; if (cell->type == "$shr") btor_op = "srl"; if (cell->type == "$sshr") btor_op = "sra"; - // if (cell->type.in("$shift", "$shiftx")) btor_op = "shift"; + if (cell->type.in("$shift", "$shiftx")) btor_op = "shift"; 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"; @@ -139,6 +139,9 @@ struct BtorWorker 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; + if (btor_op == "shift" && !b_signed) + btor_op = "srl"; + if (cell->type.in("$shl", "$sshl", "$shr", "$sshr")) b_signed = false; @@ -146,11 +149,38 @@ struct BtorWorker btor_op = "srl"; int sid = get_bv_sid(width); - 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 nid; - int nid = next_nid++; - btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); + if (btor_op == "shift") + { + int nid_a = get_sig_nid(cell->getPort("\\A"), width, false); + int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + + int nid_r = next_nid++; + btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); + + int nid_b_neg = next_nid++; + btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b); + + int nid_l = next_nid++; + btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg); + + int sid_bit = get_bv_sid(1); + int nid_zero = get_sig_nid(Const(0, width)); + int nid_b_ltz = next_nid++; + btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero); + + nid = next_nid++; + btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r); + } + else + { + int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); + int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); + + nid = next_nid++; + btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); + } SigSpec sig = sigmap(cell->getPort("\\Y")); diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh index 0dc8ad854..e0f1a0514 100644 --- 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 /$shift /$shiftx' +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod' 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 -v ${fn%.il}.btor > ${fn%.il}.out + boolectormc -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 |