21st Century Power SEQers
Power consumption has been an important consideration for IC designs for a while now. Mobile devices today are more powerful than they’ve ever been. I can stream movies, order food, get turn by turn directions and take incredible quality photos and videos using a single device in my pocket… So long as I can make it to the end of the day without the battery running flat. Nobody wants to be in the middle of an important email when the screen suddenly goes black and I’m pretty sure I’m not the only one who’s gone diving into a coffee shop seeking power outlets because of it! These days, we all live with a small amount of power anxiety and 6th sense for hunting down USB sockets and power sources. Combine this with the huge number of servers out there burning power and it’s no surprise that most modern designers are always looking to find that delicate balance of power and performance.
One of the most common techniques for reducing power consumption in designs is through clock gating. Clocking all those flops all the time is burning an unnecessary amount of power and inserting gates into the design helps to ensure that we are only clocking the right flops at the right time therefore reducing the overall power burn. The only problem is what happens if we get it wrong? A design that burns no power and doesn’t do anything isn’t much use to anyone, so it’s important to make sure that when optimizing designs for power the new design is functionally equivalent to the previous implementation.
The SEQ (pronounced “seek”) app in VC Formal is a perfect solution to verify sequential equivalence between two implementations of RTL design (For example: same RTL code with and without clock gating cells inserted). The application uses formal technology to prove with cycle accuracy that under the same set of input conditions, two designs will always produce the same output. A proof of equivalence is an exhaustive formal proof and gives total confidence that any changes that have been made in the design haven’t affected the functionality. From a user perspective, all that needs to be provided are the two implementations of the design and any additionally needed constraints. The tool automatically maps the ports of the designs and can even map uninitialized values so you don’t see any spurious failures. In terms of the technology working under the hood though, the SEQ app has some pretty nifty features. Internal helper property generation helps speed up the runtime of the tool, whereas native debug and root causing allows users to quickly locate the source of any failures that happen to crop up.
We all want the next generation most powerful chips and using VC Formal SEQ App can help make sure that your power savings aren’t compromising design’s functionality!
