1.5 Limitations of Formal Verification
Formal verification, although offering exhaustive checking on properties, by no means guarantees complete functional correctness of design. Many factors can betray the confidence offered by formal verification. These factors include, but are in no way limited to, the following:
- Errors in specification. An implementation verification requires two versions of a design. Therefore, a bug in the specifications voids the reference model, may escape implementation verification, and may trickle down to implementations. A typical type of specification error is missing specifications.
- Incomplete functional coverage of specifications. Formal methods verify properties that, of course, can be specifications. In practice, however, it is rare that all specifications are given to a formal checker on the complete design, because of memory and runtime limitations. A partial specification is checked against the relevant portion of the design. Therefore, it leaves the door open to errors resulting from not checking all properties mandated by the specifications and from situations when, for example, a property succeeds on a subcircuit but does not succeed on the whole circuit.
- User errors. Example user errors are incorrect representation of specifications and overconstraining the design.
- Formal verification software bugs. Bugs in formal verification software can miss design errors and thus give false confirmation. It is well-known that there is no guarantee for a bug-free software program.