Wie schreibe ich eine Eigenschaft für die formale Verifikation?

property prop1; 
@(posedge clk) 
$fell(sig1) ##1 sequence1 |-> sequence2; 
endproperty

Ich möchte die Eigenschaft deaktivieren, wenn sig1 = 1'b1 nach dem ersten Taktzyklus.Wie schreibe ich eine Eigenschaft für die formale Verifikation?

Übergang von hoch zu niedrig auf sig1 ist meine auslösende Bedingung. Wenn ich deaktiviere, wird iff (sig1) auslösende Bedingung nicht erfüllt werden.

Auch die Verwendung von "durchgehend" ist nicht möglich, sowohl für die Aktivierung als auch für die Erfüllung von Sequenzen in formalen Verifikatoren.

Wie kann ich es tun? Danke!

Quelle

2016-05-12 kkdev

Bitte seien Sie ausführlich. Warum können Sie nicht 'disable iff (sig1);'? – sharvil111

Übergang von hoch zu niedrig auf sig1 ist meine auslösende Bedingung. Wenn ich deaktiviere, wird iff (sig1) auslösende Bedingung nicht erfüllt werden. – kkdev

Aktualisiert. Nur eine Randnotiz. Können Sie den nichtüberlappenden Operator (| =>) so verwenden, dass nur dann, wenn $ fell (sig1) TRUE ergibt, nur sequenz1 ausgewertet wird? Wie: $ $ fell (sig1) | => sequenz1 | -> sequenz2; ' – sharvil111

Wie wäre es einige Satelliten-Code zu schreiben eine verzögerte Version von sig abzuleiten: kann

always @(posedge clk) sig1d <= sig1; property prop1; @(posedge clk) disable iff(sig1d) $fell(sig1) ##1 sequence1 |-> sequence2; endproperty

http://www.edaplayground.com/x/2tbX

Quelle

2016-05-12 12:33:02

Wenn ich nicht falsch liege, verzögert es immer noch die Deaktivierung, wenn um einen Taktzyklus von dem, was ich tun möchte. – kkdev

Aber beachten Sie, ich habe immer noch '$ fiel (sig1)' NOT '$ fiel (sig1d)'. Sicher, wenn Sie es deaktivieren wollten, selbst wenn "sig1" im ersten Taktzyklus hoch wäre, dann wäre '$ fell (sig1)' niemals wahr? Vielleicht brauchen wir ein Timing-Diagramm? (Oder ändern Sie meinen Code, um einen zu erzeugen?) –

@MatthewTaylor Sie müssen mit der Tatsache vorsichtig sein, dass der 'disable' Ausdruck asynchron abgetastet wird und zu Wettlaufbedingungen führen kann. Sie sollten 'disable iff ($ samples (sig1d))' verwenden. –

Sie neu schreiben, um nur Trigger Ihre Behauptung, wenn Sie hohe sehen nicht sig1 nach dem ersten Zyklus:

property prop1; 
    @(posedge clk) disable iff(sig1d) 
    $fell(sig1) ##1 !sig1 ##0 sequence1 |-> sequence2; 
endproperty

Quelle

2016-05-13 18:10:36

Ich habe das schon probiert. Das Problem ist, ich kann es nicht auf sequenz2 tun. Zum Beispiel: $ fiel (sig1) ## 1! Sig1 durchgehend (sequenz1) | -> sequenz2; Aber ich kann nicht durchgehend auf sequenz2 setzen (formale Werkzeuge erlauben das nicht). Also dachte ich, der beste Fall wäre, die Eigenschaft auf sig1 nach einem Zyklus zu deaktivieren. Alle anderen Vorschläge sind sehr willkommen. – kkdev

@ kkdev Von dem, was ich erhalte, sollten Sie Ihre Frage umformulieren, weil sie mehrdeutig ist. Sie möchten nicht, dass die Eigenschaft deaktiviert wird, wenn das "sig1" nach dem ersten Zyklus hoch wird (was als Zyklus nach den ersten Zyklen verstanden werden kann). Sie möchten es deaktivieren, wenn 'sig1' in jedem nachfolgenden Zyklus hoch wird. Sie sollten versuchen, die Antwort von @ Mathew Taylor zu verwenden, da dies der einzige Weg ist. –

Wie schreibe ich eine Eigenschaft für die formale Verifikation?

Antwort

Verwandte Themen