Novel SAT-based invariant-directed low-power synthesis

Dynamic power consumption is a critical concern in the design of both high performance and low-power circuits. Clock-gating is one of the most efficient and prominent approaches to reduce dynamic power. In this paper, (1) we propose the first scalable SAT-based approaches for Observability Dont Care (ODC) based clock gating; (2) we intelligently choose those inductive invariants candidates such that their validation will benefit clock-gating-based low-power design. Our approach shows an average 23.2% reduction in dynamic power with an average 9.5% increase in area.