# Sequential Logic Equivalence and Simplification

Different implementations of a circuit may vary in their state encoding or even in the amount of state they keep in terms of bits. One might be simpler or better than the other for a given purpose. At times we need to check the equivalence of deigns.

For a synchronous clock domain, if two designs are known to have the same state encodings, then the problem degenerates to that of combinational equivalence checking of their respective next-state functions. For each D-type flip-flop we need to check the combinational equivalence of its sourcing circuit in the two designs. However, even if the state encodings are the same, there can be un-used portions of the state space which must be treated as don't-cares for this check.

If the state encoding is known to be changed, then what can be compared? Perhaps we can compare the trajectory of states between two designs, building up our own mapping between the encodings in each design. Generally, two designs will have the same set of output terminals and so the basis of the mapping is equivalence classes formed around each possible setting of the output terminals.

This leads to the concept of full equivalence in terms of external observable behaviour. Do the two designs behave the sames as each other in black box testing: that is, without any knowledge of the internal behaviour. If so, they are said to bi-simulate each other.

Again, not all of the reachable state space may be used. The circuit might always be wired up externally so that one input is a delayed version of one output. Therefore the question arises, do a pair of designs follow the same state trajectory when interfacing with a specified reactive automaton ?

Commonly, the number of clock cycles of delay through a sub-system (its latency) is not important and perhaps can be disregarded in equivalence checking. This leads to the concept of temporally floating ports (not lectured in 2008/9), where a pair of designs are equivalent if the timing behaviour inside a port (subset of the external collections) appears equivalent, even though we would see differences if we looked at the relative timing of operations with respect to other ports. For example, the precise order in which an Ethernet hub chip sends a broadcast packet to each of its output ports does not matter, as long as it is actually delivered to each port, and from any given port this ordering cannot be perceived without peeking at the other ports. This sort of floating is similar to the temporal decoupling ides in the loosely-timed models, in that systems are designed, at the high level, to be tolerant to timing and performance variations in their major components. .

Two other variations in the problem definition arise for systems where the exact number of clock cycles is not considered important. This clearly also applies to asynchronous systems without a clock.

• When a pair of sub-systems are wired to each other, the composition may be a synchronous or asynchronous (turn-taking) composition. The algorithms used for making the different combinations may vary (a research topic of DJG) and the possible behaviours may also be different. For instance, it might only be possible to enter a given state (on the next clock edge) without the simultaneous change of two communicating nets, but if these are sourced in different components that share the same clock this might never happen. This is rather like the two main types of auction: where participants either bids in turn, with knowledge of the previous bid, or all bid together without knowledge (competitive tender) and then another round is used when there are tie-breaks needed.
• Strong or weak bi-simulation: a pair of designs might differ in the number of clock cycles they take to produce a response to a given input. As mentioned, this can be hidden by putting the input and output in different temporal groups, or it can be considered a difference (strong bi-simulation) or it can be considered not a difference if no nets other than the clock have changed in the meantime: a stuttering equivalence (a form of weak bi-simulation).

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.