Die Grundaufgabe des Equivalence-Checking besteht darin, zwei boolesche Funktionen auf funktionelle Gleichheit zu überprüfen. Beim expliziten Ansatz betrachtet man die Verknüpfung beider Funktionen. Die beiden Ausgangssignale müssen für beliebige Eingangskombinationen stets gleich sein. Ist dies erfüllt, so sind die beiden Funktionen funktionell identisch. Dies ist im Bild durch die Verknüpfung von und über ein Äquivalenzgatter dargestellt.
Ein geeignetes Verifikationsverfahren ergibt sich aus der Idee des Widerspruchsbeweises. Nehmen wir an, die beiden Funktionen seien nicht identisch. Dann muss es eine Eingangskombination geben, für die am Ausgang des Äquivalenzgatters eine logische 0 auftritt. Umgekehrt gilt, dass, wenn es unter der Annahme eines solchen Wertes gelingt, eine gültige Eingangskombination zu finden, die Schaltungen offenbar nicht identisch sind. Gelingt es nicht, eine solche Kombination zu finden, sind die beiden Funktionen identisch. Diese Fragestellung führt unmittelbar auf das sogenannte Erfüllbarkeitsproblem.