Implicit manipulation of equivalence classes for large finite state machines

In the fields of synthesis and verification of VLSI circuits, sequential op timisation has attracted increasing interest due to the time, area and powe r constraints of modern devices. For example, state minimisation aims to re duce the number of states of a sequential circuit, optimising its represent ation. The need to handle large state sets makes implicit methods, based on binary decision diagrams and symbolic traversal techniques, quite appealin g. 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 st ate-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 s pace is pruned by constraining it to well suited subspaces. To this purpose , the concepts of underestimation of equivalence classes, and of non-minima l reduction are introduced. This leads to major simplifications and is quit e effective in dealing with large problems and improving efficiency.