The task of architectural requirements verification has traditionally been undertaken through full-chip RTL simulation or emulation. With these methods, verification of system-level requirements, such as those related to deadlock, cache-coherence, safety and security, occurs late in the design cycle, once all the design modules are coded and integrated to construct the entire chip. Due to the complexity of modern SoC designs, the coverage achieved at this level is predictably low and it leaves the possibility of architectural superbugs surviving the verification process.
Architectural formal verification is an approach which leverages the exhaustive analysis capability of formal to uncover corner-case bugs, while using highly abstract architectural models to overcome complexity barriers and enable deep analysis of system-level design behaviors. This enables effective system-level requirements verification that is especially useful to target areas that are not well covered by traditional verification methods, such as deadlock and cache-coherence.
Since the methodology does not rely upon the availability of RTL models, one additional benefit is that it can be deployed very early in the design phase. This allows architectural bugs to be detected and fixed before they are propagated throughout the implemented design. In contrast, finding late-stage architectural bugs through full-chip simulation or emulation may require many RTL design changes, since fixing these types of bugs often has a ripple effect that spans out to many blocks. It is vastly preferable to avoid that type of code churn, which can result in a significant set-back in verification maturity and lead to project delays.
- Quality: eliminate architectural superbugs through deep formal analysis of architectural designs
- Efficiency: early architectural requirements verification saves the high cost of late-stage bug fixes
Three Steps of Architectural Formal Verification
Step 1: Architectural Modeling
In the first step, an Architectural Model (AM) is created for each block that contributes to the system-level requirement that is being verified. The block AMs include only a small slice of the functionality of the blocks. This slice of behavior models the contract for an individual system-level requirement. A collection of block AMs forms a set of abstract models for which all other block-level design details are excluded (Fig. 1).
Figure 1: Architectural models for cache-coherence verification
Step 2: System-level Requirements Verification
In the second step, the system-level architectural model is constructed from a collection of block level AMs. Then the formal sign-off methodology, which is routinely employed for block level verification, is used to prove that the system level requirements hold for this architectural model.
Step 3: RTL Implementation Verification
The third and final step in the architectural formal verification flow is to check that the RTL implementation of the blocks will guarantee the system-level contract that was assumed for the AMs. Essentially, this step is an equivalency check between the AMs and the RTL model, one block at a time. It serves the purpose of closing the loop on the architectural verification process to ensure that the implementation has not introduced bugs that would cause the design to fail to meet the architectural requirements.