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.