riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Improve SMT2 encoding of $reduce_{and,or,bool} 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-04 21:22:20 +01:00
parent 45a6fce92c
commit 8b7602e660
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
backends/smt2/smt2.cc
View File

@ -379,7 +379,8 @@ struct Smt2Worker
if (type == 's' || type == 'd' || type == 'b') {
width = max(width, GetSize(cell->getPort("\\A")));
width = max(width, GetSize(cell->getPort("\\B")));
if (cell->hasPort("\\B"))
width = max(width, GetSize(cell->getPort("\\B")));
}
if (cell->hasPort("\\A")) {
@ -561,6 +562,13 @@ struct Smt2Worker
if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
bool is_and = cell->type == "$reduce_and";
string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0');
return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
}
if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);