Skip to content

Commit 4e25053

Browse files
committed
write_btor: support $barrier, $buf and $_BUF_
1 parent c0c42c8 commit 4e25053

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

backends/btor/btor.cc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -508,7 +508,7 @@ struct BtorWorker
508508
goto okay;
509509
}
510510

511-
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos)))
511+
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf), ID($_BUF_), ID($barrier)))
512512
{
513513
string btor_op;
514514
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
@@ -520,9 +520,9 @@ struct BtorWorker
520520
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
521521
SigSpec sig = sigmap(cell->getPort(ID::Y));
522522

523-
// the $pos cell just passes through, all other cells need an actual operation applied
523+
// buffer cells just pass through, all other cells need an actual operation applied
524524
int nid = nid_a;
525-
if (cell->type != ID($pos))
525+
if (!cell->type.in(ID($pos), ID($buf), ID($_BUF_), ID($barrier)))
526526
{
527527
log_assert(!btor_op.empty());
528528
int sid = get_bv_sid(width);

0 commit comments

Comments
 (0)