A study on Low Power Check and Formal Verification

Low power techniques such as clock gating, power gating, multi-voltage, multi-threshold, etc. are utilized, to decrease the power dissipation in the design. To verify the proper implementation of these techniques, a low power check is used. Different special low-power cells such as Isolation cells, Level Shifter cells, Retention cells are discussed. Implementation of power-aware design is explained using Unified power format (UPF). In an Application Specific Integrated Circuit (ASIC) design flow, from Register-transfer level (RTL) to Graphic Database System (GDSII), netlist undergoes many changes in the process of synthesis, Design for Testability (DFT) insertion, and Placement and Routing (PNR). Hence, formal verification has to performed to ensure whether its functionality remains the same. Basic mathematical algorithms underlying formal Verification such as Binary decision diagrams (BDD) and Satisfiability (SAT) solvers are discussed.