Formal Analysis of Gate-Level Power Estimation in ASICs using Model Checking

Abstract

With the rapid increase of IoTs, power consumption is considered to be an essential performance parameter in ASICs. Power estimation is necessary to determine the minimum power budget, implement power optimization and reduction techniques and accordingly define the packaging and cooling environment to improve reliability of the chip. Early stage power estimation is preferred during the design flow. However, the power estimates at higher abstraction levels deviate up to 40% from real silicon. Whereas, the most accurate layout-level power estimation imparts a very high computational and redesign cost. Therefore, gate-level power analysis serves as a middleground for accurate power estimation with more redesign flexibility. Despite the significance and criticality of accurate power analysis, the state of the art gate-level power estimation tools use logic simulation based techniques, which merely consider a limited number of input vectors and thus provide imprecise power estimates that may threaten the chip’s reliability. In or der to address these issues, we propose a framework to formally estimate and verify the maximum bounds on each type of gate-level power consumption i.e. leakage, internal, switching and dynamic using the nuXmv model checker. In particular, this thesis presents the formal models for all the basic logic cells based on their characterized data in a standard cell library. Then the given netlist is translated into a state-space model using the for