# Formal Verification

The purpose of formal verification is to determine whether or not a particular design satisfies a set of predetermined requirements, properties, or conditions. It is a sum of a number of different techniques that employ the use of static analysis and mathematical or algorithmic calculations in order to determine just how correct or incorrect a piece of ASIC block or SoC is.

Before the verification process begins, the ASIC or SoC design needs to first be converted into a format that is verifiable. If a design is verified it means that the design accomplishes the purpose for which it was created in the first place. In order to verify the correctness of a design, we need to analyze its static as well as dynamic aspects, or better understood as the structural and behavioral components.

There are a number of different approaches that can be taken when it comes to formal verification of a software or hardware. Here are some of the most commonly and frequently used types:

Model Checking

In this first approach, we use abstraction techniques in order to exhaustively search, explore, and review all possibilities in a mathematical model systematically. Model checking can understandably be performed on models that have a finite number of states or conditions, but it can also be performed on seemingly infinite sets of states if there is a way to represent them in finite terms using abstraction techniques. Some of the smart and domain specific abstraction techniques include the likes of abstract interpretation, symbolic summation, abstraction refinement, and state space enumeration. The properties of the system are usually represented as formulas in temporal logic. As such, we go through the graph of the transition system and ensure that every state satisfies the formula of the temporal logic of the model.

Equivalence Checking

Equivalence checking is very commonly and frequently used in order to test and explore RTL and gate level description of circuit designs. It is now also being used to verify FPGAs, and RTL description descriptions of a block.

SoC Level Verification

As of this point in time, formal verification techniques that are able to test and verify the entirety of a System on a Chip in a go do not exist yet, but it is possible to perform their exploration in combination with simulations and emulations, depending on the size of the design that is being tested.

Focused Formal Verification

Formal verification techniques are being used in focused campaigns for very specific purposes and its importance continues to grow everyday. These techniques are of particular importance in areas and fields were catching bugs and faults is extremely essential to the process. Clock Domain Crossing, or CDC, and X-propagation are good examples of focused formal verification techniques.