Case Study of the Cambridge Fast Ring ECL Chip using HOL

From bibtex.

Abstract

This article describes the formal specification and verification of an integrated circuit which is part of a local area network interface. A single formal language is used to describe the structure and behaviour at all levels in the design hierarchy, and an associated computerised proof assistant is used to generate all formal proofs. The implementation of the circuit, described as a structure of gates and flip-flops, is verified via a number of levels with respect to a high-level formal specification of required behaviour. The high-level formal specification is shown to be close to precise natural language description of the circuit behaviour. The specification language used, HOL, has the advantage of permitting partial specifications. It turns out that partial specification has an important effect on the specification and verification methodology, and this is presented. We have also evaluated aspects of conventional design, such as techniques for locating errors and the use of simulation, within the case study of formal methods. We assert that proof strategies must assist error location and that simulation has a role alongside formal verification.