A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

Abstract. This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. This is a modern RISC architecture with many advanced features. The formalization is detailed and extensive. Considerable tool support has been developed, with the goal of making the model accessible and easy to work with. The model and supporting tools are publicly available – we wish to encourage others to make use of this resource. This paper explains our monadic specification approach and gives some details of the endeavours that have been made to ensure that the sizeable model is valid and trustworthy. A novel and efficient testing approach has been developed, based on automated forward proof and communication with ARM development boards.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Anthony C. J. Fox, Magnus O. Myreen
• Keywords: Current Arm Instruction, ITP 2010, Mathematics, Modern Risc Architecture, Monadic Specification Approach