Accession Number : ADA165696

Title :   Formal Proof of Correspondence between the Specification of a Hardware Module and Its Gate Level Implementation,

Corporate Author : ROYAL SIGNALS AND RADAR ESTABLISHMENT MALVERN (ENGLAND)

Personal Author(s) : Pygott,C H

PDF Url : ADA165696

Report Date : Nov 1985

Pagination or Media Count : 68

Abstract : The growing use of digital circuits in safety critical environments and the cost of correcting mistakes in large scale integrated circuits, both lead to a requirement for a high level of confidence in the correctness of the design of micro-electronic elements. This paper describes a novel application of a general hardware description language that enables the implementation of a synchronous circuit to be checked exhaustively against a high level, implementation independent, specification of its functionality (originally written in a formalism such as first order predicate calculus). The technique avoids the cost, in simulation time, usually associated with exhaustive checking. The method is illustrated by examples written in the design and description language ELLA: no prior knowledge of ELLA is assumed. Included in the annexes to this paper are a library of ELLA functions that provide those facilities required for the validation of circuits, and the translation of specifications written in the first order predicate calculus language LCF-LSM into ELLA.

Descriptors :   *DIGITAL SYSTEMS, *MICROELECTRONICS, *GATES(CIRCUITS), *INTEGRATED CIRCUITS, CALCULUS, CIRCUITS, CONFIDENCE LEVEL, ENVIRONMENTS, LANGUAGE, SAFETY, SIMULATION, TIME, VALIDATION

Subject Categories : Electrical and Electronic Equipment

Distribution Statement : APPROVED FOR PUBLIC RELEASE