3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00

Respect \A_SIGNED for $shift

This reflects the behaviour of $shr/$shl, which sign-extend their A
operands to the size of their output, then do a logical shift (shift in
0-bits).
This commit is contained in:
Xiretza 2020-07-03 13:13:21 +02:00 committed by Marcelina Kościelnicka
parent 22765ef0a5
commit 928fd40c2e
7 changed files with 61 additions and 65 deletions

View file

@ -205,9 +205,8 @@ struct BtorWorker
if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor";
log_assert(!btor_op.empty());
int width = GetSize(cell->getPort(ID::Y));
width = std::max(width, GetSize(cell->getPort(ID::A)));
width = std::max(width, GetSize(cell->getPort(ID::B)));
int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
int width = std::max(width_ay, GetSize(cell->getPort(ID::B)));
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
@ -224,11 +223,23 @@ struct BtorWorker
int sid = get_bv_sid(width);
int nid;
int nid_a;
if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) {
// sign-extend A up to the width of Y
int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed);
// zero-extend the rest
int zeroes = get_sig_nid(Const(0, width-width_ay));
nid_a = next_nid++;
btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded);
} else {
nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
}
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
if (btor_op == "shift")
{
int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
int nid_r = next_nid++;
btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
@ -248,9 +259,6 @@ struct BtorWorker
}
else
{
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
nid = next_nid++;
btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
}

4
backends/btor/test_cells.sh Normal file → Executable file
View file

@ -6,7 +6,7 @@ rm -rf test_cells.tmp
mkdir -p test_cells.tmp
cd test_cells.tmp
../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor'
../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx'
for fn in test_*.il; do
../../../yosys -p "
@ -19,7 +19,7 @@ for fn in test_*.il; do
hierarchy -top main
write_btor ${fn%.il}.btor
"
boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out
if grep " SATISFIABLE" ${fn%.il}.out; then
echo "Check failed for ${fn%.il}."
exit 1

View file

@ -750,21 +750,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf(" = ");
if (cell->getParam(ID::B_SIGNED).as_bool())
{
f << stringf("$signed(");
dump_sigspec(f, cell->getPort(ID::B));
f << stringf(")");
dump_cell_expr_port(f, cell, "B", true);
f << stringf(" < 0 ? ");
dump_sigspec(f, cell->getPort(ID::A));
dump_cell_expr_port(f, cell, "A", true);
f << stringf(" << - ");
dump_sigspec(f, cell->getPort(ID::B));
f << stringf(" : ");
dump_sigspec(f, cell->getPort(ID::A));
dump_cell_expr_port(f, cell, "A", true);
f << stringf(" >> ");
dump_sigspec(f, cell->getPort(ID::B));
}
else
{
dump_sigspec(f, cell->getPort(ID::A));
dump_cell_expr_port(f, cell, "A", true);
f << stringf(" >> ");
dump_sigspec(f, cell->getPort(ID::B));
}