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') 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') 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