Specification and verification of digital systems using higher-order predicate logic

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.