diff options
| author | clairexen <claire@symbioticeda.com> | 2020-05-29 16:37:23 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-29 16:37:23 +0200 |
| commit | 94c10353897c6b2b3f960bdd6647a5da9c1d9f2c (patch) | |
| tree | 695ca7d8b26c8c4268498c76e09c157d9846bde0 /backends/smt2 | |
| parent | af36afe722dc35b129351af592ef340e512e0292 (diff) | |
| parent | f88bef767263590c94e157d0989afa91db3ccdb0 (diff) | |
| download | yosys-94c10353897c6b2b3f960bdd6647a5da9c1d9f2c.tar.gz yosys-94c10353897c6b2b3f960bdd6647a5da9c1d9f2c.tar.bz2 yosys-94c10353897c6b2b3f960bdd6647a5da9c1d9f2c.zip | |
Merge pull request #1885 from Xiretza/mod-rem-cells
Fix modulo/remainder semantics
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 3e67e55f2..26f17bcb3 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -590,7 +590,17 @@ struct Smt2Worker if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)"); if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)"); if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd'); + // "rem" = truncating modulo if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd'); + // "mod" = flooring modulo + if (cell->type == ID($modfloor)) { + // bvumod doesn't exist because it's the same as bvurem + if (cell->getParam(ID::A_SIGNED).as_bool()) { + return export_bvop(cell, "(bvsmod A B)", 'd'); + } else { + return export_bvop(cell, "(bvurem 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))) { |