From 80c6a7eaf37da031b1b3e0c15997db6ea5c52cd5 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 20 Nov 2024 13:57:29 +0100 Subject: [PATCH] write_btor: support $barrier, $buf and $_BUF_ --- backends/btor/btor.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 51f28afcd..84b0cc970 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -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);