Die wesentlichen heute gebräuchlichen formalen Verifikations-Werkzeuge können in zwei Gruppen eingeteilt werden:
Equivalence-Checker:
Diese Verfahren weisen die vollständige funktionale Übereinstimmung zwischen zwei unterschiedlichen Implementierungen nach. Eingesetzt wird Equivalence- Checking z.B. um das funktionelle Modell einer Schaltung mit der Gatternetzliste zu vergleichen und somit die Korrektheit des Synthese-Schritts im Entwurfsablauf einer integrierten Schaltung formal zu beweisen. Zeitraubende Simulationen der Gatternetzliste werden damit eingespart.
Die Verfahren des Equivalence-Checkings sind weit entwickelt. Für kombinatorische Systemteile lassen sich diese Verfahren sehr einfach und effizient einsetzen.
Model-Checker:
Model-Checker überprüfen einzelne Eigenschaften einer Schaltungsbeschreibung. Es kann beispielsweise zu überprüfen sein, ob eine Schaltung nach einer gewissen Zeit immer wieder in ihren Ruhezustand zurückkehrt. Die Schwierigkeit besteht darin, die zu überprüfenden Eigenschaften der Schaltung in der Eingabesprache für den Model-Checker zu beschreiben.
Generell gilt für Verfahren der formalen Verifikation, dass sie für den Anwender, den Schaltungsentwickler, schwerer zugänglich und ungewohnter sind als Simulatoren. Die notwendige Formalisierung der Eingaben stellt neue Anforderungen an den Design-Prozess und damit an den Entwickler. Auch die Ausgaben der formalen Verifikationswerkzeuge sind nicht immer leicht verständlich.
Die Grundidee des Modell-Checking ist eine Erreichbarkeitsanalyse im Zustandsraum. Damit liegt das Hauptproblem der formalen Verifikationsverfahren in der so genannten Zustandsexplosion (State Explosion). Um einen Beweis durchführen zu können, muss unter Umständen der gesamte Zustandsraum eines Systems untersucht werden. Die Zahl der zu untersuchenden Zustände steigt exponentiell mit der Anzahl der Zustandsraumdimensionen an. Die Speicher- und Laufzeitkomplexität solcher Verfahren sind damit exponentiell in den Dimensionen des Zustandsraumes. Die exponentielle Komplexität stellt de facto eine obere Grenze für die behandelbaren Systemgrößen dar. Allerdings konnte durch verschiedene Optimierungen die Einsetzbarkeit der Verfahren erheblich gesteigert werden, so dass heute große digitale Blöcke handhabbar sind.