Ich bin ein Assertion Verification Newbie versucht zu lernen, wie es richtig gemacht werden soll. Ich habe eine Menge Informationen über die Struktur und die technischen Details der Systemverilog + Behauptungen gefunden, aber ich habe immer noch keine Art von "Kochbuch" -Material gefunden, wie Dinge wirklich in der realen Welt gemacht werden.SVA Annahme/Behauptungen für kontinuierliche Dateneingabe
Die Frage und Abhängigkeiten:
- Entwurf hat einen Dateneingangsbus mit Daten gültig und ID Eingänge
- One Daten "Paket" ist 3 Proben
- nach Kanal n gibt es immer Daten von Kanal n + 1
- Kanal-IDs werden wickelt, nachdem die größte ID ein beliebige Anzahl von clk zwischen Datenbytes ist Zecken sein kann
- Es geschickt wurde
Folgendes ein einfacher und hoffentlich korrekt mit Kanal-IDs Zeitdiagramm:
So wie tun Sie dies mit mindestens ammount von Code? Schön und sauber. Zuvor habe ich Dummy-Verilog-Module gebaut, um die Daten zu fahren. Aber sicherlich könnte man einfach die Eigenschaft verwenden, um nur die Kanal-IDs zu beschränken, aber ansonsten die Hände frei lassen für das formale Werkzeug, um zu versuchen, mein Design zu bremsen?
Einfache Vorlage für den Anfang könnte sein:
data_in : assume property (
<data with some ID>[=3]
|=>
<data with the next id after any clk tick>
);
Ich denke, das Problem ist, dass davon ausgegangen/Behauptungen wie oben neigen dazu, auf jeder Datenprobe auslösen und parallele Threads erzeugen, die sich zeitlich überlappen.
@MatthewTaylor Das OP spricht über formale Verifikation. Die Terminologie bei der formalen Verifikation besteht darin, dass Sie Annahmen über Ihren Input-Stimulus machen und diese seinen gesetzlichen Statusraum einschränken. –
@Tudor Oh - so ist es. Das habe ich vermisst. –