Optimizing power in complex devices is much simpler using formal verification techniques.
By Joe Hupcey III
It’s not surprising that power optimization is a critical part of today’s complex designs. Unbeknownst to most consumers is an underlying methodology that every design engineer must follow to make sure a consumer device meets the power requirements of the consumer—even if the consumer doesn’t realize they’re demanding it.
The situation in industrial products, such as servers and routers in cloud computing data centers, is equally acute. Running at lower power can save millions of dollars in electricity consumption and reduced HVAC capacity. Without a solid power optimization methodology, today’s devices would be stuck in the proverbial “stone ages,” with extremely limited functionality, painfully short battery life, and/or huge electricity and cooling bills. Therefore, without a solid power-aware design methodology, engineers could not deliver electronic devices that perform the necessary tasks users demand from their electronic devices.
To get the desired power intent, designers must strike a precise balance of power usage throughout the device. The design and verification engineer need to address whether the inserted power management circuitry functions correctly, as well as making sure the overall chip functionality is not corrupted by the power intent described in the UPF or CPF descriptions. Functional analysis, optimization and verification throughout the design flow, complicated by inadequate visibility of third-party IP white-box functionality, mandates the following five principal requirements for implementing and verifying a low-power scheme:
Traditional power-aware verification has been done with a patchwork of tools and approaches, which only provide limited analysis and verification capabilities and achieve inadequate quality of results (QoR).
A formal power-aware verification flow, in contrast, comprehensively meets power-aware verification requirements with the requisite QoR.
The front-end of the flow should automatically create power-aware transformations and generate a power-aware model that identifies power domains, the power supply network and switches, isolation rules and data retention rules. That requires parsing and extracting relevant data from the UPF/CPF specification, the RTL code and any user-defined assertions.
It then must automatically generate assertions to verify the interplay between design elements defined in the power description (e.g., isolation cells) and design elements defined in the RTL description (e.g., clock & control signals). It helps if the app is automated, outputting a report that summarizes which DUT elements satisfy or violate a particular property.
Additionally, the power-aware design database and assertions generated by the app can be used to verify the power reduction and management circuitry conforms to the UPF/CPF specification and does not corrupt the original RTL functionality. Other critical pieces include:
Formal verification offers the ability to accurately deliver the delicate balance of low power optimization that goes into creating a device that services all the functionality that consumers expect.
—Joe Hupcey III is director of product development at Jasper Design Automation.
Leave a Reply