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