Practical Issues in Sequential Equivalence Checking through Alignability: Handling Don't Cares and Generating Debug Traces

Reset states are often not known for a given design until late in the design cycle. There is therefore a need for sequential equivalence checking algorithms that work in the absence of this information. One popular choice for such a notion is alignability, which has the allure of not necessarily needing a symbolic traversal of every state in the system. However, to use alignability in practice, there are several obstacles that needs to be overcome. First of all, the standard alignability theory does not take into account that the golden design often may specify a range of acceptable implementations by means of designer annotated don't care states and don't care logic. Second, when two designs are unalignable, the fact that there are no specified initial state makes it hard to generate a meaningful counter-example to aid the designer in debugging the designs. We address these issues by extending the standard alignability theory so that it handles don't care information in the absence of reset states, and by devising a heuristic for finding a meaningful initial state for the debug traces. Our experimental results show that our theory extensions are necessary to be able to deal with a large portion of the industrial designs that we have applied our alignability checking tool to. We also show how our debug trace heuristic has allowed us to find a real optimization tool bug.