diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-12-10 08:40:11 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-12-10 08:40:11 +0100 |
| commit | cc119b5232a7f9aa201595d32b08e4e6f519dd3c (patch) | |
| tree | 66c034524a344e8a26f3c02534bc259d827bcefa | |
| parent | 133a0f497865c76e3e9c42ced93eb7f5d349ade6 (diff) | |
| download | yosys-cc119b5232a7f9aa201595d32b08e4e6f519dd3c.tar.gz yosys-cc119b5232a7f9aa201595d32b08e4e6f519dd3c.tar.bz2 yosys-cc119b5232a7f9aa201595d32b08e4e6f519dd3c.zip | |
Fix btor back-end shift handling
| -rw-r--r-- | backends/btor/btor.cc | 10 | ||||
| -rw-r--r-- | backends/btor/test_cells.sh | 2 |
2 files changed, 7 insertions, 5 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 6e8da4707..cd6430090 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -114,7 +114,7 @@ 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", + if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) { string btor_op; @@ -123,6 +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("$and", "$_AND_")) btor_op = "and"; if (cell->type.in("$or", "$_OR_")) btor_op = "or"; if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor"; @@ -138,10 +139,11 @@ 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 (cell->type.in("$shl", "$shr")) { - a_signed = false; + if (cell->type.in("$shl", "$sshl", "$shr", "$sshr")) b_signed = false; - } + + if (cell->type == "$sshr" && !a_signed) + btor_op = "srl"; int sid = get_bv_sid(width); int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh index c3572bc93..0dc8ad854 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 /$shl /$shr /$sshl /$sshr /$shift /$shiftx' +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$shift /$shiftx' for fn in test_*.il; do ../../../yosys -p " |