Miroslav N. Velev Carnegie Mellon University

Formal Verification of VLIW Microprocessors with Speculative Execution

I will begin with a summary of abstraction techniques for reducing the complexity of microprocessor formal verification: 1) functional units and memories are replaced with "black boxes" that satisfy very few of their original properties; and 2) data operands and memory states are abstracted each with a single symbolic value, whose only property is that of equality/inequality with other symbolic values. Our main contributions are the properties of Positive Equality and conservative transformations. They allow us to replace most of the symbolic values with distinct constants, thus dramatically pruning the solution space and accelerating the correctness proof with orders of magnitude. As a result, a single-issue 5-stage pipelined DLX processor can be formally verified in just 0.22 seconds by a completely automatic tool. Next, I will present the formal verification of microprocessors with exceptions, branch prediction, and multicycle functional units. All of these techniques were applied to a 9-wide VLIW processor that imitates the Intel Itanium in the number and types of functional units, as well as in speculative features such as predicated execution, register remapping, advanced loads, and branch prediction. Recent progress in Boolean Satisfiability (SAT) checkers has resulted in additional speedup of orders of magnitude. Now the above VLIW benchmark can be formally verified in only 15 minutes.

Bio
Miroslav has B.S./M.S. in Electrical Engineering, and B.S. in Economics, received simultaneously from Yale University in May, 1994. He worked on the development of a global information system in the Information Services of Credit Suisse First Boston Corporation, New York, 1994-95. In the fall of 1995, he joined the Department of Electrical and Computer Engineering at Carnegie Mellon University, where he is a Ph.D. candidate advised by Prof. Randal Bryant. Miroslav is the recipient of the Franz Tuteur Memorial Prize for the Most Outstanding Senior Project in Electrical Engineering at Yale University, May 1994.