mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Add btor $shift/$shiftx support

Browse source
This commit is contained in:
Clifford Wolf 2017-12-11 14:24:19 +01:00
parent cc119b5232
commit 82d1fd77de
2 changed files with 37 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

34
backends/btor/btor.cc
View file

@ -123,7 +123,7 @@ struct BtorWorker
if (cell->type.in("$shl", "$sshl")) btor_op = "sll"; if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
if (cell->type == "$shr") btor_op = "srl"; if (cell->type == "$shr") btor_op = "srl";
if (cell->type == "$sshr") btor_op = "sra"; if (cell->type == "$sshr") btor_op = "sra";
// if (cell->type.in("$shift", "$shiftx")) btor_op = "shift"; if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
if (cell->type.in("$and", "$_AND_")) btor_op = "and"; if (cell->type.in("$and", "$_AND_")) btor_op = "and";
if (cell->type.in("$or", "$_OR_")) btor_op = "or"; if (cell->type.in("$or", "$_OR_")) btor_op = "or";
if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor"; if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
@ -139,6 +139,9 @@ struct BtorWorker
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false; bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false; bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
if (btor_op == "shift" && !b_signed)
btor_op = "srl";
if (cell->type.in("$shl", "$sshl", "$shr", "$sshr")) if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
b_signed = false; b_signed = false;
@ -146,11 +149,38 @@ struct BtorWorker
btor_op = "srl"; btor_op = "srl";
int sid = get_bv_sid(width); int sid = get_bv_sid(width);
int nid;
if (btor_op == "shift")
{
int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
int nid_r = next_nid++;
btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
int nid_b_neg = next_nid++;
btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b);
int nid_l = next_nid++;
btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg);
int sid_bit = get_bv_sid(1);
int nid_zero = get_sig_nid(Const(0, width));
int nid_b_ltz = next_nid++;
btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
nid = next_nid++;
btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
}
else
{
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed); int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed); int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
int nid = next_nid++; nid = next_nid++;
btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b); btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
}
SigSpec sig = sigmap(cell->getPort("\\Y")); SigSpec sig = sigmap(cell->getPort("\\Y"));

4
backends/btor/test_cells.sh
View file

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