| EPSRC Reference: |
GR/N64243/01 |
| Title: |
HARDWARE VERIFICATION BY COMBINING MODEL CHECKING AND THEOREM PROVING TECHNOLOGIES |
| Principal Investigator: |
Jackson, Dr PB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
30 November 2000 |
Ends: |
29 June 2004 |
Value (£): |
59,274
|
| EPSRC Research Topic Classifications: |
| Electronic Devices & Subsys. |
Fundamentals of Computing |
|
| EPSRC Industrial Sector Classifications: |
| Information Technologies |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The intellectual challenge of this research is to discover how best to formally crystallise a central essence of the architecture and logical structure (eg symmetry) of complex integrated circuit (IC) designs.The changing economics of IC design are making design errors increasingly costly. Intel lost 300M in 1995 because of a design error in an early version of the Pentium IC. This proposal concerns a method for combining two formal techniques for verifying the functional of IC designs. Formal techniques analyse the mathematical structure of designs and can provide stronger assurances of correctness than can simulation, the traditional functional verification technique.The two formal techniques are more highly automated and easier to use model checking and the more flexible mechanical theorem proving. The novelty is that we plan to generalise in a theorem prover the design abstraction mechanisms that are currently essential in model checkers to make them practically useful. We anticipate that this generalisation will allow us to significantly advance the best currently available formal verification technologies. We intend to demonstrate our work with at least one cutting edge verification case study.
|
|
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.ed.ac.uk |