Was sind Yosys formale Fähigkeiten mit Verific?

Question

Ich versuche, Yosys formale Verifikationsfunktionen zusammen mit Verific Parser zu verwenden.

Was sind die unterstützten Funktionen von yosys mit Verific für die formale Verifikation im Vergleich zum Befehl "read_verilog-formal"? Zum Beispiel kann eine schnelle Erstellung von formalen Code, der mit read_verilog arbeitet gab mir einen Fehler für „annehmen Eigenschaft“ Syntax: „Die SVA-Richtlinie ist es, eine Uhr nicht empfindlich Unclocked Richtlinien werden nicht unterstützt.“

Ich bin Ich bin mir nicht sicher, ob ich die Flags für die Verific-Bibliothek in irgendeiner Weise modifizieren sollte, um mehr Funktionen zu unterstützen, oder etwas, das nicht unterstützt wird.

Answer 1

Derzeit hat Yosys nur sehr eingeschränkte Unterstützung für SVA mit oder ohne Verific. Wir planen jedoch, die Yosys-Unterstützung für SVA in naher Zukunft über Verific erheblich zu erweitern. Das Ziel ist, nahezu vollständige Unterstützung für alles bereitzustellen, was Verific analysieren kann.

In Bezug auf die "Die sva-Richtlinie ist nicht empfindlich auf eine Uhr. Unclocked Direktiven werden nicht unterstützt" Fehlermeldung: Das ist eine Verific-Fehlermeldung und ich glaube nicht, es gibt eine Verific-Bibliothek Flag um es zu umgehen. (Aber ich bin mir nicht sicher.) Technisch nicht getaktete Eigenschaften sind nicht Teil des SystemVerilog-Standards afaik. (Die Syntax würde dies erlauben, aber der Standardtext definiert keine Semantik dafür.)

Yosys unterstützt nicht getaktete SVA-Eigenschaften. (Aber nur triviale Expressionseigenschaften.)

Sowohl Verific als auch Yosys unterstützen unmittelbare Behauptungen und Annahmen. (Das sind Behauptungen und Annahmen in immer Blöcken.) Gerade jetzt ist das die Sache, die ich für die meisten Fälle empfehle, wo Leute neue Eigenschaften schreiben, auch weil die meisten Simulatoren bessere Unterstützung für unmittelbare Behauptungen haben (oder es wäre leichter hinzuzufügen, wenn der Support ist soweit fehlt).

Im Moment würde ich sagen, der größte Vorteil der Verwendung von Verific mit Yosys ist die Unterstützung für Nicht-SVA System Verilog (und VHDL) Code. In einigen Monaten werden wir hoffentlich Unterstützung für viel mehr SVA-Konstrukte über Verific bekommen, aber das ist noch nicht implementiert.

Bearbeiten/Aktualisieren: SVA Unterstützung über Verific ist langsam Verbesserung jetzt. Beispiele, die über Verific verarbeitet werden können, finden Sie unter this directory. Neue Beispiele werden hinzugefügt, wenn den Verific-Bindungen neue Funktionen hinzugefügt werden. Derzeit ist counter.sv das am weitesten fortgeschrittene Beispiel dort.