Formal-based methodology cuts digital design IP verification time

Article By : David Vincenzoni

Changing your methods of performing verification can reduce verification time by several weeks.

When we talk about the signoff of digital IP, we are referring to the full verification of a block. Every feature listed in a device’s datasheet requires verification. Furthermore, every register transfer language (RTL) statement, branche, and expression also needs verification. Only when the functional (features’ check) and RTL code coverage reaches 100%, the IP is signed-off. To get there, we can consider two different modes to reach the target: the universal verification methodology (UVM) approach (classical methodology) and the formal-based approach (new methodology). Here’s how the formal-based approach can significantly reduce verification time.

Classical methodology

For many years, we’ve used UVM-SV/UVMe methodologies for the verification of digital IPs. This approach is based on complex object/aspect-oriented languages for building constrained-random tests to verify digital blocks and discover bugs. With this method, we can check the features of our block and run hundreds of tests by simply randomizing the data generation, which helps us find the corner conditions and/or dead lock.

The developing of verification environment of a digital IP can be split in the following tasks:

  • UVM test bench developing (verification IPs, scoreboards, checkers)
  • UVM registers developing (verification of configuration and status registers)
  • UVM tests developing (verification of functional features)
  • Run of constrained-random tests (the UVM tests runs many times with randomized data)
  • Code & functional coverage extraction
  • Refinement of coverage by creating new tests and/or increasing the randomized runs

Sometimes SystemVerilog Assertions (SVAs) are added in the test bench to check specific conditions such as the relationship between handshake signals. Figure 1 summarizes these steps.

classical IP verification methodology testsFigure 1 The classical IP verification methodology requires adding tests until sufficient coverage is reached.

The step of code coverage is usually corroborated with the help of formal unreachability flow. The classical approach is “improved” by the formal unreachability flow that lets us discover dead/unreachable RTL code that cannot be covered through any simulation. In this way, such code is removed from the count of overall code coverage.

New methodology

The new methodology is based on formal verification flow. The digital IP is completely verified with this methodology and signed-off (formal sign-off). The flow is based on the use of formal apps and the developing of SVA code verifying all the functional features of the block. As for UVM based flow, also the formal flow can be split into several tasks:

  • RTL code cleaning with linting tool (RTL code check)
  • Bus protocol verification–e.g. advanced micro controller bus architecture (AMBA) bus–with assertion based verification IP (ABVIP)
  • Control and status register verification
  • Formal property verification (verification of functional features)
  • Clock domain crossing verification (both for clock and reset) for IP that has asynchronous clock domains
  • Code & functional coverage extraction
  • Refinement of coverage by proving new SVA Assertions

Figure 2 summarizes these tests.

formal-based verification methodologyFigure 2 The formal-based verification methodology is a more streamlined approach.

As soon as the RTL is ready, the first step is to analyze it with a formal linting tool. This can result in Verilog/VHDL code free from many errors such as:

  • Dead/unreachable code
    • Very often, a dead/unreachable code could hide a bug. This is highlighted by the formal tool showing that some statement is unreachable. The designer can discover that the reason of this unreachability is a bug in the code
  • Data overflow for arithmetic logic
  • Bus contentions
  • Finite state machine (FSM) dead lock and live lock
    • This represents a first verification of the FSM
  • Combinatorial loops
  • Design for testability (DFT) checks
    • Full control of clocks and reset during the scan mode

The bus protocols of the IP (e.g. AMBA bus) can be effectively proved with ABVIP. The concept is quite similar to a UVM verification IP with the main difference that the rules of protocol are exhaustively verified. The configuration and status registers of the block can easily be verified with formal app. It is possible to check any kind of access policy, not only the simple read/write or read only, but also write by hardware/read by software or write to clear and so on. This step of verification is exhaustive.

For linting, bus protocol and register check, the designer does not need to write any SVA statement. The formal apps automatically generate the Assertion to prove the RTL code. All the others feature of the IP can be verified by writing custom SVA code. The formal property verification tool will prove exhaustively the assertions. The formal methodology lets us verify the re-synchronization structures (e.g. handshakes) for the IPs that have multiple asynchronous clocks. Data stability and re-synchronization flip flops are checked throughout structural and formal analysis.

UVM flow, as with formal flow, it’s possible to extract the RTL code coverage, as well as functional coverage. When the coverage target is not reached, more SVA assertions are developed and proved.

UVM vs. formal

To gain a better understanding about comparison between UVM and formal based methodologies, we can model the RTL code as many states in a space.

The digital design has states and transactions that are not only the related to the FSM, but are also the overall combination of a digital protocol bus and/or counters. The states can be hundreds or thousands, and the scope of our verification is to cover all the space.

When we simulate the design with dynamic constrained-random tests, we are covering a subset of this state-space. Figure 3 shows an example; The yellow circles are the reachable state-space that shall be verified and covered. The green circles are the already covered state-space through UVM constrained-random tests. The blue circles are the unreachable state-space that represent dead code or unreachable code due to parameter configuration or not legal states.

UVM state-space coverageFigure 3 UVM state-space coverage.

The coverage of the state-space can be of course increased by developing new UVM tests and also running tests with more randomization.

The formal verification is exhaustive. Proving a SVA assertion means to verify all the state-space. It is equivalent to run thousands of UVM tests. Figure 4 shows an example. The SVA constraints (defined as assume property) reduce the state-space by removing the not legal transactions/states, e.g. in a bus protocol where not all the possible signal combinations are legal.

Formal verification state-space coverageFigure 4 Formal verification state-space coverage.

Table 1 compares UVM vs formal methodology task-by-task.

Table 1 UVM vs formal methodology task-by-task.

The formal flow can be used for every verification task, while UVM is not applicable for RTL code linting nor for clock domain crossing (CDC). Bus protocol and registers verification use the formal verification instead the UVM, which can several weeks of work. The functional features, when the formal is applicable, are verified through the formal flow.

Integrating the IP block in a system on chip (SoC), we apply both methodologies to produce a combined verification. Connectivity check for IO muxing and unreachability (dead code) is performed with formal flow, UVM dynamic tests are developed for the top level verification.

If we measure the effort in weeks/days needed for every verification task, and we compare the result between UVM flow and formal flow, we found where Figure 5 shows that we can save several weeks by using the formal flow instead of UVM for the sign-off of digital IPs.

UVM vs formal task effortsFigure 5 UVM vs formal task efforts: UVM has fewer tasks but overall, it takes longer.

The resources saved in this verification step can be deployed to the top-level verification, where the UVM methodology is still heavily applied (Figure 6).

Formal verification saves timeFigure 6 The formal methodology saves considerable time.

Using formal methodology, we can save several weeks on verification tasks. When the formal flow is applicable, the formal sign-off for digital IPs lets us find more bugs in less time than any constrained-random test. The UVM methodology is widely applied to verify the integration at SoC level.

David Vincenzoni is an R&D Design Manager at STMicroelectronics.