Formal verification deployment can reveal a return on your investment in the design, say guest columnists Jim Kasak, Ross Weber and Holly Stump
Formal verification can be a valuable addition to an existing IC verification flow, and help reduce the risks associated with increasing design complexity. HP engineers recently undertook such a project as part of the company’s ProCurve ProVision Asic development effort.
We applied formal verification to several challenging blocks, including an arbiter, transaction conversion block, credit management system, transaction funnel, and cyclical redundancy check (CRC) system.
We used JasperGold, a property checking tool from Jasper Design Automation. As part of the verification effort, formal verification helped verify critical functionality and showed high ROI for such tasks as packet integrity analysis and flow control. Jasper also suggested methodologies for proof convergence as the tool itself contains a number of proof enabling features, reducing the need for manual efforts.
Starting with little experience in formal verification, the team found real bugs, including some that probably would not have been found with simulation. We found that formal verification can improve RTL quality, reduce lengthy random simulation efforts, and execute proofs of high-level end-to-end behaviour.
Formal deployment overview
We ran formal proofs on a next-generation design; this Asic has built-in wire speed intelligence, offers an engineering balance between feature capabilities, performance and price, and is scalable across a number of products. It contains a mix of 10G and 1G ports and approaches 1 billion transistors in size.
One goal was to prove properties on blocks that were difficult to simulate, while another was to discover bugs missed by simulation. We also wanted to learn how to enable proof convergence by reducing large state spaces and reducing sequential depth.
The effort was aimed at blocks comprised of new RTL code, blocks with limited controllability in simulation, and blocks exhibiting a high simulation bug rate. The testcases were:
• Testcase 1 – Arbiter with 13 requestors competing for 2 equivalent resources
• Testcase 2 – Transaction Conversion Block with an arbiter (Testcase 1), FIFOs, and control logic
• Testcase 3 – Multi-chip Credit Management System
• Testcase 4 – Transaction funnel merging 3 transaction streams onto a single interface
• Testcase 5 – CRC block with CRC generator, noisy channel, and CRC checker
Sample Testcase – Transaction Funnel
We enjoyed success using formal on all five of our testcases. The one detailed here exemplifies the results we were able to achieve, even as somewhat novice users, with JasperGold.
Formal was extremely valuable during the design of a transaction funnel with 3 transaction streams converging into a single interface (Figure 1). With such a block, it’s important that protocols are handled correctly, so data doesn’t get re-ordered, corrupted or lost. But the transaction funnel would have been extremely difficult to thoroughly verify with simulation because of low controllability -- it’s hard for a pseudo-random simulation to set up all possible transactions.
Figure 1 – The transaction funnel merges three transaction streams converging into a single stream.
The properties that were verified stated that transaction is never driven into the funnel when the funnel is not ready. The challenges were the huge state space, due to more than 12,000 flip-flops in the property’s cone of influence (COI) as well as the huge sequential depth due to many wide counters.
The result: A proof was achieved after around 40 minutes of run time, with a proof depth of 73 clock cycles. The ROI impact was high. Formal technology avoided a sizeable random simulation effort that would have had very low controllability and would have concluded with a limited amount of confidence that a catastrophic failure would not happen. Moreover, the formal verification effort involved creating 27 assumptions coded in System Verilog Assertion (SVA) that were added to the RTL simulation.
This block was in the critical path for the chip, and it was formally verified with about two weeks of engineering effort. A comparable simulation-based effort might have taken three months for a junior engineer or six weeks for a senior engineer. The use of formal technology with the funnel driver may have shaved a week off of the whole SoC development program, avoiding any lost revenues that a week’s delay in time to market would have cost.
Results and lessons learned
Results from the formal technology deployment were impressive. First, the design team found real DUT issues. We executed proofs of high-level, end-to-end behaviour, verifying that:
• Transactions are correctly translated through a block
• A shared resource is never over-committed
• Single/multi-bit corruptions are detected with CRC generator/checker
The team also successfully learned and used proof convergence enablers such as proof accelerators, initial value abstraction, state space tunneling, parallel proof engines, and the ability to dump a list of flip-flops in a property’s fan in-cone. These enablers made it possible to safely abstract and thus simplify the cone of influence.
One key lesson learned is that verification engineers need to have a clear agreement with their management on objectives for formal verification. Engineers can apply formal technology in several ways – to find known bugs in a buggy design, to hunt bugs in a presumably “bug free” design, and to achieve a complete proof of a property. It’s thus important to sit down with your management and agree upon what you’re trying to do and how long it will take.
In addition, there’s a myth that you do not need a formal testbench to run formal verification. This may be true for very small designs, but a sizeable block that requires clean transactions will need a testbench to drive legal transactions. In practice, a formal testbench is not as complicated as a fully fledged simulation testbench. Plan to implement a formal testbench for this purpose.
Another lesson learned was a counter-example debug shortcut. Instead of the standard, rigorous approach of back-tracing a failure by starting at the outputs, try checking the primary input stimulus that the proof engine devised first to ascertain if an illegal input stimulus had been applied. Then sharpen your assumptions or modeling logic to avoid illegal input stimulus.
Authors are Jim Kasak, senior Asic verification engineer, HP ProCurve; Ross Weber, senior field applications engineer, Jasper Design Automation and Holly Stump, v-p marketing, Jasper Design Automation
The complete article with additional test cases can be found here