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

摘要

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.