Formal verification of low-power designs encompasses two elements: low-power verification and logical equivalency. For low-power verification, the focus is on ensuring that the design is electrically correct from a low-power perspective. The flow will verify that the retention and isolation are complete and correct as specified by the power intent.
Checks at this stage include tests for missing isolation or level shifter cells, checks that state retention and isolation control signals are driven correctly by domains that remain powered up, and tests for power control functionality. In later stages of the flow (post placement), these checks also ensure that gate power pins are hooked to the appropriate power rails, that the always-on cells are appropriately powered, and that there are no “sneak” paths from power-down domains back to logic.
Logical equivalency adds to the classic logical comparison. Logical equivalency checks (LEC) have been used for a number of years. The addition of low-power structures increases the complexity because isolation and state retention cells have been added to the netlist. These cells are not in the RTL, but are specified in a power intent document. So the LEC tool must be able to formally prove that the synthesis engine has inserted these cells correctly, and that the netlist is logically equivalent to the golden RTL and power intent.
Note that these checks should be run throughout the entire flow. In particular, it is important to run these checks after synthesis and test logic insertion, and after place-and-route (before tapeout). After tapeout quality routing, the checks should be run on a physical netlist, with power and ground connections.
Page contents originally provided by Cadence Design Systems