Stellt man sich sequentielle Schaltungen als endliche Automaten vor, die über die Größen Zustandsmenge, Startzustand, Eingabealphabet, Ausgabealphabet, Zustandsübergangsfunktion und Ausgabefunktion beschrieben werden können, so ist die Übereinstimmung dieser Größen eine hinreichende Bedingung für die Übereinstimmung der beiden Automaten. Für die im Rahmen der formalen Verifikation durchzuführende Prüfung auf funktionelle Gleichheit ist diese Übereinstimmung jedoch nicht erforderlich, da es durchaus strukturell unterschiedliche Implementierungen geben kann, die die gleiche Funktion aufweisen. Hier hilft das Konzept des Produktautomaten.
Die Zustände des Produktautomaten werden durch die Zustandspaare beider Automaten gebildet. Sie entstehen durch Verknüpfung der Ergebnismengen beider Einzelautomaten. Für die Verifikation müssen nur die Zustände verglichen werden, in denen die beiden Automaten zum gleichen Zeitpunkt verweilen können. Es müssen nicht alle möglichen Kombinationen von Zuständen berücksichtigt werden.
Das Eingabealphabet ist für beide Einzelautomaten identisch. Am Ausgang liefert der Produktautomat einen Binärwert, der angibt, ob die Ausgänge für einen gegebenen Eingangswert gleich oder verschieden sind.
Für die formale Verifikation zweier Automaten wird der entsprechende Produktautomat untersucht, auch wenn dieser nicht explizit aufgestellt wird. Liefert der Produktautomat für beliebige Eingangssequenzen einen wahren Ausgangswert, so stimmen die beiden Automaten funktionell überein.
Um alle möglichen Zustände der Automaten abzutasten, geht man vom Startzustand des Produktautomaten aus. Liefert dieser ein wahres Ausgangssignal, so werden alle Folgezustände des Startzustands berechnet, die in einem Schritt erreicht werden können. Für diese neu gewonnene Menge von Zuständen wird die Korrektheit des Ausgangssignals überprüft. Durch iterative Anwendung dieses Prinzips werden alle vom Startzustand erreichbaren Zustände untersucht. Das Verfahren verfolgt dabei das Prinzip der Breitensuche, um mögliche Unterschiede in einzelnen Ästen der erreichbaren Zustandsmenge möglichst schnell zu finden. Werden keine Unterschiede zwischen den Automaten festgestellt, so terminiert das Verfahren erst, wenn alle erreichbaren Zustände untersucht sind. Durch den mengenorientierten Ansatz muss jeder Zustand nur einmal untersucht werden. Wird der gleiche Zustand später nochmals erreicht, so ist dieser als schon untersucht markiert und muss nicht nochmals ausgewertet werden. Die Anzahl der zu untersuchenden Zustände des Produktautomaten wächst exponentiell mit der Anzahl der Zustände der Automaten. Aus diesem Grund ist das Verfahren auf bestimmte Systemgrössen und -klassen beschränkt.