From 4adef63cd484d81da08ae6b5fe49b1d5d4d0b369 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 17 Jun 2022 17:23:13 +0200 Subject: smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction This avoids provability regressions now that we infer more ROMs. This fixes #3378 --- backends/btor/btor.cc | 1 + 1 file changed, 1 insertion(+) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 7de5deadd..5be9bf324 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1402,6 +1402,7 @@ struct BtorBackend : public Backend { log_header(design, "Executing BTOR backend.\n"); log_push(); + Pass::call(design, "memory_map -rom-only"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From de5c4bf52320e1c19d79a13fcbe303f590d531c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Mon, 20 Jun 2022 16:39:53 -0700 Subject: btor: add support for $pos cell --- backends/btor/btor.cc | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 5be9bf324..7dec70545 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -446,25 +446,28 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($not), ID($neg), ID($_NOT_))) + if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos))) { string btor_op; if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not"; if (cell->type == ID($neg)) btor_op = "neg"; - log_assert(!btor_op.empty()); int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - - int sid = get_bv_sid(width); int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - - int nid = next_nid++; - btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - SigSpec sig = sigmap(cell->getPort(ID::Y)); + // the $pos cell just passes through, all other cells need an actual operation applied + int nid = nid_a; + if (cell->type != ID($pos)) + { + log_assert(!btor_op.empty()); + int sid = get_bv_sid(width); + nid = next_nid++; + btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); + } + if (GetSize(sig) < width) { int sid = get_bv_sid(GetSize(sig)); int nid2 = next_nid++; -- cgit v1.2.3 From d78d807a7fa1747b40da8bac9e278183cf86d3cc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 27 Jun 2022 15:47:55 +0200 Subject: memory_map: -keepdc option for formal Use it when invoking memory_map -rom-only from write_{smt2,btor}. --- backends/btor/btor.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 7dec70545..2dc3b5954 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1405,7 +1405,7 @@ struct BtorBackend : public Backend { log_header(design, "Executing BTOR backend.\n"); log_push(); - Pass::call(design, "memory_map -rom-only"); + Pass::call(design, "memory_map -rom-only -keepdc"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From 930bcf0e75f3b8d6c5afbdffda5ef7fd7eddc964 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 18:28:34 +0200 Subject: smt2, btor: Revert calling memory_map -rom-only This approach had major issues with ROMs whose initialization was not fully defined. If required, memory_map -rom-only -keepdc should be called early in a formal flow instead. (This does require a careful choice of optimization passes though. Sby's scripts will be updated accordingly.) --- backends/btor/btor.cc | 1 - 1 file changed, 1 deletion(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 2dc3b5954..831a3ada2 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1405,7 +1405,6 @@ struct BtorBackend : public Backend { log_header(design, "Executing BTOR backend.\n"); log_push(); - Pass::call(design, "memory_map -rom-only -keepdc"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:49:51 +0200 Subject: formalff: Set new replaced_by_gclk attribute on removed dff's clks This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute. --- backends/btor/btor.cc | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 831a3ada2..6dae7156a 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1112,6 +1112,16 @@ struct BtorWorker btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str()); add_nid_sig(nid, sig); + + if (!info_filename.empty()) { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr != wire->attributes.end()) { + if (gclk_attr->second == State::S1) + info_clocks[nid] |= 1; + else if (gclk_attr->second == State::S0) + info_clocks[nid] |= 2; + } + } } btorf_pop("inputs"); -- cgit v1.2.3 From 96a1173598ec1bf93670b2de3c8bb087f03a8528 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:59:39 +0200 Subject: btor: Support $anyinit cells --- backends/btor/btor.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 6dae7156a..06de71018 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -612,7 +612,7 @@ struct BtorWorker goto okay; } - if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) + if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) { SigSpec sig_d = sigmap(cell->getPort(ID::D)); SigSpec sig_q = sigmap(cell->getPort(ID::Q)); -- cgit v1.2.3