Use Formal Verification Methods to 'Shift Left' with your IC Design.

Verification Dec 18, 2015 12:13:00 PM

Dec 18, 2015 12:13:00 PM


The benefits of formal methods 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”.
ic design services Verification capabilities

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 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.



Verification of modern digital IC’s is challenging, often on the critical path for a project and consuming many costly resources. By implementing Formal Verification Methods  as part of a 'shift left' strategy, this can help hunt down bugs not easily debugged with simulation and much faster.

 You can download a datasheet about Formal Verification

Click Here to Download Datasheet


The Sondrel engineering team work with customers across various market sectors to provide tailored design service solutions focussed on Power Performance and Area target specifications. If you would like to discuss your  project requirements, why not request a call? 

Request a Call




Comments ()

Add comment

Related / News


Mentor's U2U event in Munich was well attended this year - over 300 attendees from 20 different countries. The words on everyone's lips? - AI and Machine Learning. Especially.


This blog looks at a twelve month verification engagement with a client that is already a world leader in machine vision technology. This design will be used in multiple.


In this post we look at the use of the latest power aware verification methodologies to “shift left” - to verify power architectures early and minimise bugs occurring in the.


Functional Verification can enable your verification environment to “shift left”, starting verification early in the design cycle by streamlining testbench development,.

Subscribe to Email Updates