Open side-bar Menu
 Decoding Formal
Pippa Slayton
Pippa Slayton
Pippa Slayton is Marketing and Business Development Manager at Oski Technology. She has 8+ years experience in the high-tech industry and drives marketing campaigns, marketing strategy, product launches, social media, and community building and event program management for Oski’s formal … More »

Formal 2025: It’s Back to the Future!

 
November 13th, 2015 by Pippa Slayton

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 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.

Drawing Prize: Tesla diecast Model S
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_ARM_mobile-security
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.
Networking at the Decoding Formal Club meeting Oct. 21, 2015.
Vigyan Singhal cuts cake at the 2nd anniversary of 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.
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.
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.
Networking at the Decoding Formal Club meeting Oct. 21, 2015.

Tags: , , , ,

Category: Blog

Logged in as . Log out »




© 2024 Internet Business Systems, Inc.
670 Aberdeen Way, Milpitas, CA 95035
+1 (408) 882-6554 — Contact Us, or visit our other sites:
TechJobsCafe - Technical Jobs and Resumes EDACafe - Electronic Design Automation GISCafe - Geographical Information Services  MCADCafe - Mechanical Design and Engineering ShareCG - Share Computer Graphic (CG) Animation, 3D Art and 3D Models
  Privacy PolicyAdvertise