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:

• to apply standard LOTOS as a hardware description language, though the timed extensions in E-LOTOS (Enhancements to LOTOS) are also being used
• to exploit existing techniques for LOTOS simulation, prototyping and test generation
• to develop a high-level approach that allows systems to be described abstractly and then refined into lower-level designs, with correctness of the refinement step being verified
• to specify, analyse and test both synchronous and asynchronous circuits
• to specify and analyse timing aspects of hardware designs
• to generate and apply rigorous tests of circuit designs based on their specifications

Approach

• the circuit design approach (synchronous, asynchronous)
• the desired level of abstraction (abstract, structural, behavioural, gate-level)
• the desired delay model (pure delay, inertial delay)
• the relevance of timing (untimed, timed)

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

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:

• DILL: Specifying digital logic in LOTOS presents the foundation for describing digital hardware using LOTOS.
• Extended DILL: Digital Logic in LOTOS shows how the DILL library can be extended for many typical digital components.
• Timed DILL: Digital Logic in LOTOS shows how timed `components' can be added to the library to describe timing delays and timing constraints.
• Specifying Hardware Timing Characteristics with ET-LOTOS uses two time-extended LOTOS variants to model and validate timing properties of hardware designs.
• Protocol-Inspired Hardware Testing adapts an approach used in deriving protocol tests to the testing of hardware.
• Specification and Verification of Synchronous Hardware using LOTOS presents an approach for modelling synchronous hardware designs and verifying properties of them. An extended version of this paper deals with Modelling and Verifying Synchronous Circuits in DILL.
• Verifying and Testing Asynchronous Circuits using LOTOS presents an approach for modelling asynchronous hardware designs, and verifying properties of them such as delay and speed insensitivity.
• Formally-Based Design Evaluation synthesises the results on verification and conformance testing of synchronous and asynchronous circuits.
• Formal Specification and Analysis of Digital Hardware Circuits in LOTOS presents substantial project results including circuit modelling, the circuit library and tools, the specification of synchronous and asynchronous circuits, timing analysis, verification and testing.

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