Formal Verification of an ARM Processor

This paper presents a detailed description of the application of a formal verification methodology to an ARM processor. The processor, a hybrid between the ARM7 and the StrongARM processors, uses features such as a 5-stage instruction pipeline, predicated execution, forwarding logic and multi-cycle instructions. ruction set of the processor was defined as a set of abstract assertions. An implementation mapping to relate the abstract states in these assertions to detailed circuit states in the gate-level implementation of the processor. Symbolic Trajectory Evaluation was used to verify that the circuit fulfills tract assertion under the implementation mapping. The verification was done concurrently with the design implementation of the processor. Our verification did uncover 4 bugs that were reported back to the designer in a timely manner.

• Type: Conference
• Year: 1999
• Where: VLSID
• Authors: Vishnu A. Patankar, Alok Jain, Randal E. Bryant
• Keywords: ARM Processor, Formal Verification Methodology, Implementation Mapping, VLSI, VLSID 1999