The recent Decoding Formal Club meeting hosted by Oski Technology on October 21, 2015 at the Computer History Museum in Mountain View celebrated the club’s 2nd anniversary with a “back to the future” twist.
While many of the predictions in the movie “Back to Future Part II” did not come true on October 21, 2015, the day of “the future” to which Marty McFly and Doc Brown time travel in a flying silver DeLorean sports car, that didn’t deter us from inviting attendees from Apple, ARM, Arteris, Broadcom, Ericsson, Google, Imagination, Microsoft, NVIDIA, Palo Alto Networks, Qualcomm and others to make some timely predictions for formal verification in 2025. The group was comprised of formal experts with years of experience, as well as engineers who are new to formal verification, so the predictions for 2025 were daring, but some are quite possible.
1. Formal will replace simulation
2. Verification will use 80% FV + 20% DV
3. The processors/tools will be powerful enough to check/prove any design in an unbound cycle.
4. Formal will replace simulation for unit testing
5. FV will be mature enough to support plug-and -play HW IP components.
6. No constraints written by a human will be needed
7. Formal will be the sign-off tool
8. Formal will scale to full subsystems of very large chips
9. We will be able to specify properties at higher levels of design/abstraction
We believe that in the next ten years formal will become the default verification strategy in the verification flow, routinely used to sign-off at the unit level. This is already possible today. The obstacle is not in formal technology or even lack of methodology. Instead, the barrier for broad adoption is that early adopters have experienced failure, and discovered how difficult it is to succeed without a solid strategy.
Will the technology advance enough wherein formal can be applied to any design without an unbounded cycle? This is an audacious prediction, but is surely possible. We may need quantum computing to assist, and true artificial intelligence in formal verification, to learn and reapply. This prediction appeals to us because it holds a bold “back to the future” vision, without which no advance in formal is possible.
We didn’t just focus on the future at our Decoding Formal event. We also focused on techniques readily available today that make the application of formal verification successful. Prashant Aggarwal, principal engineer from Oski Technology covered how to ensure the formal testbench is complete. Kenny Xing, principal design engineer, shared Broadcom’s success in verifying PCACHE using creative coloring techniques. Yogesh Mahajan, engineer from NVIDIA and Vigyan Singhal from Oski, talked about compositional gotchas. Both the Broadcom paper and NVIDIA presentation are available for download under the technical papers section on the Oski web site. Attendees gave very positive feedback about these presentations, rating them as engaging, appropriate and focused.
With so much planned for the event, we wrapped up the day, slightly past our scheduled ending time – but aptly, just before 4:30 pm., with one highlight and popular prize drawing worth a mention. Not a replica of the silver DeLorean sports car in the movie, of course, but instead a beautiful midnight silver metallic diecast model of the Tesla Model S P85, shown below. Just like Tesla, who is pioneering and revolutionizing electric cars and helping our world to become a cleaner place, Oski is revolutionizing the way we approach the verification flow, and helping companies find bugs earlier on in the process. We are looking forward to the next Decoding Formal Club meeting in Q1, 2016 and keeping our sights on 2025, when we are optimistic that many of these predictions will have come true.