HOME       UP       PREV       FURTHER NOTES       NEXT (Automated Stimulus Generation (Directed-Random Verification))  

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.


26: (C) 2008-13, DJ Greaves, University of Cambridge, Computer Laboratory.