MCBCG: Model Checking Based Sequential Clock-Gating

Dynamic power reduction techniques such as sequential clock-gating aim at eliminating inconsequential computation and clock-toggles of the registers. Usually sequential clock-gating opportunities are discovered manually based on certain characteristics of a design (e.g. pipelining). Since manual addition of sequential gating circuitry might change the functionality of the design, sequential equivalence checking is needed after such changes. Tools for sequential equivalence checking are expensive, and based on recent technologies. Therefore, it is desirable to automate the discovery of sequential clock-gating opportunities using already existing and proven technologies such as model checking and thereby a priori proving that the changes will not affect the required functionality. Model Checking Based Sequential Clock Gating (MCBCG) method formally proves particular sequential dependencies of registers on other registers and logic, thus sequentially gating such registers will not require further validation. An automation scheme for MCBCG methodology is also proposed in this paper. Preliminary experiments show up to 30% more savings than the traditional (combinational) clock-gating based power reduction techniques.