EPSRC logo

Details of Grant 

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:
No relevance to Underpinning Sectors Information Technologies
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