We describe a technique for verifying the control logic of pipelined microprocessors. It handles more complicated designs, and requires less human intervention, than existing methods. The technique automatically compares a pipelined implementation to an architectural description. The CPU time needed for verification is independent of the data path width, the register file size, and the number of ALU operations. Debugging information is automatically produced for incorrect processor designs. Much of the power of the method results from an efficient validity checker for a logic of uninterpreted functions with equality. Empirical results include the verification of a pipelined implementation of a subset of the DLX architecture.
CITATION STYLE
Burch, J. R., & Dill, D. L. (1994). Automatic verification of pipelined microprocessor control. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 818 LNCS, pp. 68–80). Springer Verlag. https://doi.org/10.1007/3-540-58179-0_44
Mendeley helps you to discover research relevant for your work.