Static and Formal Verification of Power Aware Designs at the RTL Using UPF

ABSTRACT

The Unified Power Format (UPF) low power specification standard allows designers to explicitly specify the insertion of isolation cells and level shifters at the RTL. In this paper, Rudra Mukherjee and his colleagues demonstrate a technique that leads designers to places in the design that are prone to bugs related to multi-voltage 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. Mukherjee and his coauthors 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).