mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 09:55:20 +00:00
Code Activity

Fix signed $shift/$shiftx handling in write_smt2

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-03-09 13:19:41 -08:00
parent 399ab16315
commit 94f995ee37
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
backends/smt2/smt2.cc
View file

@ -416,6 +416,7 @@ struct Smt2Worker
for (char ch : expr) { for (char ch : expr) {
if (ch == 'A') processed_expr += get_bv(sig_a); if (ch == 'A') processed_expr += get_bv(sig_a);
else if (ch == 'B') processed_expr += get_bv(sig_b); else if (ch == 'B') processed_expr += get_bv(sig_b);
else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
else processed_expr += ch; else processed_expr += ch;
@ -554,7 +555,7 @@ struct Smt2Worker
if (cell->type.in("$shift", "$shiftx")) { if (cell->type.in("$shift", "$shiftx")) {
if (cell->getParam("\\B_SIGNED").as_bool()) { if (cell->getParam("\\B_SIGNED").as_bool()) {
return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
"(bvlshr A B) (bvlshr A (bvneg B)))", "(bvlshr A B) (bvlshr A (bvneg B)))",
GetSize(cell->getPort("\\B")), 0), 's'); GetSize(cell->getPort("\\B")), 0), 's');
} else { } else {