Tags:Formal Verification, Low Power Verification (LPV), Retention Optimization, Retention Sufficiency and SEC (Sequential Equivalence Checking)
Abstract:
State retention cells are critical design elements used to save and restore of design logic during power shutoff in a Low Power Design. Missing retention on an essential state element can lead to failures in Silicon. Verifying retention optimization for a low power design through non-exhaustive random techniques doesn't gurantee if the retention reduction(optimization) is safe. This has inspired people to try formal menthods for verifying complex problem like retention optimzation and retention sufficiency.Traditionally, formal tools haven't been used widely for doing LP verification and simulation has been the primary technology which is widely used for doing LP verification. But overtime this trend has changed and with the motication to do a left shift DV engineers at various have started exploring and applying formal flows for verifying of power aware designs. In this paper we present a new Low Power Verification (LPV) flow called "Retention Sufficiency", which uses exhaustive formal methodology to prove that the identified list of non-essential retention cells in a low power design can be safely removed/reduced from the design, and still maintain the original design functionality. The final reduced list of retention cells after successfull validation in formal will be the sub(optimal) list which is essentially required for retention sufficiency. Retention Sufficiency flow has been successfully run on multiple designs helping optimize/reduce non-essential retention cells in block level setups by upto 15%.
Retention Sufficiency Validation for Optimizing State Retention Cells in Low Power Design