MODELLING AND VERIFICATION OF PIPELINED MICRO-ARCHITECTURES: FUNCTIONAL APPROACH

S. Merniz and M. Benmohammed

References

  1. [1] J. Burch & D. Dill, Automatic verification of pipelined microprocessor control, in D. Dill (Ed.), Computer aided verification(CAV’94), LNCS 818 (Springer-Verlag, 1994).
  2. [2] R.M. Hosabettu, M. Srivas, & G. Gopalakrishnan, Decomposing the proof of correctness of pipelined microprocessors, in A.J. Hu & M.Y. Vardi (Eds.), Computer aided verification (CAV) 1998, LNCS 1427 (Springer-Verlag, 1998).
  3. [3] M. Velev & R. Bryant, Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction, Design Automation Conference (DAC’00), Los Angeles, California, USA, 2000.
  4. [4] J.R. Burch, Techniques for verifying superscalar microprocessors, Design Automation Conference (DAC’96), 1996.
  5. [5] M.N. Velev, Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a re-order buffer, Design Automation & Test in Europe (DATE’02), France, 2002.
  6. [6] S.K. Lahiri, S.A. Seshia, & R.E. Bryant, Modeling and verification of out-of-order microprocessors in UCLID, in Mark Aagaard & John W. O’Leary (Eds), Formal methods in computer-aided design (FMCAD’02), LNCS 2517, Porland, Oregon, USA, 2002.
  7. [7] A.C.J. Fox, An algebraic framework for verifying the correctness of hardware with input and output: A formalization in HOL, in Jose Luiz Fiadiero, Neil Herman, Markus Roggenbach & Jan. J.M.M.Rutten (Eds), Conference on Algebra and Coalgebra in Computer Science, CALCO 2005, LNCS 3629, University of Wales, Swansea, UK, 2005.
  8. [8] A.C.J. Fox, Verifying the ARM block data transfer instructions, Designing Correct Circuits Workshop (DCC 2004), Barcelona, 2004.
  9. [9] P. Manolios, Well founded equivalence bissimulation, Technical Report, Department of Computer Science, University of Texas at Austin, 2000.
  10. [10] P. Manolios, Correctness of pipelined machines, in W.A. Hunt & S.D. Johnson (Eds.), Formal methods in computer-aided design (FMCAD: Austin, TX, USA), 2000, 161–1178.
  11. [11] S. Tahar & R. Kumar, A practical methodology for the formal verification of RISC processors, Formal Methods in Systems Design, 13(2), 1998, 159–225.
  12. [12] D. Schostak, Methodology for the formal specification of RTL RISC processor designs, Ph.D. Thesis, the University of Leeds, Leeds, 2003.
  13. [13] K.C. Claessen, An embedded language approach to hardware description and verification, Ph.D. Thesis, Chalmers University of Technology, Gothenburg, Sweden, 2001.
  14. [14] J.R. Matthews, Algebraic specification and verification of processor micro-architectures, Ph.D. Thesis, Oregon Graduate Institute of Science and Technology, Oregon, 2000.
  15. [15] S L. Peyton Jones, et al., Haskell 98: A non strict purely functional language, Revised: February 1999, available at http://www.haskell.org/onlinereport91
  16. [16] F. Orejas, J. Navarro & A. Sanchez, Implementation and behavioural equivalence: A survey, Proc. 8th Workshop on Algebraic Specification, Dourdan, 1991.
  17. [17] S. Merniz & M. Benmohammed, A methodological approach for the formal specification of RISC microprocessors: Application to the MIPS Processor, 5eme Seminaire National en Informatique, Biskra, Algerie, 2005.
  18. [18] S. Merniz & M. Benmohammed, A methodology for the formal verification of RISC microprocessors: A functional approach, ACS International Conference on Computer Systems and Applications (AICCSA’07), Amman, Jordan, 2007.
  19. [19] J.L.Hennessy & D.A. Patterson, Computer architecture: A quantitative approach, Third Edition San Francisco, (CA: Morgan Kaufmann Publishers Inc., 2003).
  20. [20] R.E. Bryant, S.K. Lahiri, & S.A. Seshia, Convergence testing in term level bounded model checking, in Daniel Geist & Enrico Tronci (Eds), Correct Hardware Design and Verification Methods, CHARME 2003, L’Aquita, Italy.
  21. [21] R. Plasmeijer & M.V. Eekelen, Functional programming and parallel graph rewriting (Addison-Wesley, 1993).

Important Links:

Go Back