Formal verification of a pipelined processor with new memory hierarchy using a commercial model checker

Recently, model checkers have become commercially available. To investigate their ability, Solidify is selected as the representative of them and applied to a verification of a new processor. The processor adopts new memory hierarchy and new instructions. Its instruction issue is pipelined and in-order. Our experiment reveals that Solidify can verify the processor but drastic abstraction is indispensable for successful verification. The experimental results also suggest that it is quite hard to verify more complex out-of-order issue processors without very drastic and efficient abstraction. Through the experience, we also recognize the benefit of fully automatic verification. However, we suffer from the invariant problems. Experience is still important for this problem.