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.