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 III
for Team Verify
On 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" session
Presented at DVCon 2011 on Wednesday March 2, 2011
Authors: Alan Carlin, Freescale Semicondutor, Inc.; Chris Komar, Cadence Design Systems, Inc.; Anuj Singhania, Freescale Semicondutor, Inc.