next up previous contents
Next: Experiments in Specification Up: Meeting at Madrid Previous: Strongly-typed Theory of

Rigorous Specifications of Gates and Flipflops

by Keith Hanna, University of Kent

The specification of the behaviour of gates and flipflops at the synchronous level is trivial: all signals are well defined and the functions are well defined and of extreme simplicity.

When viewed at the asynchronous level of abstraction, however, matters are rather more complex. Many published specifications are unrealisable or inconsistent.

One approach to developing specifications at this level of abstraction is to work in terms of atomic predicates that assert that a given signal is constant at a given digital level over a specified interval of time. Using this approach, a behavioural specification of (for example) a latched D-type flipflop becomes a predicate over the tuple of waveforms at its terminals, and this predicate can be expressed relatively easily in terms of the above atomic predicates. Formal verification of asynchronous circuitry can be handled within the same framework.



Bernhard Moeller
Fri May 12 14:21:20 MET DST 1995