The benefits of formal verification are becoming more significant when designing modern complex ICs, enabling you to verify designs earlier and more reliably, helping you achieve the desired “shift left”.
The type of services that benefit from this technique include:
- Development of formal verification strategies,integration and optimisation of existing verification flows
- Provision of reusable formal verification components
- Assistance with verification of new IP components and achieving fast coverage closure.
- Screening existing IP portfolios by undertaking exhaustive checks or troubleshooting HW bugs that are difficult to replicate in simulation
- Performing automated exhaustive checks at sub-system and SoC level e.g. CDC checking, UPF checks, connectivity checks, register map checks
- Clock domain crossing checks
- Automated register map checks
Formal verification is an umbrella term for techniques that use static analysis based on mathematical transformations to determine if hardware or software will behave correctly. This is in contrast to dynamic verification techniques such as simulation that sequentially apply stimuli to a design under test (DUT) and to check the corresponding responses.
Static analysis achieved using formal methods has some advantages. The creation of a traditional testbench to generate and check stimuli is not required. This enables verification of new designs described in HDLs like verilog to begin much earlier whilst the code is evolving, avoiding bugs at source. Complex designs can, in practical terms, simply take too long for the simulator to fully exercise. In this case formal verification can help hunt down bugs not easily debugged with simulation and much faster.
Formal methods are mathematical techniques for specifying, developing and verifying systems. A mathematical model suitable for applying formal methods can be extracted from modern hardware description languages and this formal specification can be used as the basis for checking the properties of a design to ensure its correct behavior. Formal verification techniques have been known for some time and are now an essential complementary strategy to traditional simulation approaches for accelerating and achieving design closure.
Simulation run times for SoCs and complex sub-systems can be extremely long. Iterating many simulations in order to debug and verify designs is very time consuming. Formal verification can be used to avoid bugs as RTL code evolves, statically checking correct behaviour of FSMs, fifos, bus interfaces and other functions, minimising the presence of bugs before simulation starts.
The state space of a complex IP, e.g. a device supporting full cache coherency, can be so vast that it is impossible to check every possible state using simulation. Formal verification engineers can exhaustively verify such complex functions in a fraction of the time, hunting down bugs by taking advantage of mathematical proof and abstraction techniques. An example of where this can be particularly useful is where there are difficult interactions between state machines that can result in deadlock and livelock conditions.
Other applications of formal include identifying RTL dead code which cannot be covered by simulation, automatic connectivity checks, automatic checking of register and bit maps, identifying sources of x or undefined signal values, checking completeness and consistency of power control networks described in UPF and ensuring designs are free from metastability issues caused by clock domain crossing.
Many of the formal verification techniques can be applied to IP blocks and subsystems in your portfolio before they are required to be integrated into a SoC. Minimising the number of bugs present in IP components when a SoC is integrated, reducing the need for long simulation debug cycles, or identifying deadcode before attempting code coverage closure, can dramatically reduce the verification effort for your designs.