diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-12-18 19:59:29 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-18 19:59:29 +0100 |
| commit | 2d73e1b60a43f2a621b387768134b83054f59e89 (patch) | |
| tree | 613ccca3d1cfad1d36886867cdf8dfd7ed235347 | |
| parent | eddf075d934693471f77e92fb2cf687f69a59cb5 (diff) | |
| parent | abf5930a3325b8ae89f8cbb89a0f963e316c0889 (diff) | |
| download | yosys-2d73e1b60a43f2a621b387768134b83054f59e89.tar.gz yosys-2d73e1b60a43f2a621b387768134b83054f59e89.tar.bz2 yosys-2d73e1b60a43f2a621b387768134b83054f59e89.zip | |
Merge pull request #748 from makaimann/add-btor-ops
Add btor ops for $mul, $div, $mod and $concat
| -rw-r--r-- | backends/btor/btor.cc | 40 | ||||
| -rwxr-xr-x[-rw-r--r--] | backends/btor/test_cells.sh | 0 |
2 files changed, 38 insertions, 2 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index ab2702807..d3fb9b858 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); diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh index e0f1a0514..e0f1a0514 100644..100755 --- a/backends/btor/test_cells.sh +++ b/backends/btor/test_cells.sh |