ABD - Sequential Logic Simplification

A finite-state machine may have more reachable states than it needs to perform its observable function (n.b. one-hot coding does not increase the reachable state space).

A Moore machine can be simplified by the following procedure: 1. Partition all of the state space into blocks of states where the observable outputs are the same for all members of a block. 2. Repeat until nothing changes (i.e. until it closes) For each input setting: 2a. Chose two blocks, B1 and B2. 2b. Split B1 into two blocks consisting of those states with and without a transition from B2. 2c. Discard any empty blocks. 3. The final blocks are the new states. Bisimulation algorithm not examinable in this course.

Alternative algorithm: start with one partition per state and repeatedly conglomerate. The best algorithms use a mixture of the two approaches to meet in the middle.

»Wikipedia: Formal Equivalence Checking

Research example: CADP package: developed by the VASY team at INRIA.

Commercial products: Conformal by Cadence, Formality by Synopsys, SLEC by Calypto.

One future use of this sort of procedure might be to generate an instruction set simulator for a processor from its full RTL implementation. This sort of de-pipelining would give a non-cycle accurate, higher-level model that runs much faster in simulation.