S. Merniz and M. Benmohammed
[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] R.M. Hosabettu, M. Srivas, & G. Gopalakrishnan, Decom-posing 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] 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] J.R. Burch, Techniques for verifying superscalar microprocessors, Design Automation Conference (DAC’96), 1996. [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] 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] 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] A.C.J. Fox, Verifying the ARM block data transfer instructions, Designing Correct Circuits Workshop (DCC 2004), Barcelona, 2004. [9] P. Manolios, Well founded equivalence bissimulation, Technical Report, Department of Computer Science, University of Texas at Austin, 2000. [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] 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] D. Schostak, Methodology for the formal specification of RTL RISC processor designs, Ph.D. Thesis, the University of Leeds, Leeds, 2003. [13] K.C. Claessen, An embedded language approach to hardware description and verification, Ph.D. Thesis, Chalmers University of Technology, Gothenburg, Sweden, 2001. [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] 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] F. Orejas, J. Navarro & A. Sanchez, Implementation andbehavioural equivalence: A survey, Proc. 8th Workshop onAlgebraic Specification, Dourdan, 1991. [17] S. Merniz & M. Benmohammed, A methodological approachfor the formal specification of RISC microprocessors: Appli-cation to the MIPS Processor, 5eme Seminaire National enInformatique, Biskra, Algerie, 2005. [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] J.L.Hennessy & D.A. Patterson, Computer architecture: A quantitative approach, Third Edition San Francisco, (CA:Morgan Kaufmann Publishers Inc., 2003). [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] R. Plasmeijer & M.V. Eekelen, Functional programming and parallel graph rewriting (Addison-Wesley, 1993).
Important Links:
Go Back
