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.
Debug will get your attention, sooner or later