From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
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 ++++++++++
 backends/smt2/smt2.cc | 11 +++++++++++
 2 files changed, 21 insertions(+)

(limited to 'backends')

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");
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index f6c3560c1..126ee1175 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -239,6 +239,17 @@ struct Smt2Worker
 			clock_negedge.erase(bit);
 		}
 
+		for (auto wire : module->wires())
+		{
+			auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+			if (gclk_attr != wire->attributes.end()) {
+				if (gclk_attr->second == State::S1)
+					clock_posedge.insert(sigmap(wire));
+				else if (gclk_attr->second == State::S0)
+					clock_negedge.insert(sigmap(wire));
+			}
+		}
+
 		for (auto wire : module->wires())
 		{
 			if (!wire->port_input || GetSize(wire) != 1)
-- 
cgit v1.2.3