Anzeige
Erschienen in:
2003 | OriginalPaper | Buchkapitel
Formal Specification and Verification of ARM6
verfasst von : Anthony Fox
Erschienen in: Theorem Proving in Higher Order Logics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper gives an overview of progress made on the formal specification and verification of the ARM6 micro-architecture using the HOL proof system. The ARM6 is a commercial processor design prevalent in mobile and embedded systems – it features a 3-stage pipeline with a multi-cycle execute stage, six operating modes and a rich 32-bit RISC instruction set. This paper describes some of the difficulties encountered when working with a full blown instruction set architecture that has not been designed with verification in mind.