mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 01:24:10 +00:00
Code Activity

add $divfloor support to write_smt2

Browse source 
Fixes: #3330
This commit is contained in:
Jacob Lifshay 2022-05-24 01:34:25 -07:00
parent c525b5f919
commit d53479a0d6
1 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
backends/smt2/smt2.cc
View file

@ -649,6 +649,27 @@ struct Smt2Worker
return export_bvop(cell, "(bvurem A B)", 'd'); 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)) && 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))) { 2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {