Wenn Sie ein full_case Synthese-Attribut auf einen Case-Statement-Header anwenden, weist es Tools an, nicht näher spezifizierte Zustände als Werte "egal" zu interpretieren. Die Quartus® II Software leitet zusätzliche Logik ab, um die "Don't Care"-Zustände darzustellen. Diese zusätzliche Logik kann sich von der vom formalen Verifizierungstool abgeleiteten Logik unterscheiden, was zu einer Diskrepanz bei der formalen Verifizierung führt.
Um das Missverhältnis zu überwinden, definieren Sie alle Zustände in der Zustandsmaschine.
Weitere Informationen zu den Richtlinien für die Zustandskodierung von Maschinen finden Sie im Kapitel Empfohlene HDL-Codierungsstile (PDF) in Teil 1 des Quartus II Handbuchs.