diff options
| author | Jannis Harder <me@jix.one> | 2022-05-25 12:25:04 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-05-25 12:25:04 +0200 |
| commit | 8e9471c695598a48ee30ff044ab6bf1564f998ef (patch) | |
| tree | c73588e55bff9236ac6c902f2698a1b148ab76b5 | |
| parent | 904e2efe11926c81ccce0f643a903f9a71474ecd (diff) | |
| parent | d53479a0d6e7c799e29c18cae47f96dfabee9d21 (diff) | |
| download | yosys-8e9471c695598a48ee30ff044ab6bf1564f998ef.tar.gz yosys-8e9471c695598a48ee30ff044ab6bf1564f998ef.tar.bz2 yosys-8e9471c695598a48ee30ff044ab6bf1564f998ef.zip | |
Merge pull request #3335 from programmerjake/divfloor-in-write_smt2
add $divfloor support to write_smt2
| -rw-r--r-- | backends/smt2/smt2.cc | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a3628197e..ed6f3aff9 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -649,6 +649,27 @@ struct Smt2Worker return export_bvop(cell, "(bvurem A B)", 'd'); } } + // "div" = flooring division + if (cell->type == ID($divfloor)) { + if (cell->getParam(ID::A_SIGNED).as_bool()) { + // bvsdiv is truncating division, so we can't use it here. + int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B))); + width = max(width, GetSize(cell->getPort(ID::Y))); + auto expr = stringf("(let (" + "(a_neg (bvslt A #b%0*d)) " + "(b_neg (bvslt B #b%0*d))) " + "(let ((abs_a (ite a_neg (bvneg A) A)) " + "(abs_b (ite b_neg (bvneg B) B))) " + "(let ((u (bvudiv abs_a abs_b)) " + "(adj (ite (= #b%0*d (bvurem abs_a abs_b)) #b%0*d #b%0*d))) " + "(ite (= a_neg b_neg) u " + "(bvneg (bvadd u adj))))))", + width, 0, width, 0, width, 0, width, 0, width, 1); + return export_bvop(cell, expr, 'd'); + } else { + return export_bvop(cell, "(bvudiv A B)", 'd'); + } + } if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) && 2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) { |