Methodology for the formal specification of RTL RISC processor designs (with particular reference to the ARM6)

Due to the need to meet increasingly challenging objectives of increasing performance, reducing power consumption and reducing size, synchronous processor core designs have been increasing significantly in complexity for some time now. This applies to even those designs originally based on the RISC principle of reducing complexity in order to improve instruction throughput and the performance of the design.

As designs increase in complexity, the difficulty of describing what the design does and demonstrating that the design does indeed do this, also increases. The usual practice of describing designs using natural languages rather than formal language exacerbates this because of the ambiguities inherent in natural language descriptions. Hence this thesis is concerned with the development of a scalable methodology for the creation of a formal description of synchronous processor core design

Not only does the methodology of this thesis provide a standardised approach for describing synchronous processor core designs, but the description that it generates can be used as a basis for the formal verification of the solutions to the problem that increasing complexity poses for traditional validation.

The concept of different presentations of one description is part of the methodology of this thesis and is use to reconcile differences in how the description is best used for one purpose or another.

The methodology of this thesis was developed for the formal specification of the ARM6 processor core and thus this design provides the primary example used in this thesis. Case studies of the use of the methodology of this thesis with other processor cores and a modernised version of the ARM6 are also discussed.