With the increasing chip complexity checking the design correctness has become a more challenging task.
In fact time spent in verification exceeds the time spent in design phase even for FPGA designers, according to the 2020 Wilson Research Group study. This means the simulation is not enough to test design correctness and more powerful techniques are required to find corner case bugs faster. Here comes into the stage Formal Verification.
But what does formal mean anyway?
In order to understand what formal does, let’s have a look first at how the simulation process works.
In RTL simulation engineers create testbenches that stimulate the DUT. Testbenches use typically constrained random or directed tests to generate vectors that may or may not reveal bugs.
The downside of simulation is that it takes time and cannot cover the entire state space. Some test vectors may test the expected functionality and others may discover bugs. However, in order to explore the entire state space a large number of tests is required otherwise some bugs might be missed. But that takes way too much time and it is unrealistic goal through simulation.
With that being said let’s return to describe the concept of Formal verification, that is a mathematical and algorithmic solution designed to explore the entire state space. Unlike simulation that tests the design functionality, formal proves that implementation meets requirements. With Formal no testbench is needed, instead the verification engineers can use constraints and assumptions to restrict the analysis scope.
State space expands geometrically, cycle by cycle, starting from an initial state and examines all possible states, making Formal an exhaustive solution. If illegal states are reachable, a bug is found. Otherwise we’ve got a proof of the intended functionality.
Simulation and formal verification should be used complementary to ensure design correctness and reduce time spent in the verification process.
You may learn more about the universe of Formal solutions provided by Siemens EDA by accessing Verification Academy