This presentation will consist of two complementary talks on the use of FDTs (Formal Description Techniques) standardised for use in data communications. The aim is to show that techniques developed for protocols can be applied with success in hardware design.
Digital hardware is treated as a collection of interacting parallel components. This permits the use of a standard formal technique for specification and analysis of circuit designs. The ANISEED method (Analysis In SDL Enhancing Electronic Design) is presented for specifying and analysing timing characteristics of hardware designs using SDL (Specification and Description Language). A signal carries a binary value and an optional time-stamp. Components and circuit designs are instances of block types in library packages. The library contains specifications of typical components in single/multi-bit and untimed/timed forms. Timing may be specified at an abstract, behavioural or structural level. Timing properties are investigated using an SDL simulator or validator. Consistency of temporal and functioanl aspects may be assessed between designs at different levels of detail. Timing characteristics of a design may also be inferred from validator traces. A variety of examples is used, ranging from a simple gate specification to realistic examples drawn from a standard hardware verification benchmark.
The DILL (Digital Logic in LOTOS) approach allows formal modelling and analysis of synchronous and asynchronous hardware designs. The relevance or protocol conformance testing techniques to hardware testing will be discussed. It will be shown that the ioconf (input-output conformanc) approach used in protocol testing can be applied to generate tests for a synchronous hardware design using its formal specification. The generated tests are automatically applied to a circuit by a VHDL testbench, thus giving confidence that the hardware design meets its high-level formal specification. Case studies will illustrate how the ideas can be applied to standard hardware verification benchmarks such as the Single Pulser and Black-Jack Dealer.