Static And Formal Verification Of Power-Aware Designs At The RTL Level Using UPF
The constant scaling of transistors has made power one of the critical design constraints. Convergence of various technologies in portable battery operated devices has put pressure on designers to reduce leakage and maximize battery life. As a result, they utilize various power management techniques to reduce power consumption in their designs. Thus, designs consist of multiple operating voltages, power islands, multi-threshold devices, and different sleep modes (voltages).
A common problem that exists with power-related verification of multi-voltage designs involves the accurate placing of level shifters and isolation cells. Normally, these are done manually or by using scripts, and they are inserted during or after synthesis. These techniques are error prone and cause unique verification problems that are difficult to rectify and typically require costly respins. The new Unified Power Format (UPF) low power specification standard allows designers to explicitly specify the insertion of isolation cells and level shifters at the RTL. The requirement for level shifting is static. It is based on the specification of voltage domains (voltage(s) at which a power domain may operate within specific system power states). Deferring validation of an electrically correct supply network to simulation needlessly burdens the simulator with checks that can be performed statically. It also raises the risk that the simulation tests will fail to expose potential problems. Therefore, a static, lint-type check for level shifters and isolation is needed.
In this paper, we demonstrate a technique that leads designers to places in the design that are prone to bugs related to multivoltage paths. The power intent is specified by the user in UPF and includes specification of the power domains, system power states, switches, and other power management features. This information will be used by the tool to perform static lint checking related to power/voltage domain crossings that are normally very difficult to figure out from simulation data. We also present formal verification techniques that can be automated by the tool to reduce the burden on the designer. These techniques involve generating assertions, which test the power control sequencing, check for invalid sleep mode transitions, and catch the race condition between the retention controls (e.g., save and restore) and design controls (e.g., clock, set, reset).
Tags: Mentor Graphics, UPF