| EPSRC Reference: |
GR/N13135/01 |
| Title: |
FORMAL SPECIFICATION AND VERIFICATION OF ARM6 |
| Principal Investigator: |
Gordon, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2000 |
Ends: |
31 March 2004 |
Value (£): |
225,869
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Parallel Computing |
| System on Chip |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
We propose to help develop a mthodology for the production of executable specifications of microprocessors cores at both the instruction set and pipelined architectural levels and to use formal verification to establsih equivalence or refinement relationships between these specifications. The key technical challenge is to show that academic verification techniques developed in the 1980's for microprocessor subsystems scale to realistic complete archtectures. The project is a partnership between specifiers and verifiers at Leeds and Cambridge, and designers and engineers from ARM who will actively participate by providing understanding and insights, and reading and critiquing specifications as they emerge. We concentrate upon the ARM6 microprocessor to give the project a concrete focus, but the results and methods will be generally applicable.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.cam.ac.uk |