Easing The Burden Of Early Bug Detection

Integrated circuit designers are under constant pressure to deliver bug free code that meets ever more rigorous requirements. It is well known that the more bugs that can be detected early in the development process, the faster and easier that development effort will be. However, early bug detection requires a verification overhead on the designer that can be onerous and impact the design process.

The two major methods that designers can leverage to detect bugs are static linting and simulation. Linting requires low set up and can detect a class of bugs based on the syntax of the code, although does tend to report many potential issues that have to be analyzed and is limited when examining the sequential operation of a block. Simulation is focused on the code operation but requires a greater degree of set up, in the form of directed stimulus creation, which are usually not available at this stage in the process and will only detect issues in scenarios that the provided stimulus is examining.

What designers require for early and automated detection of implementation issues are fast and easy ways to set up static checks for the sequential operation of the code in an exhaustive fashion, without relying on user provided stimulus. Automated formal code inspection helps to rapidly eliminate errors in a piece of RTL, prior to functional verification and synthesis, while providing a fully automated, and simple use-model. Three different verification perspectives are achieved.

• Structural Analysis: Focused syntactic and semantic analysis of source code.
• Safety Checks: Exhaustively verify the absence of common sequential design operation issues and failure debugging.
• Activation Checks: Ensures that specific design functions can be executed and are not blocked by unreachability.

Each of these pieces of technology are fully automatic and require no assertions to be created by the user. There is no need to write stimulus, create assertions or understand the formal mechanisms being employed.

Let’s examine how a large wireless communications company applied this technology along with an advanced coverage closure solution on their PP32 network processor. The application entailed a 5-deep instruction pipeline, interrupt handling, and an on-CPU task mechanism.

To fully understand the impact of the automated formal technology, we need to know the challenges that this design team faced. The group of engineers were dealing with very complex IP verification. As a result, simulation was taking too long with multiple regression runs. The extent of verification coverage was unknown and therefore full functional coverage could not be achieved and zero integration bugs were found in the SoCs.

Using roughly one assertion for each instruction opcode, the company was able to verify the functional correctness of their network processor. When applying the formal verification technology to the design, the following steps were taken:

• “Virtual registers” were used to handle the forwarding mechanism
• Pipeline details were hidden helping to dramatically increase assertion readability
• The assertions obtained constituted a concise instruction set specification

The specific results achieved after implementation include:

• Formal closure on all checks
• All assertions were verified in approximately 1 hour
• Full coverage was accomplished
• 40 bugs were detected including:
  • 29 “hard-to-find”
  • 10 corner-case
  • 17 specification
  • 2 performance
  • 11 other
• No bugs were encountered in the field after the IP was integrated into 3 SoCs
• There was a 40% reduction in effort compared to simulation-based verification

As you can see the results of this technology speak for themselves, but had the company not employed this specific formal solution extensive testbench writing would have had to be done along with countless simulation cycles. The verification of the vast number of scenarios would have taken an enormous amount of time while still not achieving complete verification. All of this would have resulted in poor confidence that there would be zero bug escapes, and, in the end, the IP would have been harder to re-use.

If you’re interested in learning more about the OneSpin Inspect technology and understanding how others have used it, check out our success stories.