Use of Formal Methods in Validating Power Controllers

Power domains are required in the design due to stringent active and standby power specifications. Depending upon various modes of operation of a chip, power domains allow parts of a chip to be powered on/off independently from the rest of the chip. This has become common in all handheld and portable applications where stringent power requirements are a major competitive concern.

Even with a design with a few power domains, say 4 or 5, a set of power on resettable registers are needed that provide appropriate controls for turning on/off power domains, power domain isolation control, and clock gating control for power events. Add state retention techniques to the mix, then you also have to include save and restore controls in you power manager.

Power manager or power controller is critical to the correct functionality of your chip and needs to work correct with the software interface since typical software commands include switching power on/off to a domain, enabling/disabling clock, and reset. Power states can be altered in many different ways and a pure-simulation based approach to validate all of this can be challenging. Power management features can be written as formal properties or assertions that can be formally validated by formal tools such as Synopsys’ Magellan.

Once the power management architecture is well understood, the rest of the task involves writing assertions using a properties specification language such as SystemVerilog Assertions (SVA). Some examples are as follows:

• Power Manager sequences through a set of possible states that are determined by different modes of operation of the chip. A set of properties can be written to ensure valid transitions and sequencing in this power manager under all possible circumstances.
• Various power states correspond to appropriate register values in the registers that can be programmed by software for enabling/disabling power domains and clocks. These values can be formally checked to be present upon reset. Ensuring that soft reset control does not conflict with hard reset controls leading to lock up situations.
• Power manager would typically follow a power sequencing protocol which includes relative timing of control signals which can be written as assertions with reference to appropriate number of clock cycles.
• Power domains themselves may be related in the way they power on/off. Hierarchical power domains are used which place constraints on how lower-level power domains are powered depending upon the state of higher-level power domains.
• You have to sequence power domains in test mode and JTAG access to the power controlling registers must be present by ensuring both system and JTAG clocks are running. If JTAG is connected then none of the domains on the path can be in power down mode.

Formal validation of power manager has several obvious advantages: i) It reduces the number of test cases that need to be written for validating complex power managers, ii) It reduces the amount of simulation cycles you may end using in validating some of the corner cases and difficult to target power manager bugs, iii) It allows simulation resources to be focused on remaining issues and coverage areas, and iv) It increases your verification confidence and reduces possible chances of re-spin due to a power issue. An area of further improvement from automation standpoint is more direct support of power architecture specification in terms of automatically figuring some of the formal needs for a given design.