From 9047290683467fe981684462abf0d3d89191d148 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 6 Nov 2024 19:49:09 +0100 Subject: [PATCH 1/2] write_btor: support $buf * treated the same as $pos --- 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 c3637bc8f95..2def5eaba18 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -508,7 +508,7 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos))) + if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf))) { string btor_op; if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; @@ -520,9 +520,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 cell just passes 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; - if (cell->type != ID($pos)) + if (!cell->type.in(ID($pos), ID($buf))) { log_assert(!btor_op.empty()); int sid = get_bv_sid(width); From d7c66889052854a40d577e8d216c328256cd869a Mon Sep 17 00:00:00 2001 From: George Rennie Date: Fri, 15 Nov 2024 11:47:09 +0100 Subject: [PATCH 2/2] write_btor: support $_BUF_ --- backends/btor/btor.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 2def5eaba18..ad8f4b680e3 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -508,7 +508,7 @@ struct BtorWorker 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; 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 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()); int sid = get_bv_sid(width);