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