Bit-level abstraction in the verification of pipelined microprocessors by correspondence checking

Abstract. We present a way to abstract functional units in symbolic simulation of actual circuits, thus achieving the effect of uninterpreted functions at the bit-level. Additionally, we propose an efficient encoding technique that can be used to repre-sent uninterpreted symbols with BDDs, while allowing these symbols to be propa-gated by simulation with a conventional bit-level symbolic simulator. Our abstraction and encoding techniques result in an automatic symmetry reduction and allow the control and forwarding logic of the actual circuit to be used unmodified. The abstrac-tion method builds on the behavioral Efficient Memory Model [18][19] and its capa-bility to dynamically introduce consistent initial state, which is identical for two simulation sequences. We apply the abstraction and encoding ideas on the verifica-tion of pipelined microprocessors by correspondence checking, where a pipelined microprocessor is compared against a non-pipelined specification.