“Shift Left” with Formal Technology

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

Tags: advanced formal training, formal sign-off, formal verification, Jin Zhang, Oski Technology

Category: Blog

This entry was posted on Wednesday, April 1st, 2015 at 6:22 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.