Design Article
Overcoming the challenges of formal verification and debug
Vennsa Technologies Inc.
5/18/2011 9:08 AM EDT
.
The flow starts as usual with developing a set of properties that must be proved using the formal verification tool. Properties that are disproved will include a corresponding counter example waveform that shows how the failure can be achieved. Irrespective of the specific tool, the counter example can be dumped using a format such as VCD, Verilog testbench, FSDB, etc. In the typical flow, this counter example must be debugged by an engineer, which leads to the time drain explained previously. In the proposed methodology, the counter example can be directly fed into the automated debugger for analysis. For instance, OnPoint will take in the design, properties, counter example and reset sequence to automatically generate three sets solutions based on where the bug may be: (1) problem with the constraints, (2) bug in the design, (3) bug in the asserting property. Since the bug is maybe in any one of these three areas, the engineer can systematically view them and rule them out.
For instance, a verification engineer or a formal expert who is tasked with debugging the failure may want to look at the assertion bug or constrain problems first. In this case, he/she can navigate each suspect (possible bug source) and quickly determine the root cause. Designers, on the other hand, may want to rule out any design suspects first. To look more deeply, each group contains a list of prioritized root causes accompanied with waveforms depicting the values and times where the fix should be applied. Next the engineer will focus fixing the suspect location to alleviate the problem.
Typically, a design or block will have multiple assertions that may fail. In my experience, when there are multiple failures, it is likely that many of the assertion failures are due to the same root cause. In this case it may be a design bug or a problem with the constraints. In such cases, I have found it that is best to first combine the failures to quickly identify the single error source that can be the cause of both. This allows for a quick fix that may rectify multiple failing properties. The automated debugger allows for such analysis by combining the reports of multiple failures.
Finally, since problems with constraints stemming from missing or incomplete assumptions can cause over 50 percent of failures, the proposed flow starts by first targeting the input suspects. These are inputs to the blocks where certain behaviors are not allowed. The automated debugger will generate a sequence of values for these inputs to aid the engineer develop the rightful assumptions.
The proposed methodology was developed over many months as my group worked on the deployment of formal verification. My colleagues and I had to go through a steep learning curve and analyze the problem intensively until the proposed methodology was devised. During our analysis, we performed head-to-head comparison with a “traditional” simulation flow and observed a 42 percent reduction in verification time on average. For instance, the verification of a subset of a DDR2 controller block was reduced from 36 hours to 21 hours. We plan to deploy this methodology for formal verification across many more groups.
About the author:
Aki Matsuda is a senior engineer at Panasonic and a researcher in System LSI Research Center at the Kyushu University, where he is currently working towards completing his Ph.D. degree. His research interests lie in improving the efficiency of VLSI design, verification and debug through automation and effective methodologies.
Read also:
Debug will get your attention, sooner or later
The flow starts as usual with developing a set of properties that must be proved using the formal verification tool. Properties that are disproved will include a corresponding counter example waveform that shows how the failure can be achieved. Irrespective of the specific tool, the counter example can be dumped using a format such as VCD, Verilog testbench, FSDB, etc. In the typical flow, this counter example must be debugged by an engineer, which leads to the time drain explained previously. In the proposed methodology, the counter example can be directly fed into the automated debugger for analysis. For instance, OnPoint will take in the design, properties, counter example and reset sequence to automatically generate three sets solutions based on where the bug may be: (1) problem with the constraints, (2) bug in the design, (3) bug in the asserting property. Since the bug is maybe in any one of these three areas, the engineer can systematically view them and rule them out.
For instance, a verification engineer or a formal expert who is tasked with debugging the failure may want to look at the assertion bug or constrain problems first. In this case, he/she can navigate each suspect (possible bug source) and quickly determine the root cause. Designers, on the other hand, may want to rule out any design suspects first. To look more deeply, each group contains a list of prioritized root causes accompanied with waveforms depicting the values and times where the fix should be applied. Next the engineer will focus fixing the suspect location to alleviate the problem.
Typically, a design or block will have multiple assertions that may fail. In my experience, when there are multiple failures, it is likely that many of the assertion failures are due to the same root cause. In this case it may be a design bug or a problem with the constraints. In such cases, I have found it that is best to first combine the failures to quickly identify the single error source that can be the cause of both. This allows for a quick fix that may rectify multiple failing properties. The automated debugger allows for such analysis by combining the reports of multiple failures.
Finally, since problems with constraints stemming from missing or incomplete assumptions can cause over 50 percent of failures, the proposed flow starts by first targeting the input suspects. These are inputs to the blocks where certain behaviors are not allowed. The automated debugger will generate a sequence of values for these inputs to aid the engineer develop the rightful assumptions.
The proposed methodology was developed over many months as my group worked on the deployment of formal verification. My colleagues and I had to go through a steep learning curve and analyze the problem intensively until the proposed methodology was devised. During our analysis, we performed head-to-head comparison with a “traditional” simulation flow and observed a 42 percent reduction in verification time on average. For instance, the verification of a subset of a DDR2 controller block was reduced from 36 hours to 21 hours. We plan to deploy this methodology for formal verification across many more groups.
About the author:
Aki Matsuda is a senior engineer at Panasonic and a researcher in System LSI Research Center at the Kyushu University, where he is currently working towards completing his Ph.D. degree. His research interests lie in improving the efficiency of VLSI design, verification and debug through automation and effective methodologies.Read also:
Debug will get your attention, sooner or later
|
|
|
|
|
Navigate to related information
Luis Sanchez
5/18/2011 5:27 PM EDT
Great article! very interesting to read about your methodology to study and compare the new approach against the former. The reduction in test time from 36 to 21 hours is a great benefit. This is a field where it will always be necessary to improve and reduce times as time to market may be sometimes crucial.
Sign in to Reply
cdhmanning
5/18/2011 8:38 PM EDT
This looks like Test Driven Development (TDD) for VHDL. It makes sense to cross pollinate tools from software development into other areas too.
Sign in to Reply
Neo1
5/19/2011 12:42 AM EDT
Writing assertions is not a simple task if we really want them to acheive functional coverage. It takes a lot of effort and design insight which accoutns for a major chunk of enineering time for verification. This being the case the problem is this tool is addessing is at a later stage when we have robust assertions and a clean flow using the same, else we end up spending a huge part of our time just addressing the mistakes in ones property description. And we have not even accounted for cases which are prone to race. The problem with deplying assertions widely is that it requires good design and tool knowledge to write one effectively and when that happens you need an even more undertstandable person to debug any failures. So, hmm.. this tool is trying to bidge this gap I suppose, should be interesting.
Sign in to Reply