The Model Checking View to Clock Gating and Operand Isolation

Clock gating and operand isolation are two techniques to reduce the power consumption in state-of-the-art hardware designs. Both approaches basically follow a two-step procedure: first, they statically analyze a hardware circuit to determine irrelevant computations. Second, all parts which are responsible for these computations are replaced by others that consume less power in the average case, either by dynamically gating clocks or by isolating operands. This paper focuses on the first phase, i.e. the computation of irrelevant computation. The core of our contribution is the definition of so-called passiveness conditions for each signal x, which indicate that the value currently carried by x does not contribute to the final result of the system. After showing how our theory can be generally used in the context of clock gating and operand isolation, we classify many state-of-the-art approaches and show that they are in fact conservative approximations of our general setting. Thereby, it defines the theoretical basis for adoption of these approaches in their entirety.