Verificación formal FPGA

What is the difference between Formal Verification Funcional Simulation?

Formal Verification is a different style of verification but achieves the same end goal: clear out bugs from the design. One of the big differences between Formal and Functional Verification is the role that the tool plays. Formal verification uses static analysis based on mathematical transformations to determine the correctness of hardware or software behavior in contrast to dynamic verification techniques such as simulation.

In Simulation, test cases (scenarios) are created manually or by an automated testbench and then executed on the RTL or gate-level design. Given the huge number of states in even a small design, it is impossible to simulate more than a small percentage of the design's behavior. Simulation is probabilistic; the chances of exercising any scenario that reveals a design bug are small. Formal verification does not execute the design, so it does not require testing or testbeds. Instead, it statically analyzes the design for all possible input sequences and all possible state values, checking to see if any assertions can be violated. From a theoretical point of view, formal verification is one hundred percent exhaustive, proving that all assertions are "safe" once all bugs have been found and fixed.