At DVCon 2011, a paper presented by Freescale and Cadence described a truly novel application of formal technology for something completely different than assertion-based verification (ABV). Specifically, the authors used formal engines to optimize the selection of complex (read, "higher in area and power consumption") vs. simple (read, "lower power, lower area") power control flip-flops. In this short video, one of the authors -- Team Verify's Chris Komar of the Formal Product Expert team -- elaborates:
If the video fails to play, click here.
Beyond the savings in area and power this solution delivered, you have to take you hats off to the authors for stepping back and dreaming up this application. It's certainly gotten myself and Team Verify wondering what other non-traditional ways we can apply our formal and dual-formal and simulation technologies ...
Joe Hupcey IIIfor Team VerifyOn Twitter: http://twitter.com/teamverify, @teamverify
P.S. So you can quickly track it down once the DVCon 2011 proceedings are published, here is the paper's citation:
Title: "Optimizing Area and Power Using Formal Methods"Paper 7.2 in the "Low Power Verification" sessionPresented at DVCon 2011 on Wednesday March 2, 2011Authors: Alan Carlin, Freescale Semicondutor, Inc.; Chris Komar, Cadence Design Systems, Inc.; Anuj Singhania, Freescale Semicondutor, Inc.
Nice video and avery interesting usage of Formal. IF there could be discrete metrics shared wrt. how much saving Formal brought , just in terms of flops too then the story becomes even more promising.