Limits of Current Verification Methodologies
As design complexity grows, verification must include understanding of design structure and intent. Verification results are only as good as the specification, regardless of simulator or formal engine speed. Debugging cycles will continue to increase unless adequate specifications are created; both the design and the verification teams need to become involved in the verification process to adequately reduce chip defect risk.
- Directed Simulation utilizes blackbox checkers to test I/O behavior for feature interactions, and is not scalable due to the number of complex interactions between features
- Constrained Random Simulation utilizes external 'blackbox' checkers to define expected behaviors of DUT, with the blackbox' checkers and the DUT typically developed independently. Features and interactions are often skipped by external checkers, for example: performance related features, exceptions, and interrupt conditions.
- Formal Verification uses mathematical analysis to prove or disprove properties for all legal input stimuli. Users must specify sufficient properties to cover all design feature.
Importance of Assertion-Based Verification
Assertion-based verification enhances directed and constrained random simulation, formal and emulation verification approaches by driving more effective and targeted verification. An Assertion-based Verification approach utilizes assertions and functional coverage properties, which are logic statements that define the intended behavior of signals in the design.
- While traditional blackbox checkers specify the input and output behaviors of the DUT, 'whitebox' assertions specify the behaviors of the internal logic and inject observability into the Register Transfer Level (RTL) code.
- Assertions ensure the correctness of the implementation logic, and the number of assertions needed to verify the design scales linearly with the complexity of the RTL.
- Whitebox functional coverage properties expose corner case behaviors created by implementation and ensure such behaviors are targeted by simulation test vectors.
- Features that cannot be captured using external checkers can be effectively done with whitebox assertions.
- Whitebox assertions pinpoint the problems in the RTL when they are triggered, reducing overall debugging time.
- Assertions can be reused across all verification platforms such as simulation, formal and emulation, and allow cross checking between different test environment. They also facilitate design reuse.
Assertion-Based Verification Hindrances
As design complexity increases, assertions and coverage properties are well-recognized as an important adjunct to the black-box checkers used in simulation and formal verification flows. However, adoption of assertion-based verification has been slow for the following reasons:
- It is infeasible to manually generate an adequate number of assertions to the level needed for thorough identification of design problems. It is generally desirable to have one assertion for every 10 to 100 lines of RTL code, yet it can take hours to create, debug and maintain each assertion. Additionally, high quality assertions require different and often orthogonal perspectives, which a single designer lacks.
- It is an unwieldy and time consuming process to manually create sufficient functional coverage properties to identifying which tests are missing. Coverage properties are a critical element to prevent defects, yet high quality coverage properties are as tedious and difficult to write as high quality assertions. Additionally, many useful functional coverage properties are non-intuitive as they address the behaviors that verification engineers did not think of initially.
- The high learning curve for standard assertions languages such as SystemVerilog Assertion (SVA) and Property Specification Language (PSL) is a high barrier to adoption.
Assertion Synthesis role in Assertion-based Verification
By automating the tedious and time-consuming process of generating assertions and coverage properties, Assertion Synthesis allows design and verification teams to finally reap the benefits of assertion-based verification in a timely and resource efficient manner.
