Formal methods for power-aware verification
Lawrence Loh, Jasper Design Automation
EETimes (12/17/2012 10:42 AM EST)
The imperative for reducing power consumption now pervades application spaces ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Consequently, power reduction and management methods are now used extensively throughout the chip design flow from architectural design, through RTL implementation to physical design.
The design team must verify not only that the inserted power management circuitry functions correctly, but also that it does not corrupt the chip’s functionality. Ideally, the team would have power estimates early enough in the design flow to deploy and verify the appropriate reduction techniques, minimizing or even completely avoiding late-stage redesign. Generally, though, really accurate power estimates become available only at physical layout, where design changes — even small ones — ripple back through design flow. Consequently, power-aware design often requires iterative optimization up and down the flow. Moreover, because many optimizations are performed late in the design flow, verification effort and risk increase, and debug becomes even more tedious and time-consuming. Consequently, power-aware design can appreciably increase design and verification time and cost. The challenge is to achieve the target power consumption while limiting the cost of doing so.
Our ultimate objective is to verify not only the chip’s functionality, but also that we have completely and correctly implemented the power intent described in Unified Power Format (UPF) [1] or Common Power Format (CPF) [2] descriptions. This article concludes that an “apps” approach is the best way to apply formal methods to power-aware verification.
We first address the challenges in devising and verifying the power management scheme and power optimizations necessary to achieve this ultimate objective. Firstly, how is the power management scheme devised?
To read the full article, click here
Related Semiconductor IP
- JESD204E Controller IP
- eUSB2V2.0 Controller + PHY IP
- I/O Library with LVDS in SkyWater 90nm
- 50G PON LDPC Encoder/Decoder
- UALink Controller
Related Articles
- Formal property verification: A tale of two methods
- Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation
- IC design: A short primer on the formal methods-based verification
- Formal Methods to Verify the Power Manager for an Embedded Multiprocessor Cluster
Latest Articles
- Crypto-RV: High-Efficiency FPGA-Based RISC-V Cryptographic Co-Processor for IoT Security
- In-Pipeline Integration of Digital In-Memory-Computing into RISC-V Vector Architecture to Accelerate Deep Learning
- QMC: Efficient SLM Edge Inference via Outlier-Aware Quantization and Emergent Memories Co-Design
- ChipBench: A Next-Step Benchmark for Evaluating LLM Performance in AI-Aided Chip Design
- COVERT: Trojan Detection in COTS Hardware via Statistical Activation of Microarchitectural Events