ABD - Sequential Equivalence Checker

Another common question that needs checking is sequential equivalence. Do a pair of designs follow the same state trajectory ?

• Considering the values of all state variables ?
• Considering a re-encoding of the state variables ?
• For an observable subset of the state (e.g. at an interface) ?
• When interfacing with a given reactive automaton ?

Other freedoms that could be allowed within the notion of equivalence:

• Temporally floating ports - latency independence.
• Synchronous or asynchronous (turn-taking) composition.
• Strong or weak bi-simulation (stuttering equivalence).

Practical problem: Designs may only be equivalent in the used portion of the state space.