Open side-bar Menu
 Decoding Formal
Dr. Jin Zhang
Dr. Jin Zhang
Jin Zhang has over 15 years of experience working in EDA, driving the effort of bringing new products and services to market. At Oski Technology, she is responsible for Oski’s overall marketing strategy as well as business development in Asia Pacific. Prior to that, she was the General Manager at … More »

“Shift Left” with Formal Technology

April 1st, 2015 by Dr. Jin Zhang

“Shift Left” has become a hot phrase after Aart’s keynote speech at DVCon2015 where he talked about how shifting left in schedule resulted from 10x productivity gain in design, IP, verification and software can spur on 100x opportunities in applications across all fields. He suggested many of these technological advances have the potential of changing what mankind is all about.

Static and formal techniques were mentioned as one of the mechanisms that increase productivity and contribute to shift left in the verification schedule. There are several reasons why formal technology is a key driver for the left shift.

The most important reason is formal verification can be done in parallel to RTL development. I like to think of this as getting routine health checkup for early disease detection. We all understand the benefits of detecting and treating illness early for better treatment opportunities, early recovery and potentially lower cost. Waiting until small ailments accumulate and show up in the late stages, could have serious impact. Formal testbenches, built along RTL development can help detect bugs closest to the sources, resulting in easier diagnosis and faster bug fixes and turnaround. The flexibility of adding a new checker and necessary constraints to exhaustively verify a new feature that is being developed is a remarkable advantage of formal verification. The benefits of formal, when deployed late in the design and verification cycle are greatly discounted. At Oski, we can’t advocate enough that our customers to think, plan ahead, and do formal as early as possible so as to save verification time, we can’t comprehend why companies rush to adopt emulation, before formal. Why wait to detect bugs late when you can detect them early?

The second reason formal shifts the verification schedule to the left, is in its ability to assist in achieving verification closure. Aart showed the familiar coverage closure curve in his talk, where the last 10% coverage closure always takes the longest time.

Formal can assist in coverage closure, in a couple of ways:

1. Formal can pinpoint coverage targets that are not reachable
2. Formal is exhaustive and can be used for sign-off on all the blocks that are suitable
3. If formal is used for sign-off on all suitable blocks, then during system level simulation, there is no need to include verification closure targets in those blocks, thereby reducing the amount of effort it takes to find and fire the right simulation vectors to cover those points.

The deployment of formal technology in the verification flow is the biggest factor of the left shift in verification schedule. We have seen more and more companies adopting formal as a key verification sign-off mechanism. The argument is simple: formal can help shortening the verification cycle by detecting and getting rid of bugs early, and reaching sign-off early.

Related posts:

Tags: , , , ,

Category: Blog

Leave a Reply

Your email address will not be published. Required fields are marked *



DownStream: Solutions for Post Processing PCB Designs
TrueCircuits: UltraPLL

Internet Business Systems © 2018 Internet Business Systems, Inc.
25 North 14th Steet, Suite 710, San Jose, CA 95112
+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