• Sie befinden sich hier:
  • Wissen »
  • Blog »
  • Simulation im Vergleich zu Formal Verification
Blog

Simulation im Vergleich zu Formal Verification

  • 30. August 2021

Mit der zunehmenden Komplexität der Chips ist die Überprüfung der Design Correctness zu einer anspruchsvolleren Aufgabe geworden.

Laut der Studie der Wilson Research Group 2020 übersteigt die Zeit, die selbst für FPGA Designer für die Verifizierung aufgewendet wird, tatsächlich die Zeit, die in der Designphase benötigt wird.

Dies bedeutet, dass die Simulation nicht ausreicht, um Design Correctness zu testen, und das leistungsfähigere Techniken erforderlich sind, um Corner Case Fehler schneller zu finden. Die nächste Stufe ist dann die Formale Verification.

Aber was bedeutet Formal eigentlich?

Um zu verstehen, was Formal macht, schauen wir uns zuerst an, wie der Simulationsprozess funktioniert. In RTL erstellen Simulationsingenieure Testbenches, die das DUT stimulieren. Testbenches verwenden normalerweise eingeschränkte, zufallsbedingte oder gezielte Tests um Vektoren zu generieren, die Fehler entweder aufdecken oder auch nicht.

Der Nachteil der Simulation ist, dass es Zeit braucht und nicht den gesamten Zustandsraum abdecken kann. Einige Testvektoren können die erwartete Funktionalität testen und wieder andere können Fehler entdecken. Um jedoch den gesamten Zustandsraum zu untersuchen, ist eine große Anzahl von Tests erforderlich, da sonst einige Fehler übersehen werden könnten. Aber das dauert wesentlich zu lange und ist durch Simulation unrealistisch.

Nachdem wir das gesagt haben, kehren wir zum Konzept der formalen Verifikation zurück, einer mathematischen und algorithmischen Lösung, die entwickelt wurde, um den gesamten Zustandsraum zu untersuchen. Im Gegensatz zur Simulation, die die Designfunktionalität testet, beweist Formal, dass die Implementierung die Anforderungen erfüllt. Bei Formal ist keine Testbench erforderlich, stattdessen können die Verifikationsingenieure Einschränkungen und Annahmen verwenden, um den Analyseumfang einzuschränken. Der Zustandsraum erweitert sich geometrisch, Zyklus um Zyklus, ausgehend von einem Anfangszustand und untersucht alle möglichen Zustände, was Formal zu einer erschöpfenden Lösung macht. Wenn irreguläre States erreicht werden können, wird ein Fehler gefunden. Andernfalls haben wir einen Beweis für die beabsichtigte Funktionalität.

Simulation und formale Verifikation sollten komplementär eingesetzt werden, um die Korrektheit des Designs zu gewährleisten und den Zeitaufwand für den Verifikationsprozess zu reduzieren.

Besuchen Sie die Verification Academy um mehr über die Miniwelt der formalen Lösungen von Siemens EDA zu erfahren