Formal Verification
Lieferung umfassender Ergebnisse bei gleichzeitiger erheblicher Reduktion des Risikos
Formal Verification tools
Die Tools für die formale Verifikation von Siemens sind mit Simulation und Emulation integriert und verfügen über gemeinsame Funktionen wie Verifikationsmanagement, Compiler, Debugger und Sprachunterstützung für SystemVerilog, Verilog, VHDL, UPF und andere.
Sie ermöglichen Lösungen, die den Verifikationsprozess und die Verifikationsziele von den zugrunde liegenden Engines abstrahieren.
Formal Verification vs Simulation
Was ist der Unterschied zwischen formaler Verifikation und funktionaler Simulation?
Die formale Verifikation ist eine andere Art der Verifikation, verfolgt aber das gleiche Ziel: die Beseitigung von Fehlern im Entwurf. Einer der großen Unterschiede zwischen formaler und funktionaler Verifikation ist die Rolle, die das Werkzeug spielt. Bei der formalen Verifizierung wird die Korrektheit des Hardware- oder Softwareverhaltens durch statische Analyse auf der Grundlage mathematischer Transformationen ermittelt, im Gegensatz zu dynamischen Verifizierungstechniken wie der Simulation.
Bei der Simulation werden Testfälle (Szenarien) manuell oder mit einer automatisierten Testbench erstellt und dann auf dem RTL- oder Gate-Level-Design ausgeführt. Angesichts der riesigen Anzahl von Zuständen selbst in einem kleinen Design ist es unmöglich, mehr als einen kleinen Prozentsatz des Verhaltens des Designs zu simulieren. Die Simulation ist probabilistisch; die Wahrscheinlichkeit, dass ein Szenario ausgeführt wird, das einen Designfehler aufdeckt, ist gering. Bei der formalen Verifikation wird der Entwurf nicht ausgeführt, so dass keine Tests oder Testumgebungen erforderlich sind. Stattdessen wird der Entwurf statisch für alle möglichen Eingabesequenzen und alle möglichen Zustandswerte analysiert, um zu prüfen, ob irgendwelche Assertions verletzt werden können. Aus theoretischer Sicht ist die formale Verifikation hundertprozentig erschöpfend und beweist, dass alle Assertions "sicher" sind, sobald alle Fehler gefunden und behoben wurden.
Software for Formal Verification
Questa AutoCheck
Questa AutoCheck ist eine vollautomatische App zur formalen Fehlersuche. Es hilft Ihnen, Fehler aufgrund von häufigen RTL-Codierungsfehlern frühzeitig in Ihrem Design zu finden.
Questa CDC
Questa CDC von Siemens identifiziert Fehler mithilfe einer Strukturanalyse, um Taktdomänen, Synchronisierer und Strukturen mit geringem Stromverbrauch zu erkennen.
Sie wünschen mehr Informationen?
Do you want to receive more information?
Fragen Sie einen Formal Verification Experten:
Kontaktieren Sie uns und wir beantworten Ihre Fragen so schnell wie möglich.