DILL (Digital Logic in LOTOS)


Introduction
Approach
Status
Papers
Tools

Introduction

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:

Approach

(E-)LOTOS offers the advantages of being internationally standardised, fully formal, and capable of being used at a variety of abstraction levels in design. The key aspect of the approach has been developing appropriate models for component and circuit behaviour. For example different DILL models have been developed for use depending on:

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.

Status

The original DILL approach has been extended considerably. Modelling extensions include dealing with start-up conditions, multi-bit signals, replicated components, bus-like interconnections, tri-state devices and abstract descriptions. The library has been much enlarged to offer a wide range of typical digital components. A variety of standard hardware verification benchmarks have been successfully tackled, including the Blackjack Dealer, Bus Arbiter and Single Pulser. The design of a CPU has also been studied.

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.

Papers

The following papers provide technical details of the work:

Tools

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 Projects

Web Ken Turner Home   Email    Search Search Web Pages

Last Update: 15th July 2006
URL: http://www.cs.stir.ac.uk/~kjt/research/dill.html