Ein neuer Ansatz zur sequentiellen Verifikation von Entwürfen auf verschiedenen Abstraktionsebenen durch symbolische Simulation wird vorgestellt. Das automatische formale Verifikationswerkzeug wurde dazu verwendet, die Äquivalenz von strukturellen Beschreibungen auf Registertransferebene und den entsprechenden Verhaltensspezifikationen nachzuweisen. Die Ergebnisse eines kommerziellen Synthesewerkzeugs auf Gatterebene konnten mit Verhaltens- bzw. Strukturbeschreibungen auf Registertransferebene verglichen werden. Es ist nicht erforderlich, daß die Spezifikation synthetisierbar oder taktäquivalent zur Implementierung ist. Ferner wird eine Anwendungsmöglichkeit der Methode zur Eigenschaftsverifikation vorgeschlagen. Die symbolische Simulation wird entlang logisch konsistenter Pfade in den Beschreibungen durchgeführt. Eine erweiterbare Bibliothek verschiedener Techniken zur Äquivalenzerkennung erlaubt es, einen günstigen Kompromiß zwischen Genauigkeit und Geschwindigkeit zu erzielen. Auf Entscheidungsdiagrammen (OBDD) basierende Methoden erkennen seltene Fälle der Äquivalenz symbolischer Terme. Durch Einbeziehung der Resultate der anderen Techniken zur Äquivalenzerkennung gelingt es, die Größe der Graphen zu kontrollieren. Außerdem bilden die Entscheidungsdiagramme lediglich kleine Ausschnitte des Verifikationsproblems ab. Die Kooperation aller Techniken und eine effiziente Unterstützung der Fehleranalyse werden ermöglicht, indem Erkenntnisse über Termbeziehungen an Äquivalenzklassen vermerkt werden, anstatt die symbolischen Terme selbst zu manipulieren.