| EPSRC Reference: |
GR/S11084/01 |
| Title: |
An Integrated Framework for Formal Verification and Distributed Simulation of Asynchronous Hardware |
| Principal Investigator: |
Edwards, Dr DA |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Victoria University of Manchester, The |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 April 2003 |
Ends: |
31 March 2006 |
Value (£): |
186,432
|
| EPSRC Research Topic Classifications: |
| Modelling & simul. of IT sys. |
System on Chip |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Asynchronous hardware designs have received much attention recently due to their potential for energy savings, and consequently their suitability deployment in embeddded and mobile devices such as smartcards. Fundamental differences of timing in asynchronous hardware render conventic hardware description languages inappropriate for their modelling, make them susceptible to deadlock and place an additional requirement for adequate performance evaluation of the designs. This proposal aims to develop an integrated framework for the analysis of asynchronous hardware design; formal verification and distributed simulation. It will be implemented as an enhancement of an existing Balsa toolkit, developed by the AMULET group that supports limited analysis of the designs via simulation and various technologies for manufacture in VLSI. The core of the framework will be the process algebra CSP. CSP has an underlying mathematical theory and inherent parallelism, features that can be exploited to perform both formal verification and distributed simulation. Formal verification of properties such as deadlock and equivalence checking will be implemented through th translation of Balsa into machine readable CSP, invoking the model checker FDR and back-translating the diagnostics. Distributed simulation will ensure timing analysis of Balsa designs and performance evaluation of benchmark programs. The framework will be evaluated on major asynchronous hardware designs, such as the Amulet3i processor aimed at embedded systems.
|
|
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: |
|