Sciweavers

Share
TODAES
1998

Specification and verification of pipelining in the ARM2 RISC microprocessor

9 years 7 months ago
Specification and verification of pipelining in the ARM2 RISC microprocessor
Abstract State Machines (ASMs) provide a sound mathematical basis for the specification and verification of systems. An application of the ASM methodology to the verification of a pipelined microprocessor (an ARM2 implementation) is described. Both the sequential execution model and final pipelined model are formalized using ASMs. A series of intermediate models are introduced that gradually expose the complications of pipelining. The first intermediate model is proven equivalent to the sequential model in the absence of structural, control, and data hazards. In the following steps, these simplifying assumptions are lifted one by one, and the original proof is refined to establish the equivalence of each intermediate model with the sequential model, leading ultimately to a full proof of equivalence of the sequential and pipelined models. Categories and Subject Descriptors: B.5.2 [Hardware]: Register transfer level implementation—design aids; C.0 [Computer Systems Organization]: Gener...
James K. Huggins, David Van Campenhout
Added 23 Dec 2010
Updated 23 Dec 2010
Type Journal
Year 1998
Where TODAES
Authors James K. Huggins, David Van Campenhout
Comments (0)
books