Products

 

Today’s SoC projects are continually expanding in size and functionality and the complexity of the register map that needs to be verified has also increased significantly. Directed tests with marching patterns or pseudo-random tests are not sophisticated enough to fully verify that registers are always operating correctly and that they cannot be unexpectedly affected by other logic in the SoC.

The JasperGold® CSR Verification App formally verifies control and status registers for IP integration, as part of the design specification, and so forth. Leveraging Jasper’s formal technologies allows checks to be done at the block level, the unit level, or even the chip level.

The goal of CSR verification is to exhaustively verify that the RTL matches the CSR definition and the value read from the registers is always correct. Conceptually, the following non-deterministic trace is considered by formal for proving address A.

 

Jasper’s formal proofs are exhaustive and check for all possible sequences of RD/WRs in any order and check for all register addresses.

Typically, the registers are spread out across the entire SoC, and tests are created to verify the register operation in simulation is tedious and error-prone.  However, it is extremely difficult and nearly impossible to test all of the subtle interactions of the register operation and other logic in the SoC. A single register (a single address) might have numerous fields, and those fields can have different attributes like widths, reset values and access types such as:

 

R: readonly

RW: read write

RS: read and set to 1

RC: read and clear to 0

RR: read and reset to reset value

RO: read always see value ones

RZ: read always see value zeros

Etc.

 

Within the JasperGold CSR Verification App, the register checks are automatically generated from the CSR definition table, and the formal engines can exhaustively verify that the registers operate correctly under all circumstances.

Depending on the complexity of the design and the number of registers to be tested, 1000s of properties can be generated. Productivity and throughput are enabled by allowing multiple proofs to be kicked off in parallel with ProofGrid™ while proof jobs can be managed and tracked using ProofGrid Manager™. ProofGrid and ProofGrid Manager boost the overall performance of formal verification, leveraging the power of local machine, cluster and computer farms, while providing seamless and powerful distribution and collaboration management of the proof engines running on the network, under a unified tracking console.

Jasper’s powerful Visualize™ technology displays “live” interesting waveforms and significantly speeds up debug. If a counter-example is found, constraints can be added or modified on-the-fly using Visualize to test out “what-if” scenarios before modifying the RTL. The QuietTrace™ feature simplifies the debug process even further. It is a unique Visualize debugging capability that finds interesting behaviors with fewer signal events. Simplification of traces with minimal signal activity accelerates exploration and debugging tasks.

The complexity and modularity of todays SoCs require new methods for verifying the register map and correct operation at all levels. Formal verification and Jasper’s CSR Verification App with powerful debug capabilities is the ideal solution to ensure correct operation.