write_btor: support $barrier, $buf and $_BUF_

This commit is contained in:
George Rennie
2026-09-30 09:52:46 +02:00
committed by nella
parent 7871fe3c28
commit 80c6a7eaf3
+3 -3
View File
@@ -507,7 +507,7 @@ struct BtorWorker
goto okay;
}
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf), ID($_BUF_)))
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf), ID($_BUF_), ID($barrier)))
{
string btor_op;
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
@@ -519,9 +519,9 @@ struct BtorWorker
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
SigSpec sig = sigmap(cell->getPort(ID::Y));
// the $pos/$buf cells just pass through, all other cells need an actual operation applied
// buffer cells just pass through, all other cells need an actual operation applied
int nid = nid_a;
if (!cell->type.in(ID($pos), ID($buf), ID($_BUF_)))
if (!cell->type.in(ID($pos), ID($buf), ID($_BUF_), ID($barrier)))
{
log_assert(!btor_op.empty());
int sid = get_bv_sid(width);