Formal verification is an algorithmic-based approach to logic verification that exhaustively proves a design's functional properties. Typically, there are two types of formal verification:
1. Equivalence Checking - This verifies the functional equivalence of two designs, which can be at the same or different abstraction levels (e.g., RTL-to-RTL, RTL-to-Gate, or Gate-to-Gate). It is used for design implementation verification.
2. Model Checking - This verifies that the implementation satisfies the properties of the design. It is used early in the design creation phase to detect functional bugs.
PrimeTime is a Static Timing Analyzer tool, and Formality is a Formal Verification Tool.
For related PrimeTime information, please also see the following Answer Records: