Modelling and verification of superscalar Micro-architectures functional approach

ABSTRACT

Most proof approaches verified a pipelined Micro-Architectural (MA) implementation against an Instruction-Set-Architecture (ISA) specification, and consequently, it was impossible to find a meaningful point where the implementation state and the specification state can be compared easily. An alternative solution to such problem is to verify a pipelined micro-architectural implementation against a sequential multi-cycle implementation. Because both models are formalised in terms of clock cycles, all synchronous intermediate states represent interesting points where the comparison could be achieved easily. Furthermore, by decomposing the state, the overall proof decomposes systematically into a set of verification conditions more simple to reason about and to verify. A major advantage of this elegant choice is the ability to carry out the proof by induction within the same specification language rather than by symbolic simulation through a proof tool which remains very tedious. Also, because both models relate to the MA level, there is no need for a data abstraction function, only a time abstraction function is needed to map between the times used by the two models. The potential features of the proposed proof methodology are demonstrated over the pipelined and the superscalar pipelined MIPS processors within Haskell framework.

REFERENCES

• 1: 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
• 2: 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
• 3: Miroslav N. Velev , Randal E. Bryant, Formal verification of superscale microprocessors with multicycle functional units, exception, and branch prediction, Proceedings of the 37th conference on Design automation, p.112-117, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337331]
• 4: 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]
• 5: M. Velev, Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-of-Order Microprocessors with a Reorder Buffer, Proceedings of the conference on Design, automation and test in Europe, p.28, March 04-08, 2002
• 6: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 7: A.C.J. Fox. An algebraic framework for verifying the correctness of hardware with input and output: A formalization in HOL, CALCO 2005, LNCS, 3629, 2005.
• 8: A.C.J Fox. Verifying the ARM Block Data Transfer Instructions, DCC 2004, Barcelona, 2004.
• 9: Panagiotis Manolios, Correctness of Pipelined Machines, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.161-178, November 01-03, 2000
• 10: Sofiéne Tahar , Ramayya Kumar, A Practical Methodology for the Formal Verification of RISC Processors, Formal Methods in System Design, v.13 n.2, p.159-225, Sept. 1998 [doi>10.1023/A:1008622002590]
• 11: K.C. Claessen, An Embedded Language Approach to Hardware Description and Verification, PhD thesis, Chalmers University of technology. 2001.
• 12: John Robert Matthews , John Launchbury, Algebraic specification and verification of processor microarchitectures, Oregon Graduate Institute of Science and Technology, 2000
• 13: S L. Peyton Jones et al, Haskell 98: A non strict, purely functional language. Revised; February 1999. Available at: http://www.haskell.org/onlinereport
• 14: S. Merniz, M. Benmohammed, A Methodology for the Formal Verification of RISC Microprocessors A Functional Approach, AICCSA'07, Amman, Jordan, May 2007.
• 15: John L. Hennessy , David A. Patterson, Computer Architecture: A Quantitative Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
• 16: R.E. Bryant, S.K. Lahiri,, S.A. Seshia. Convergence testing in term level bounded model checking. CHARME 2003.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.0 GENERAL

Additional Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.1 Single Data Stream Architectures
          Subjects: RISC/CISC, VLIW architectures
  C.4 PERFORMANCE OF SYSTEMS
      Subjects: Modeling techniques; Performance attributes

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.6 Simulation Output Analysis

General Terms:
Design, Performance, Verification

Keywords:
Haskell, RISC designs, formal Verification, formal specification, micro-architectures, state functions