White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

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

Schostak, Daniel Paul (2003) Methodology for the formal specification of RTL RISC processor designs (with particular reference to the ARM6). PhD thesis, University of Leeds.


Download (1570Kb)


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.

Item Type: Thesis (PhD)
Additional Information: Supplied directly by the School of Computing, University of Leeds.
Academic Units: The University of Leeds > Faculty of Engineering (Leeds) > School of Computing (Leeds)
Identification Number/EthosID: uk.bl.ethos.529168
Depositing User: Dr L G Proll
Date Deposited: 03 Mar 2011 16:22
Last Modified: 07 Mar 2014 11:23
URI: http://etheses.whiterose.ac.uk/id/eprint/1314

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)