Advertisement

Combining symbolic evaluation and object oriented approach for verifying processor-like architectures at the RT-level

  • Jacques Chazarain
  • Hélne Collavizza
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

We consider in this paper the correctness of the translation of an assembly language instruction into a sequence of micro-instructions described at the RT-level. We develop a new method which combines the extensibility and flexibility of object oriented programming paradigm and the efficiency of a specialized computer algebra system. An object oriented programming is naturally well-adapted to express the behaviour associated to each category of components found in hardware description languages. We see each component of the processor as an object (in Common Lisp Object System: CLOS).

The other important feature in order to get a general (and mainly automatic) proof is to be able to execute micro-instructions with symbolic operands. For that purpose, we have implemented a symbolic evaluator which can deal with the operations used at the RT level. The final step of the proof is reduced to the equality of symbolic expressions. Since the memory addressing introduces expressions which need a calculus with operators on bit vectors, we built a specialized, but extensible, computer algebra system for proving the equality of such expressions.

Given the semantics of each level, we succeeded to automatically prove the correctness of the translation into micro-instructions of each assembly language instruction for a given processor.

Keywords

Operational Semantic Computer Algebra System Abstract Syntax Formal Verification Symbolic Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [1]
    D. BORRIONE, P. CAMURATI, P. PRINETTO, J.L PAILLET: “A functional approach to formal hardware verification: The MTI experience”, Proc. IEEE International Conference on Computer Design ICCD'88, New York, Oct. 88.Google Scholar
  2. [2]
    D. BORRIONE, C. LE FAOU: “Overwview of the CASCADE Multi-level Hardware Description Language and its Mixed-Mode Simulation Mechanism”, Proc. IFIP WG 10.2 Int. Conf. CHDL 85, Tokyo, Japan, Aug 85Google Scholar
  3. [3]
    M BICKFORD, M.SRIVAS: “Verification of a Pipelined Microprocessor using CLIO”, Proc Work. on “Hardware Specification, Verification and Synthesis: Mathematical Aspects”, Ithaca, Jul 89, LNCS 408.Google Scholar
  4. [4]
    P. CAMURATI, P. PRINETTO: “Formal verification of hardware correctness: an introduction”, Proc. 8th IFIP int. Conf CHDL 87, Armsterdam, April 1987 (also in computer 88)Google Scholar
  5. [5]
    W.J. CARTER, W.H.JOYNER. D. BRAND: “Symbolic Simulation for Correct Machine Design”, ACM IEEE 16th Design Automation Conference, June 1979, pp 280–286.Google Scholar
  6. [6]
    A. COHN: “A Proof of Correctness of the Viper Microprocessor”, in proc. workshop “VLSI Specification, Specification and Synthesis”, ed. G Birtwistle and P.A Subrahmanyam, Kaigary, KWA 1987.Google Scholar
  7. [7]
    P. CAMURATI, P. PRINETTO: “Formal verification of hardware correctness: an introduction”, Proc. 8th IFIP int. Conf CHDL 87, Armsterdam, April 1987 (also in computer 88)Google Scholar
  8. [8]
    J. CHAZARAIN, H. COLLAVIZZA: “An Object Oriented Approach for Specifying and Proving Processor Like Architectures at the RT-Level” Research Rapport RR-92-69 CNRS URA 1376 Sophia Antipolis, 1992.Google Scholar
  9. [9]
    L. CLAESEN, D. BORRIONE, H. EVEKING, G.J. MILNE, J.L. PAILLET, P. PRINETTO: “CHARME: towards formal design and verification for provably correct VLSI hardware”, in proc. of the advanced work. on Correct Hardware Design Methodology, Turin,12–14 June 1991.Google Scholar
  10. [10]
    H.COLLAVIZZA: “Functional Semantics of Microprocessors at the Microprogram Level and Correspondence with the Machine Instruction Level”. Proc. EDAC. March 1990.Google Scholar
  11. [11]
    H.COLLAVIZZA: “Semantique Fonctionnelle des Microprocesseurs: L'environnement de Spécication et de preuve ”μSPEED” Thesis University of Aix Marseille I 1991.Google Scholar
  12. [12]
    D. VERKEST, L.CLAESEN: “Special Benchmark Session on Tautology Checking”, Proc. IFIP WG 10.2/10.5 Work. on “Applied Formal Methods for Correct VLSI Design”, Houthalen, Belgium, 13–16 Nov. 1989 (Ed. by L. Claesen, North Holland)Google Scholar
  13. [13]
    G. GENTZEN: “Investigation into Logical Deduction” Thesis 1935, reprinted in “The collected papers of Gerhard Gentzen” E. Szabo, North Holland, Amsterdam 1969Google Scholar
  14. [14]
    M. GORDON: “LCF-LSM”, TR 41, Computer Laboratory, University if Cambridge, England, 1983Google Scholar
  15. [15]
    W.A. HUNT: “FM8501: A Verified Microprocessor”, Technical Report 47, Institute for Computing Science, University of Texas at Austin, Feb 1986.Google Scholar
  16. [16]
    J. JOYCE: “Generic Specification of Digital Hardware”, Proc. Work. on Designing Correct Circuits, 26–28 Sept 1990, Glasgow (Springer Verlag)Google Scholar
  17. [17]
    G. KAHN: “Natural Semantics”, Proc of Symp on Theoretical Aspects of Computer Science, Passau, Germany, LNCS 247,1987.Google Scholar
  18. [18]
    M. LANGEVIN, E. CERNY: “Verification of processor-like circuits”, in proc. of the advanced work. on Correct Hardware Design Methodology, Turin 12–14 June 1991.Google Scholar
  19. [19]
    G.J. MILNE: “Design for Verifiability”, Proc. Work on “Hardware Specification, Verification and Synthesis: Mathematical Aspects”, Ithaca, Jul 89, LNCS 408.Google Scholar
  20. [20]
    J.L.PAILLET: “Functional Semantics of Microprocessors at the Machine Instruction Level”, Proc 9th IFIP WG 10.2 Conf CHDL,Washington, June 89.Google Scholar
  21. [21]
    G. PLOTKIN: “A structural approach to operational semantics” Report DAIMI FN-19, Computer Science DPt Aarhus Univ, Danemark, 1981.Google Scholar
  22. [22]
    G. L. STEELE Jr.: “Common LISP The Language” Second Edition Digital Presss, 1990.Google Scholar
  23. [23]
    WINDLEY: “The formal Verification of Generic Interpreters”, Phd Thesis, University of California, Division of Computer Science, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Jacques Chazarain
    • 1
  • Hélne Collavizza
    • 1
  1. 1.Laboratoire d'Informatique I3SUniversité de Nice Sophia Antipolis CNRS. URA 1376ValbonneFrance

Personalised recommendations