An Introduction to Formal Verification

As the complexity of the system grows there is a need to move on to a higher level of validation.
As the complexity of the system grows there is a need to move on to a higher level of validation.
Formal verification is an automated testing method that detects many common design errors and may reveal ambiguities in the design. Formal verification is the process of verifying the accuracy of a project using mathematical techniques. Official verification tools use various algorithms to validate the design and do not perform any time checks. These tools do not require a stimulus or a testbench, therefore, official verification is done early in the IC design cycle - that is, as soon as the RTL code is available. When a bug is identified, it can be easily fixed.

Official verification gained popularity after the discovery of a popular Pentium bug in Intel processor, which led to the recall of faulty processors and Intel had to deal with a loss of close to $ 500 million. Various other incidents, such as the Ariane 5 explosion and radiation exposure at the Panama Cancer Institute, could have been avoided with official confirmation. Many hardware applications are essential, where any failure can cause significant financial or physical damage.

The figure above shows how the delay in the making of a chip affects the cost. This shows that as many bugs as possible needs to be removed in the early stages and new design errors should not be introduced while refining the design.

What is Formal Verification?

Formal Validation refers to the process of establishing a functional equity of two designs usually represented as HDL models without functional equations and simulations.

To formally validate a design, it must first be converted into a simpler "verifiable'' format. The design is defined as a set of interactive systems; each has a limited number of configurations, called states. States and transitions between states forms FSM. The whole system is FSM, which can be obtained by combining the FSMs associated with each component. So the first step to verification involves getting a complete FSM description of the system. Given the current state (or current configuration), the next (or subsequent configuration) of the FSM can be written as a function of its current status and input function (transition function or transition relationship).

Why Formal Verification?

Formal verification methods detect bugs that cannot be detected by standard verification methods. Also, in the case of bugs that can be detected using conventional techniques, formal verification usually identifies itself with the most faster rate. Before a design is functionally verified by simulation and emulation, it is formally verified.

Some of the benefits of formal verification are as follows:

  • Identifies bugs early in the design cycle
  • Lack of time
  • You are trustworthy
  • Immediately
  • Perfect

As ASICs become larger and more complex, netlist simulation becomes a very time-consuming process, and it is not advisable to use netlist simulation for weeks with very little change in RTL to prove that the net list is correct. Formal verification is the answer to such a problem. Often late repairs, also called ECOs, need immediate verification without the use of long simulations. Formal Verification is your answer. Formal verification is also a double check on your synthesis tool, that it does a good job.

Advantages of Formal Verification:

Performing formal property checking has the following advantages over the simulation approach

  • Verification is mostly fully automatic except for initial set-up, property coding
  • Verification can be started as soon as RTL is ready. It need not wait for the readiness of complete RTL. It can start the analysis even with basic functionalities
    • Reset Analysis
    • Sanity checks etc.
In a way, formal inherently lends itself to agile process
  • Testbench effort is not as exhaustive as in simulation method. So, a lot of effort is saved
  • As testbench is not required, stimulus generation will be automatically managed by the FA tool with or without constraints around it
  • The prove will be extremely fast compared to dynamic simulations
  • Simulations usually takes more time to detect the corner cases, FSM deadlock conditions. Sometimes it need additional metrics (coverage data) to identify the corners. But FA tool can easily find and reach those cases in quick time (fraction of minutes)
  • Both black box and white box approach can be used
  • Probably, the most important aspect of formal is that verification is 100%. There is no concept of corner cases or missed scenarios etc. In other words, if the property and constraints are correct than if the property passes then the design has no bugs associated with the property in question. Contrast this with simulation method, the verification is always “best effort” based and despite any amount of verification, there is no guarantee that the design is bug free

Limitations of Formal Verification:

Even though formal verification has many advantages it does have certain disadvantages:

  • As the design size grows, the state-space increases exponentially. So, when compared to a design with 2048 flops, a design with 2049 flops will have an exponential increase in the state space. Hence as the design size increases, quickly we reach an upper limit where the machine cannot handle the size of the design or the time taken to explore the state space starts to reach a point of diminishing returns. This is called the problem of state-space explosion.
  • FA is not suitable for data paths functions except for simple functions. This is true especially for algorithmic blocks
  • FA is good for verifying a system but not for validating the system.
  • FA can only handle RTL logic. Any analog blocks will get black boxed or can be removed from the DUT during FA

Formal verification Techniques:

The following figure illustrates the various formal verification techniques:

What is the difference between Traditional method and Formal verification?

  • Traditional Method -Testing & Simulation:
  • Here all the possible cases cannot be covered.
  • There is a possibility of surviving subtle corner case bugs.
  • Formal verification:
  • This method is equivalent to simulation all cases in simulation.
  • According to the property of formal verification there will be no bugs.
  • Property checking and equivalence checking is done in Formal verification.

Top Level Architecture and High Level Flow:

Examples of EDA tools for formal verification:

  • JasperGold from Cadence
  • Formality from Synopsys
  • Co-formal from Cadence

Summary

Formal verification is an automatic checking methodology that catches many common design errors and can uncover ambiguities in the design. It is an exhaustive methodology that covers all input scenarios and also detects corner case bugs.

This form of verification saves the designers time and effort as potential bugs are caught even before the test environment is developed. It can be used on high-level, RTL, or GLS representations of the design. There is a wide variety of sophisticated formal tools available on the market, many of which provide a pushbutton way to find errors in your design.

Chiplogic Technologies

Maidenhead Concorde Park
Concorde Road
Building 3, 1st Floor
Maidenhead SL6 4BY
United Kingdom

Sign up to Our Newsletter


© 2020 Chiplogic Technologies.