Statt ein Erfüllbarkeitsproblem zu untersuchen, kann man beim Equivalence Checking versuchen, die beiden Systeme direkt miteinander zu vergleichen. Dazu bildet man die Systeme jeweils auf einen Graphen ab und versucht, die Isomorphie der beiden Graphen zu beweisen. Damit dies möglich ist (das generelle Graphenisomorphieproblem ist NP-vollständig), muss eine eindeutige (kanonische) Darstellung gefunden werden. Diese ist durch so genannte binäre Entscheidungsgraphen Binary Decision Diagrams (BDDs) gegeben.