We present a technique for automatic verification of pipelined microprocessors using model checking. An- tecedent conditioned slicing is an efficient abstraction tech- nique for hardware designs at the Register Transfer Level (RTL). Antecedent conditioned slicing prunes the verifica- tion state space, using information from the antecedent of a given LTL property. In this work, we model instructions of a pipelined processor as LTL properties, such that the instruc- tion opcode forms the antecedent. We use antecedent condi- tioned slicing to decompose the problem space of pipelined processor verification on an instruction-wise basis. We pass the resulting smaller, tractable problems through a lower level verification engine.

We thereby verify that every instruction behaves accord- ing to the specification and ensure that non-target registers are not modified by the instruction. We use the SMV model checker to verify all the instruction classes of a Verilog RTL implementation of the OR1200, an off-the-shelf pipelined processor.