| EPSRC Reference: |
GR/J42236/01 |
| Title: |
A SEMANTICALLY BASED DESIGN ENVIRONMENT FOR ASICS |
| 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: |
16 November 1993 |
Ends: |
15 November 1996 |
Value (£): |
134,236
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
To develop an environment based on the HOL theorem proving system that will support the design of correct circuits from specifications given in multiple hardware description languages. Transformation of language texts and synthesis of netlists will be done with reference to formal semantics of the languages, giving a high degree of assurance in their correctness.Progress:Tools have been implemented to assist in the embedding of computer languages in the HOL theorem proving system. These all take the same syntactic specification as their input and include a lexical analyser generator, a parser generator, a pretty-printer generator (not yet fully integrated), and programs that produce definitions of ML datatypes and HOL logical types for representing abstract syntax trees (ASTs). Definitions of ML functions to map between the two representations of ASTs can also be generated. This will create a synergy between the use of slow but trustworthy operations in the logic and fast but less secure operations in ML. The pretty-printers will allow language texts that have been generated by transformation from other languages or within the same language to be output in concrete syntax and thus be used by other programs. The tools have been tested on the full ELLA 2000 language, a realistically-sized hardware description language. The next step is to produce tools that generate logical definitions and ML function declarations from a semantic specification. These tools are likely to be less general and less automatic than those for syntax. Although the production of the tools has been quite time consuming, they have two significant benefits. First, the work involved in embedding each language specified in the case for support will be greatly reduced as the tools do much of the work automatically. Second, the specifications of syntax and semantics together will allow automatic generation of certain proof tools such as symbolic evaluators (simulators), and fast but less secure versions can be generated in ML allowing rapid testing of designs. In other words, the high level specifications eliminate duplication of effort and will allow automation that would not be possible if direct implementations of parsers, etc., were used. The syntax of ELLA 2000 has already been embedded. This will be reduced to a tractable subset when the semantics is considered. The semantics will be based on the one produced in the IED project The HOL Verification of ELLA Designs . There has been a change of plan concerning which other languages will be considered. The company supporting the Qudos HDL (which was a target language in the case for support) has ceased trading, and since this language is not widely used, we have decided to consider a subset of the Verilog HDL instead. Verilog is widely used in commercial electronic design. We still intend to embed the Xilinx XNF netlist language and the simple imperative programming language SAFE. We are also monitoring the progress of work elsewhere to produce a formal semantics for the VHSIC Hardware Description Language (VHDL). The rejection of Qudos HDL means that all our prototyping of designs will now be done using Xilinx gate arrays.
|
|
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 |