Formal verification can be a powerful tool for low-power design optimization, according to a paper authored by Cadence and Freescale and presented at the recent DVCon conference. The paper showed how formal property checking can validate whether retention flip-flops are controllable, and identify those that might need to be replaced with clock-state independent (CSI) flops.
Titled "Optimizing Area and Power Using Formal Methods," the paper was co-authored and presented by Alan Carlin, microcontroller verification engineer at Freescale. The other co-authors were Anuj Singhania of Freescale and Chris Komar of Cadence. The paper describes a flow used at Freescale in connection with the Kinetis K40 microcontroller. This and other archived papers will be available at the DVCon web site April 18.
In his presentation, Carlin noted that when chips power down, the design state should normally be restored as quickly as possible at power-up, so the "design picks up right where it left off." State-retained power gated (SRPG) flip-flops provide an easy way to do that.
Click here to read more ...