aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-08-02 15:49:51 +0200
committerJannis Harder <me@jix.one>2022-08-16 13:37:30 +0200
commita5e1d3b9974668b4ab526a6b77ca96f1aa16d01f (patch)
tree0c4308ab9831f550d6e6d34a79239b569944c427 /backends
parentc0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 (diff)
downloadyosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.tar.gz
yosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.tar.bz2
yosys-a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f.zip
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.
Diffstat (limited to 'backends')
-rw-r--r--backends/btor/btor.cc10
-rw-r--r--backends/smt2/smt2.cc11
2 files changed, 21 insertions, 0 deletions
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
@@ -241,6 +241,17 @@ struct Smt2Worker
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)
continue;
SigBit bit = sigmap(wire);