To reduce dynamic power dissipation in digital circuits, a dependency graph (DG) is derived for a sequential circuit to accomplish verification and synthesis of clock-gated circuits. This is used recursively to derive sufficient conditions for a given bank of flops (flip-flops) to be legally clock gated (disabled.) These conditions are expressed with linear temporal logic (LTL)/past LTL (PLTL) properties, which can be used to create hardware monitors and justified by hardware model checkers. For sequential equivalence checking (SEC), LTL/PLTL properties are formulated to be proved on a clock-gated circuit (R) derived from a “golden” circuit (G). If these sufficient conditions can be proved on R, then the clock gating structures are proved redundant and can be removed. This creates a simplified circuit (R') and makes the SEC task easier. Experiments were performed on a set of benchmarks. It was observed that since the properties are expressed in terms of the control signals which only appear in the DG, they are quite easy to prove on R because the DG abstracts away complicated arithmetic logic. Similarly, the miter between G and R' is usually proved easily by model-checking methods because of the increased similarity between G and R' in sequential behaviors, compared to the changes between G and R. The proposed formulation is extended to provide a systematic and automatic method for sequential clock-gating synthesis. Experiments showed that the DG-based framework for synthesis gave encouraging results.

Sequential clock-gating can lead to easier equivalence checking problems, compared to the general sequential equivalence checking (SEC) problem. Modern sequential clock-gating techniques introduce control structures to disable unnecessary clocking. This violates combinational equivalence but maintains sequential equivalence between the original and revised circuits. We propose the use of characteristic graphs (CGs) to extract essential LTL clock-gating properties, which when proved imply certain sequential redundancies. The extraction, proof and subsequent removal of the implied redundancies lead to an efficient SEC procedure for clock-gated circuits. Experiments show that the proposed SEC procedure substantially outperforms existing methods in terms of speed and scalability when applied to several difficult cases.