Efficient bit-level model reductions for automated hardware verification

Transition systems which do not perform domain-specific operations on their state variables can be efficiently reduced. We present two different algorithms which automatically eliminate domain-specific operations and reduce the domains of occurring variables from infinite to small domains. Our work extends earlier techniques which are applicable solely to combinatorial properties to temporal properties of transition systems. We have implemented our algorithm as a proof method in the Isabelle/HOL theorem prover and applied it to bit-level hardware designs. To demonstrate the efficiency of our technique, we fully automatically verify a liveness property of a pipelined processor and correctness of a memory management unit.