System Architecture Sign-Off

Case Study: Architectural Formal Verification of System-Level Deadlocks

Problem: Architecture Superbugs

Parallelism has created an increasing number of superbugs at the system architecture level. Traditionally, verification tasks for system architecture requirements, such as those related to deadlock and cache-coherence, have been undertaken through full-chip RTL simulation or emulation. These methods occur late in the design cycle after all design modules are coded and integrated to construct the entire chip.

The coverage achieved for complex SoCs at this level is predictably low, which leaves the possibility of architectural bugs surviving the verification process.

Example: System-level Deadlock Bugs

System-level deadlock superbugs can occur when there are circular dependencies in the design.

For example, if Block-A is waiting for Block-B, but Block-B cannot make progress until Block-C responds and Block-C is in turn waiting for Block-A.

Oski System Architecture Formal Sign-Off is Exhaustive

Oski’s advanced formal verification methodology eliminates system architecture superbugs for targeted areas such as deadlock and cache-coherence.

We leverage the exhaustive analysis capability of formal sign-off to uncover corner-case bugs, while utilizing highly abstract architectural models to overcome complexity barriers and enable deep analysis of system-level design behaviors. The combination enables effective system-level requirements verification that are not well covered by traditional verification methods.

Early Formal Sign-Off Avoids Late-Stage Bug Fixes

Oski’s formal sign off methodology does not rely upon RTL model availability, so 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.

Oski’s System Architecture Formal Sign-Off Methodology

Step 1: Architectural Modeling

An Architectural Model (AM) is created for each block that contributes to the system-level requirement being verified. The block AMs include only a small slice of the block functionality.

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

Cache-coherence verification architectural models

Step 2: System-level Requirements Verification

The system-level architectural model is constructed from a collection of block level architectural models. The formal sign-off methodology, routinely employed for block-level verification, is then used to prove that the system level requirements hold for this architectural model.

Step 3: RTL Implementation Verification

The 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 architectural models.

This step is essentially an equivalency check between the architectural models and the RTL model — one block at a time. It closes the loop on the system architecture formal sign-off process, ensuring that the implementation has not introduced any bugs that would cause the design to fail to meet the architectural requirements.