file.pdf (123.3 kB)
0/0

Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking

Download (123.3 kB)
journal contribution
posted on 01.06.1997 by Miroslav N Velev, Randal E. Bryant
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 represent uninterpreted symbols with BDDs, while allowing these symbols to be propagated 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 abstraction method builds on the behavioral Efficient Memory Model [18][19] and its capability to dynamically introduce consistent initial state, which is identical for two simulation sequences. We apply the abstraction and encoding ideas on the verification of pipelined microprocessors by correspondence checking, where a pipelined microprocessor is compared against a non-pipelined specification

History

Publisher Statement

All Rights Reserved

Date

01/06/1997

Exports

Exports