To complement the “Decoding Formal” Contests hosted live at DAC 2013 in Austin TX, Oski Technology launched a parallel online “Decoding Formal” Contest so engineers who were not attending DAC could also participate. The online competition concluded on June 21st with many participants from Europe, Asia and US. The 3 winners were chosen based on their answers on all the questions. Congratulations to Oski Online “Decoding Formal” Winners:
Amit Rustagi from Broadcom
Charu Aggarwal from Apple
Junhyuk Park from Samsung
There were 10 questions covering formal technology and its application. Most questions were multiple choice except for the last which was an essay question – “ Do you think formal technology is a must have technology in the verification flow? Why or why not?” Most participants answered yes, echoing what we have seen in our projects with our customers, that formal technology has become an integral component and in some cases one of the sign-off criteria in the verification flow.
There were many reasons for this. Answers submitted by contestants included the following –
“Yes. It complements simulation based DV flow. There are a lot of freebies you get just for running the design through a formal tool. Localized properties make debugging easier. Properties can be ported from unit level all the way to top level DV”
“Yes, because many functional bugs in designs with large state space may not be caught by simulation over large number of runs. Formal Verification needs to be run on such designs before sign-off of the design.”
“Formal Verification removes end to end bugs in a design which is not plausible using simulations. It can catch bugs in very early stages of the design. For the correct type of design it will save both time and resources and would give a better result as compared to simulations. So, a MUST-HAVE technology in the verification flow”
“Yes, I think formal verification is a must have technology in the verification flow. The prime reason is that formal proves to be really quick in hunting bugs on some specific designs, for example data transport designs, if applied with suitable abstraction methods”
“Formal verification is a must-have technology. Because we can verify design exhaustively with formal”
The competition results showed most participants have a good understanding of what formal technology is, its application and benefits.
In the question “Can formal verification replace simulation in a verification methodology”, all the contestants answered yes to different levels of application. While formal technology is commonly used to complement simulation methodology, on many blocks, it is possible to replace simulation completely with formal. Oski has done many such projects for our customers to build block-level formal testbench so no simulation needs to be run at that level.
Oski Decoding Formal” Online Competition Question: Can formal replace simulation in verification methodology?
In answer to a follow-up question “What kind of checkers are needed in order for formal to replace simulation for a block”, most participants understood that it takes interface assertions and end-to-end checkers for formal to replace simulation.
Oski “Decoding Formal” Online Competition Question: What kind of checkers are needed for formal to replace simulation for a block?
As formal technology has an inherent complexity barrier due to the large state space it needs to analyze, often the formal run doesn’t converge. In response to question “What should I do when formal verification times out”, participants correctly explained that all is not lost. Indeed many things can be done to achieve convergence, and the spread of the answers showed a nice mix of techniques such as adjusting constraints, writing abstraction models and ensuring bounded proof is good enough. It is particularly encouraging for us to see that the technique that Oski Technology has been using in all our projects – using Abstraction Models to overcome the complexity barrier – are becoming more widely accepted and regarded as an effective technique.
Oski Decoding Formal” Online Competition Question: What should I do when formal verification times out?
Oski Technology has been a instrumental in the formal space, fostering the growth of formal technology adoption and its application in design houses worldwide, and it is our goal to see that the engineering community discovers the significant benefits to be had with leveraging formal, and that formal continues to be adopted and understood by the engineering community, worldwide.
Once again we want to thank all contest participants and congratulate our winners on a job well done! Look forward to seeing some of you in San Francisco, June 2014!