InFormal Chat


DAC 2017 Review: Exotic Formal Applications

As I wrote in previous blog “DAC 2017 -Feels Like a Formal Candy Store”, I was expecting a lot of interesting presentations on Formal applications at DAC. Not only did I find some sweet Formal presentations but also some pretty exotic Formal applications. It is clear that there is a lot of usage of Formal tools out there and people are pushing Formal in unexpected directions such as verifying functions across firmware and hardware boundaries and inside analog circuits.

Eye ball halloween candy on orange background, 3d

Two additional applications which fall into the relatively known space for Formal verification that were discussed a lot at DAC were Formal Coverage and Architectural Formal. By applying Formal at the architecture level, you can find system level behaviors such as cache coherency protocol deadlock before any RTL is written. Formal coverage is of course a requirement for formal sign-off but other innovative uses include guiding bug hunting with Formal and finding missing connectivity checking properties.

Coming back to exotic applications, the first that I saw at DAC were two papers on HW and SW co-verification using Formal; “Formal Techniques for Effective Co-Verification of Hardware/Software Co-Designs” by Rajdeep Mukherjee – Univ. of Oxford, United Kingdom  and “End-to-End Formal Verification Method for Communication IP Including S/W” by Fumitaka Fukuzawa – Renesas System Design Co., Ltd., Tokyo, Japan. The design under test (DUT) is not only the RTL but also the FW control flow. The Formal testbench has two components, one to verify the HW communication protocol and second to verify SW control. The assertions for the HW communication can be written in standard SVA but how do you write an assertion of the form “FW function call |-> HW signal asserted” to verify the FW control flow? Another interesting consideration is to verify the HW after FW boot. What if you successfully verify HW security features in the RTL but these features are inadvertently disabled during FW boot. So many chips have embedded SW today that I think we’ll see more applications of Formal taking SW into account.

The second exotic Formal application is when the DUT is a mixed analog digital circuit. The paper “Formal Verification for Analog/Mixed Signal Designs“ was presented by Sudhakar Surendran – Texas Instruments India Pvt. Ltd. & Texas Instruments, Bangalore, India. Turns out that you can verify interface behaviors, prove SVA properties and do connectivity verification using standard Formal tools. You will need to create abstract models for analog components, model input to output dependencies of analog modules and verification using temporal random variables in Formal will still be much faster than in simulation. This allowed the user to find incorrect connections between analog and digital modules and find the wrong kind of buffers on analog signals which would result in open circuits. It is exotic today but with analog sensors embedded in many IoT devices, I think we’ll see more usage in this space as well.

These two exotic applications are good examples showing that the design verification community is starting to leverage Formal to address verification problems in the domains that we had not expected a few years back. This makes Formal verification even more exiting and I am sure we’ll see other exciting Formal applications in the coming years.

Share and Enjoy:
  • Digg
  • Facebook
  • Google Bookmarks
  • LinkedIn
  • Twitter