Sciweavers

Share
VLSID
1999
IEEE

Formal Verification of an ARM Processor

9 years 8 months ago
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.
Vishnu A. Patankar, Alok Jain, Randal E. Bryant
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where VLSID
Authors Vishnu A. Patankar, Alok Jain, Randal E. Bryant
Comments (0)
books