This project has been mainly undertaken by Ji He (Helen Ji) under the supervision of Ken Turner . The project was supported by the University of Stirling, the Overseas Research Studentship scheme and the Sino-British Fellowship Trust.
The goal of this work is to develop a method for formally specifying and analysing digital hardware designs. The project is delivering a rigorous method, library and accompanying tools for specifying and analysing circuits using LOTOS (Language Of Temporal Ordering Specification, ISO/IEC 8807) as the formal basis. The work is taking into account existing results on formal description of hardware and software. It is a considerable extension of the original work by Ken Turner and Richard Sinnott on the DILL language and tools.
The objectives of the project are:
These models are captured in a substantial library of ready-specified components. The designer can include components using a high-level macro notation that requires only limited knowledge of LOTOS. A circuit specification is then generated automatically from this, and processed by standard and extended LOTOS tools and techniques.
The main toolset used with DILL specifications is CADP (Cæsar Aldébaran Development Package). This supports basic specification, simulation and verification using LOTOS. In addition, DILL has extended CADP with algorithms for generating tests for synchronous and asynchronous circuit designs. The tests are automatically applied using a VHDL testbench and a low-level circuit design expressed in VHDL. Further algorithms are used to check delay and speed insensitivity of asynchronous designs.
An approach has also been developed for describing timing characteristics using DILL. Timing `components' in the library allow an untimed description to be extended with delays and timing constraints. Models have also been created for synchronous and asynchronous designs. A method has been developed for formally verifying delay-independence and speed-independence in asynchronous circuit designs.
Hardware testing has been studied by extending results from IOLTS (Input-Output Labelled Transition Systems) in protocol conformance testing. This allows useful tests to be derived automatically from circuit designs. The tests can then be automatically applied, e.g. to the corresponding VHDL description. This approach has shown up timing errors in otherwise correct benchmark designs.
The following papers provide technical details of the work:
Some of the DILL library, tools and examples are available online (though these have now been superseded by later versions).
Up one level to Ken Turner - Research ProjectsLast Update: 15th July 2006