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.
Chapter PDF
Keywords
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
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.
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 85
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.
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)
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.
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.
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)
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.
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.
H.COLLAVIZZA: “Functional Semantics of Microprocessors at the Microprogram Level and Correspondence with the Machine Instruction Level”. Proc. EDAC. March 1990.
H.COLLAVIZZA: “Semantique Fonctionnelle des Microprocesseurs: L'environnement de Spécication et de preuve ”μSPEED” Thesis University of Aix Marseille I 1991.
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)
G. GENTZEN: “Investigation into Logical Deduction” Thesis 1935, reprinted in “The collected papers of Gerhard Gentzen” E. Szabo, North Holland, Amsterdam 1969
M. GORDON: “LCF-LSM”, TR 41, Computer Laboratory, University if Cambridge, England, 1983
W.A. HUNT: “FM8501: A Verified Microprocessor”, Technical Report 47, Institute for Computing Science, University of Texas at Austin, Feb 1986.
J. JOYCE: “Generic Specification of Digital Hardware”, Proc. Work. on Designing Correct Circuits, 26–28 Sept 1990, Glasgow (Springer Verlag)
G. KAHN: “Natural Semantics”, Proc of Symp on Theoretical Aspects of Computer Science, Passau, Germany, LNCS 247,1987.
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.
G.J. MILNE: “Design for Verifiability”, Proc. Work on “Hardware Specification, Verification and Synthesis: Mathematical Aspects”, Ithaca, Jul 89, LNCS 408.
J.L.PAILLET: “Functional Semantics of Microprocessors at the Machine Instruction Level”, Proc 9th IFIP WG 10.2 Conf CHDL,Washington, June 89.
G. PLOTKIN: “A structural approach to operational semantics” Report DAIMI FN-19, Computer Science DPt Aarhus Univ, Danemark, 1981.
G. L. STEELE Jr.: “Common LISP The Language” Second Edition Digital Presss, 1990.
WINDLEY: “The formal Verification of Generic Interpreters”, Phd Thesis, University of California, Division of Computer Science, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chazarain, J., Collavizza, H. (1993). Combining symbolic evaluation and object oriented approach for verifying processor-like architectures at the RT-level. In: Milne, G.J., Pierre, L. (eds) Correct Hardware Design and Verification Methods. CHARME 1993. Lecture Notes in Computer Science, vol 683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021718
Download citation
DOI: https://doi.org/10.1007/BFb0021718
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56778-3
Online ISBN: 978-3-540-70655-7
eBook Packages: Springer Book Archive