|
Formal verification (FV) is a generic name for a variety of methods used to prove the correctness of systems or programs. Given a formal description of a system, and a formal specification of its desired behavior, FV methods can be used to mathematically prove that the system adheres to its specification.
As an example, FV can be used to prove that a cache control unit complies with the cache coherency rules defined by the architecture, or that a bus interface unit complies with the bus protocol.
|