摘要:

The paper describes how higher-order predicate logic may be used to specify both the structure and the behaviour of a digital system, and to reason about their interrelationship. The overall approach is named VERITAS; the paper concentrates particularly on describing its methodological aspects. The behaviour of a system is specified by a predicate on the analogue waveforms at the ports of the system. In general, behavioural specifications are partial. The internal structure of a system is defined by a set of projection functions that yield its component parts, together with a set of equations describing their interconnections. Reasoning about the behavioural properties of digital systems is carried out within the framework of an axiomatic theory that describes relevant properties of arithmetic, time, waveforms and structures. The logic is embedded within a programming language, MV, whose data types include signature, term and derivation. This allows inferencing to be carried out computationally, which in turn guarantees its correctness.

DOI:10.1049/ip-e.1986.0031

出版商:IEE    

年代:1986

数据来源: IET

摘要:

We describe how the functional correctness of a circuit design can be verified by machine checked formal proof. The proof system used is LCF_LSM, a version of Milner's LCF with a different logical calculus called LSM. We give a tutorial introduction to LSM in the paper. Our main example is the ECL chip of the Cambridge fast ring (CFR). Although the ECL chip is quite simple (about 360 gates) it is nevertheless real. Minor errors were discovered as we performed the formal proof, but when the corrected design was eventually fabricated it was functionally correct first time. The main steps in the verification were: (a) writing a high-level behavioural specification in the LSM notation, (b) translating the circuit design from its modula-2 representation in the Cambridge design automation system to LSM, (c) using the LCF_LSM theorem-proving system to generate mechanically a proof that the behaviour determined by the design is equivalent to the specified behaviour. To accomplish the second of these steps, an interface between the Cambridge design automation system, and the LCF_LSM system was constructed

DOI:10.1049/ip-e.1986.0032

出版商:IEE    

年代:1986

数据来源: IET

摘要:

The paper illustrates the use of a mechanical model for describing the time behaviour of hardware. In this model, any variable is represented by a function of time, giving the value of the variable at each instant. Some tools are introduced for describing such functions, and the use of function algebra, for reasoning about hardware descriptions, is illustrated.

DOI:10.1049/ip-e.1986.0033

出版商:IEE    

年代:1986

数据来源: IET

摘要:

A method is presented for automatically verifying asynchronous sequential circuits using temporal logic specifications. The method takes a circuit desctibed in terms of Boolean gates and Muller elements, and derves a state graph that summaries all possible circuit executions resulting from any set of finite delays on the outputs of the components. The correct behaviour of the circuit is expressed in CTL, a temporal logic. This specification is checked against the state graph using a model checker program. Using this method, a timing error in a published arbiter design is discovered. A corrected arbiter is given and verified

DOI:10.1049/ip-e.1986.0034

出版商:IEE    

年代:1986

数据来源: IET

摘要:

The paper describes a study of an aid for hardware logic design using temporal logic, called linear time temporal logic (LTTL), and Prolog. A review of specification techniques for synchronisation parts using LTTL is given. A temporal logic programming language called Tokio, which is based on LTTL and includes interval variables, is presented. As parallelisms are tedious to describe sequentially in LTTL, the notion of interval variables which express a finite number of successive times is introduced.

DOI:10.1049/ip-e.1986.0035

出版商:IEE    

年代:1986

数据来源: IET

摘要:

A VLSI design language, µFP, is presented and it is shown how it can be used in the development of regular array circuits. The higher order functions which are used to build circuit descriptions have geometric as well as semantic interpretations. They allow common circuit forms to be described simply and concisely. The language obeys various algebraic laws, and circuits are developed by transforming a correct (but possibly inefficient) initial design into a more acceptable implementation. A transformation consists of the application of one or more of the algebraic laws and the final circuit is guaranteed to have the same behaviour as the original one. This algebraic approach to circuit design and verification is demonstrated by using it to develop several alternative systolic and semi-systolic implementations of a simple FIR filter.

DOI:10.1049/ip-e.1986.0036

出版商:IEE    

年代:1986

数据来源: IET