A central task in formal verification is the definition of *
invariants*, which characterize the reachable states of the system.
When a system is finite-state, invariants can be discovered
automatically.
Our experience in verifying microprocessors using symbolic logic
is that finding adequate invariants is extremely time-consuming.
We present three techniques for automating the discovery of some of these
invariants. All of them are essentially syntactic transformations on
a logical formula derived from the state transition function. The
goal is to eliminate quantifiers and extract small clauses implied by
the larger formula.
We have implemented the method and exercised it on a description
of the FLASH Protocol Processor (PP), a microprocessor designed
at Stanford for handling communications in a multiprocessor. We had
previously verified the PP by manually deriving invariants.
Although the method is simple, it discovered
6 out of 7 of the invariants needed for verification of the CPU
of the processor design, and 28 out of 72 invariants needed for
verification of the memory system of the processor.
We believe that, in the future, the discovery of invariants
can be largely automated by a combination of different methods,
including this one.