3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-27 10:55:51 +00:00

write_btor: support $_BUF_

This commit is contained in:
George Rennie 2024-11-15 11:47:09 +01:00
parent 9047290683
commit d7c6688905

View file

@ -508,7 +508,7 @@ struct BtorWorker
goto okay; goto okay;
} }
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf))) if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf), ID($_BUF_)))
{ {
string btor_op; string btor_op;
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
@ -522,7 +522,7 @@ struct BtorWorker
// the $pos/$buf cells just pass through, all other cells need an actual operation applied // the $pos/$buf cells just pass through, all other cells need an actual operation applied
int nid = nid_a; int nid = nid_a;
if (!cell->type.in(ID($pos), ID($buf))) if (!cell->type.in(ID($pos), ID($buf), ID($_BUF_)))
{ {
log_assert(!btor_op.empty()); log_assert(!btor_op.empty());
int sid = get_bv_sid(width); int sid = get_bv_sid(width);