Implicit manipulation of equivalence classes for large finite state machines

In the fields of synthesis and verification of VLSI circuits, sequential optimisation has attracted increasing interest due to the time, area and power constraints of modern devices. For example, state minimisation aims to reduce the number of states of a sequential circuit, optimising its representation. The need to handle large state sets makes implicit methods, based on binary decision diagrams and symbolic traversal techniques, quite appealing. Nevertheless, implicit techniques have limitations, and two improvements to standard methods are proposed to deal with larger circuits. First, the degree of freedom offered by don´t care sets is exploited to enhance the state-of-the-art approach using cofactor-based techniques. Internal steps of the process are simpler and faster, although very large problems cannot be dealt with. Secondly, partitioning and approximation are used. The search space is pruned by constraining it to well suited subspaces. To this purpose, the concepts of underestimation of equivalence classes, and of non-minimal reduction are introduced. This leads to major simplifications and is quite effective in dealing with large problems and improving efficiency