Exercise 10: Timed Circuits

As with the last exercise, you should load the numLib library to define the natural numbers before continuing.

Modelling Timed Behaviour

Until now we have been interested in the voltage level on a wire only at a particular point in time. For this purpose it was sufficient to model a wire as a boolean value, with true representing a high value and false representing a low one. We would now like to look at how the voltage on a wire changes over time; for this we require a more elaborate model.

We will model times as natural numbers. Time 0 will be the time at which the circuit is turned on, and greater numbers will represent progressively later times. The length of time between some time point t and the next t+1 will be some arbritrary, but small, period of time; lets call it a tick. For the sake of argument, lets say that a tick is equal to the switching time of a CMOS gate, called a gate delay.

Lets now think of a wire not just as a voltage, but as a wave-form, which describes how the voltage changes over time. We can model this in HOL as a function from numbers to booleans. For example, If w is a wire, then w t models the voltage (high or low) on that wire at time t. For example, imaging the waveform below as a function from numbers to booleans.

Circuits with Delay

Using this model of time, define a predicate DNOR a b c such that the predicate represents a NOR gate with input wires a and b and output wire c, and there is a one `tick' propagation delay between a value being present on the input wires and the corresponding value appearing on the output wire.

Using the DNOR predicate define a predicate SR_IMP r s q q' to represent the following circuit:

SR Flip-Flop

Next, prove the following properties of the flip-flop implementation:

• That if s is held high and r is held low for two time units, then on the third tick q will be high and q' will be low.
• That if s and r are both held low, and if one of q and q' is high and the other low, then at the next time unit the values of q and q' will be unchanged.

Hints:

• Use the conversion Num_conv.num_CONV to get rid of `abstract' decimal notation (e.g., `1',`2', etc.) from your goal early on by converting it into unary form (e.g., `SUC 0', `SUC (SUC 0)').
• The theorem ADD_CLAUSES from the arithmetic theory will be helpful here. The arithmetic theory is loaded as part of the num library. You can access the theorem as arithmeticTheory.ADD_CLAUSES.

You can search for existing theorems using the LAL documentation system by selecting the option `HOL Theorem Manual' from the search menu. Use this facility to find all the theorems with names that contain `ADD'.

The MoscowML help system can be used to learn more about any loaded theory (and many other things besides). For example, use the command `help "arithmeticTheory"' to learn more about the arithmetic theory.