How Long Does It Take to Formally Verify This Design?

This year at DAC, we asked attendees to participate in a guessing game – make an educated guess about how long it takes to formally verify a design based on the given design description and statistics.

How Long Does it Take to Formally Verify This Design?

Here is a recap of the information provided to participants:

Design Description
Reorder IP packets that can arrive out of order and dequeue them in order; when an exception occurs, the design flushes the IP packets for which exceptions has occurred. Support 36 different inputs that can send the data for one or more ports. Another interface provides dequeue requests for different ports. Design supports 48 different ports.

Design Interface
Packets arrive with valid signal; a request/grant mechanism for handling requests from 36 different sources; All 36 inputs are independent and can arrive concurrently; All 48 ports can be dequeued in parallel using another request/grant mechanism.

Design Micro-architecture Details
Supports enqueue and dequeue for IP packets for 362 different input and 48 different ports respectively; 48 different queues used to store IP packets for different ports; A round robin arbiter resolves contention between enqueue requests from different sources for the same port at the same cycle.

Design Statistics
• Lines of RTL: 10,830 • Inputs: 3,904 bits • Outputs: 9,137 bits • Flip Flops, 84,027 • Clock Domain: 1 • Data Latency: 6 cycles • Required Proof Bound: 28 cycles

Distribution of Answers
We saw a very interesting distribution of answers as shown in the photo we took of the final guessing board:
• 0-2 months: 48 votes
• 2-4 months: 51 votes
• 4-6 months: 29 votes
• 6-8 months: 7 votes
• 8-10 months: 5 votes
• >10 months: 2 votes

Voting in the 0-2 Months Category
Most people who voted in the category of “0-2 months” was based on the following thinking:
1. Trust in our methods: Since Oski is verifying this design, it probably will not take very long
2. Presentation: It is customary for companies to showcase the fastest and best results, therefore 0-2 months is chosen as it is the best result
3. User experience with other types of formal: Based on experience with equivalence checking (logical or sequential), this verification time should be similar
4. Management pressure: More than 2 months verifying a design and I would be fired

The outlier on the “over 10 months” spectrum was based on layout and backend experience.

Why Oski Invited Attendees to Play
The reason we proposed this game is because the concept of formal sign-off is new, most people don’t have a sense of what it takes to formally verify a design block completely without relying on simulation. They don’t realize that it takes a good deal of effort to build a formal testbench – writing constraints, End-to-End checkers, reference models and most importantly dealing with complexity. The formal sign-off methodology needs to deal with all 4 Cs as shown in the picture below:

Solution: How Oski Allocated Time to Verify This Design:
For this particular project, our time spent was as follows:

1. One week: to understand the design specification; No documentation was available; Review RTL with designer; Had QA sessions over email and phone
2. Four weeks: to build constraints to model the environment; Modeling system level cycle accurate constraints were the hardest
3. Six weeks: to create End-to-End checkers to completely verify the whole functionality of the design; Design had 738 outputs signals and hence writing End-to-End checkers along with interface checkers took long time
4. Six weeks: to write reference models for these End-to-End checkers; Writing different reference models for each of the End-to-End checkers was a challenge
5. One week: to come up with Abstraction models to overcome complexity; We identified the useful and applicable Abstraction models at the planning stage and all those Abstraction models able we solve the complexity; Saved time as we did not re-analyze the complexity
6. Two weeks: to iterate with the designer for blocking bug fixes

How Long Did Oski Take to Verify This Design?
All together it took a good 5-months to finish the formal test bench development and completely verify this design using formal property verification tool. While the time may seem long, it is worth knowing that it took a year to write this RTL, also the design has a lot of corner cases and concurrent operations that it would have taken much longer to verify using simulation without the confidence that all corner-case bugs are found.

Deploying formal in the verification flow will definitely shorten the overall project cycle because more bugs would have been found at the block level rather than at the subsystem or chip level, thereby reducing overall debugging time. However when we approach our customers on formal projects, we are realistic with the expectation that on an individual block level, saving time is not the reason for formal deployment, rather it should be improving design quality for those blocks that are weak spots for simulation. People should come to formal with the right expectation, Thinking a complex job will be finished in fewer than 2 months is unrealistic, and will definitely lead to disappointment.

We had a lot of fun with the guessing game – two winners were chosen each day to receive an Oski T-shirt. Thanks to all for playing this game, and congratulations to the winners!

Booth visitor takes a guess at how long it takes to formally verify a design.

Tags: #51DAC, DAC, Design Statistics, formal analysis, formal sign-off, formal test planning, formal verification, Oski Technology

Category: Blog

This entry was posted on Friday, June 13th, 2014 at 2:43 pm. 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.