NEXT (ABD - Sequential Logic Simplification)
ABD - Sequential Equivalence Checker
Anoter common questions 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.