Formal 2025: It’s Back to the Future!

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 AppleARMArterisBroadcomEricssonGoogleImaginationMicrosoftNVIDIAPalo Alto NetworksQualcomm 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.

A Tesla diecast Model S drawing prize, presented at the 2nd anniversary of the Decoding Formal Club, held at the Computer History Museum, Oct. 21, 2015.

Vikas Chandra of ARM talks about mobile hardware security at the Decoding Formal Club meeting, Oct. 21, 2015 at the Computer History Museum.

Networking at the Decoding Formal Club meeting Oct. 21, 2015.

Vigyan Singhal cuts a cake to celebrate the 2nd anniversary of the Decoding Formal Club and Oski Technology’s 10th anniversary in business, Oct. 21, 2015.

Prashant Aggarwal delivers presentation on the Completeness of End-to-End Formal Testbench for formal sign-of at the Decoding Formal Club meeting Oct. 21, 2015.

Kenny Xing, principal design engineer at Broadcom delivers presentation on Creative Formal Techniques to Verify PCache at the Decoding Formal Club meeting Oct. 21, 2015.

Networking at the Decoding Formal Club meeting Oct. 21, 2015.