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.
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).
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:
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.
Performing formal property checking has the following advantages over the simulation approach
Even though formal verification has many advantages it does have certain disadvantages:
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.