Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction

ABSTRACT

We extend the Burch and Dill flushing technique [6] for formal verification of microprocessors to be applicable to designs where the functional units and memories have multicycle and possibly arbitrary latency. We also show ways to incorporate exceptions and branch prediction by exploiting the properties of the logic of Positive Equality with Uninterpreted Functions [4][5]. We study the modeling of the above features in different versions of dual-issue superscalar processors.

REFERENCES

• 1: W. Ackermann, Solvable Cases of the Decision Problem, North-Holland, Amsterdam, 1954.
• 2: ARM Technical Reference Manuals & Data Sheets, http: //www. arm. com.
• 3: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 4: Randal E. Bryant , Steven M. German , Miroslav N. Velev, Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions, Proceedings of the 11th International Conference on Computer Aided Verification, p.470-482, July 06-10, 1999
• 5: R.E. Bryant, S. German, and M.N. Velev, "Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic,''2 Technical Report CMU-CS-99-115, Carnegie Mellon University, 1999.
• 6: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 7: Jerry R. Burch, Techniques for verifying superscalar microprocessors, Proceedings of the 33rd annual conference on Design automation, p.552-557, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240623]
• 8: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 9: CUDD-2.3.0, http ://vlsi. colorado, edu/~fabio.
• 10: Anuj Goel , Khurram Sajid , Hai Zhou , Adnan Aziz , Vigyan Singhal, BDD Based Procedures for a Theory of Equality with Uninterpreted Functions, Proceedings of the 10th International Conference on Computer Aided Verification, p.244-255, June 28-July 02, 1998
• 11: John L. Hennessy , David A. Patterson, Computer architecture (2nd ed.): a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 12: Ravi Hosabettu , Mandayam K. Srivas , Ganesh Gopalakrishnan, Decomposing the Proof of Correctness of pipelined Microprocessors, Proceedings of the 10th International Conference on Computer Aided Verification, p.122-134, June 28-July 02, 1998
• 13: R. Hosabettu, M. Srivas, and G. Gopalakrishnan, "Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions Approach," Computer-Aided Verification (CAV'99), N. Halbwachs and D. Peled, eds., LNCS 1633, Springer-Verlag, June 1999, pp. 45-59.
• 14: MoCORE: microRISC Engine Programmer's Manual, http://www, motorola, com/SPS/MCORE.
• 15: Amir Pnueli , Yoav Rodeh , Ofer Shtrichman , Michael Siegel, Deciding Equality Formulas by Small Domains Instantiations, Proceedings of the 11th International Conference on Computer Aided Verification, p.455-469, July 06-10, 1999
• 16: Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
• 17: Jun Sawada , Warren A. Hunt, Jr., Processor Verification with Precise Exeptions and Speculative Execution, Proceedings of the 10th International Conference on Computer Aided Verification, p.135-146, June 28-July 02, 1998
• 18: Stanford Validity Checker, http: //sprout. stanford, edu.
• 19: Incorporating Timing Constraints in the Efficient Memory Model for Symbolic Ternary Simulation, Proceedings of the International Conference on Computer Design, p.400, October 05-05, 1998
• 20: Miroslav N. Velev , Randal E. Bryant, Bit-Level Abstraction in the Verfication of Pipelined Microprocessors by Correspondence Checking, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.18-35, November 04-06, 1998
• 21: Miroslav N. Velev , Randal E. Bryant, Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.37-53, September 27-29, 1999
• 22: M.N. Velev, and R.E. Bryant, "Formal Verification of Superscalar Microprocessors with Multicycle Functional Units, Exceptions, and Branch Prediction,''2 Technical Report CMU-CS-00-116, Carnegie Mellon University, 2000.

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification