| EPSRC Reference: |
GR/T06315/01 |
| Title: |
Applications of Theorem Proving to Assertion Based Verification |
| 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 November 2004 |
Ends: |
31 October 2007 |
Value (£): |
199,077
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
| System on Chip |
VLSI Design |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
We will investigate new ways of applying theorem proving to Assertion Based Verification (ABV ) that use carefully optimised proof scripts to interpret machine readable versions of the formal semantics of industrial property languages.We hope to contribute to solving two problems that beset the current use of assertions: different tools support different 'standard' property languages, and it is difficult for property writers to be sure that required behaviour has been adequately captured. We will address the first of these by implementing proof based translation between languages, using PSL and SystemVerilog Assertions as examples. To make property writing easier, we will develop higher level property constructs and supporting tools that aid design intent capture and provide facilities for converting properties into the form needed for eployment in verification (e.g. factoring complex properties into equivalents sets of simpler ones, then expressing them in a specific property language, or as simulation monitors).In a separate research thread, we will explore new methods for statically checking, by theorem proving, that properties hold of models.
|
|
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 |