SAT-based synthesis of clock gating functions using 3-valued abstraction

Clock gating is a power reduction technique for digital circuits that works by eliminating unnecessary switching of parts of the clock network, a power-hungry component in hardware designs. An effective approach to clock gating synthesis is based on a functional analysis of the design using BDDs. Algorithms of this type attempt to build a BDD for a clock gating circuit and then reduce its size with an approximation. If the BDD of a particular latch grows too large the attempt to gate that latch is aborted. We replace BDDs with a SAT-based technique combined with 3-valued abstraction. Our technique generates the approximation directly from the circuit, and thus avoids the explosion. Furthermore, our technique is incremental in the sense that it produces a partial result (a weaker approximation) if time or memory limits are exceeded. Our experimentation shows that more than 70% of latches that could not be gated using the BDD-based approach were gated by the SAT-based method.