Wie schreibe ich Eigenschaft in System Verilog Assertions?

Question

Ich möchte eine Eigenschaft in SVA schreiben, um ein Verhalten formal zu verifizieren.

Hier ist, was ich will:

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    $fell(sig1) ##[1:$] first_match($fell(sig2)) ##0 sig3 |-> sig4 == sig3; 
endproperty 

Wie kann ich die obige Eigenschaft umschreiben, so dass nach sig1 fällt, bleibt es LOW während Auswertezyklen verbleibenden?

Anmerkung: Ich möchte nicht sig1 als disable iff (SIG1)

Dank setzen! Abschnitt

Answer 1

property prop1(sig1,sig2,sig3,sig4); 
    @(posedge clk) 
    (!sig1) throughout (##[1:$] first_match($fell(sig2)) ##0 sig3) 
      |-> sig4 == sig3; 
endproperty 

See 16.9.9 Bedingungen über Sequenzen in der 1800-2012 LRM