Unexpected SVA Behauptung Verhalten für ein periodisches Signal

Question

aus einem Buch "SystemVerilog Assertions und Functional Coverage", Ashok Mehta auf Seite 42, Zitiert

@ (posedge clk) a | => a!; In der obigen Sequenz, lassen Sie uns sagen, dass die Variable 'a' ändert sich auf '1' zur gleichen Zeit , dass die Abtastrand Clock posedge clk geht (und davon ausgehen, 'a' war '0', bevor es ging auf eine '1'). Wird es eine Übereinstimmung des Antezedens "a" geben? Nein! Da ein 'von' 0 'zu' 1 'zur gleichen Zeit ging, zu der die Uhr gestellt wurde, ist der Wert von' a ', der durch den Takt abgetastet wird,' 0 '(vorgesetzte Region) und nicht' 1 '. Dies führt nicht dazu, dass die Eigenschaft ausgelöst wird, da der Vorgänger nicht als wahr bewertet wird. Dies verwirrt Sie beim Debuggen . Sie würden erwarten, dass "1" abgetastet wird und die Eigenschaft ausgelöst wird davon. Sie erhalten jedoch genau das Gegenteil. Dies ist ein sehr wichtiger Punkt zu verstehen, weil in einer Simulation Wellenform (oder für die Angelegenheit mit Verilog $ Monitor oder $ Strobe) Sie eine '1' auf 'a' mit posedge clk sehen und würde nicht verstehen, warum die Eigenschaft nicht feuern oder warum es fehlgeschlagen (oder bestanden für diese Angelegenheit). Denken Sie immer daran, dass an der Abtastkante der "vorherige" Wert (d. H. Ein Delta vor der Abtastkante in der vorbereiteten Region) von die abgetastete Variable verwendet wird.

Ich habe versucht, dieses Szenario von dieser Testbench zu testen. Allerdings erwartete ich Behauptung bei Simulationszeiten FAIL # 10, # 50, # 90

module assert_immediate(); 

     reg a,b,clk; 

     initial 
     begin 
     clk = 0; 
     forever #10 clk = !clk; 
     end 

     initial 
     begin 
     a = 0; 
     b = 0; 
     repeat (10) @(posedge clk) a = ~a; 
     end 

    // always@(posedge clk) $display("a = %d at time %t \n", a, $time); 

     property p1; 
     @(posedge clk) a |=> !a; 
     endproperty 

     initial #100 $finish; 

     assert property (p1) $display("Entered assert at %t \n", $time); else $display("FAIL at %t \n", $time); 
     cover property (p1) $display("PASS at %t \n", $time); 

endmodule 

Aber wenn ich auf EDAPlayground lief VCS, bekam ich ein anderes Verhalten

# KERNEL: Entered assert at     10 
# KERNEL: 
# KERNEL: PASS at        10 
# KERNEL: 
# KERNEL: Entered assert at     50 
# KERNEL: 
# KERNEL: Entered assert at     50 
# KERNEL: 
# KERNEL: PASS at        50 
# KERNEL: 
# KERNEL: PASS at        50 
# KERNEL: 
# KERNEL: Entered assert at     90 
# KERNEL: 
# KERNEL: Entered assert at     90 
# KERNEL: 
# KERNEL: PASS at        90 
# KERNEL: 
# KERNEL: PASS at        90 

Answer 1

Ich denke, dass es 2 Probleme gibt.

1. Ich denke, dass es im Implikationsoperator ein Missverständnis gibt. Assertion sollte in Ihrem Fall nicht fehlschlagen. Die Implikation lässt zu, dass der Ausdruck auf der rechten Seite letztendlich wahr ist. Also, wenn a geht, wird es schließlich sinken. Also bei # 50 geht es nach dem Abtasten hoch bei # 30 nach unten, und dies bewirkt, dass die Behauptung durchgeht und zum nächsten Evaluierungszyklus geht: # 70 -> # 90.

Für jede erfolgreiche Spiel der vorgängigen sequence_expr, die daraus folgende property_expr isseparately ausgewertet. Der Endpunkt der Übereinstimmung des Antezedens sequence_expr ist der Startpunkt der Auswertung des nachfolgenden property_expr.

2. Es gibt einen Fehler im Compiler, den Sie verwenden. Es sollte keine Zusicherungsnachricht zum Zeitpunkt # 10 geben. Ich habe es mit VCS 2017.03 versucht und es hat richtig funktioniert.

auch können Sie diese Zeile Sie Code hinzufügen, um einige Debug-Drucke zu erhalten:

always @(posedge clk) $display("%0t a = %b", $time, $sampled(a)); 

Ich habe diese Ergebnisse bei der Simulation:

10 a = 0 
30 a = 1 
50 a = 0 
Entered assert at 50 
PASS at   50 
70 a = 1 
90 a = 0 
Entered assert at 90 
PASS at   90 

Answer 2

Warum Sie erwarten, dass Ihr Behauptung zu versagen? Sie haben Ihre Testbench angewiesen, a alle posedge im initial Block zu ändern, damit Ihre Assertion bestanden wird (Sie werden eine Sequenz von a, !a, a, !a haben), so erwarte ich 2 Assertion Pässe.

Was ich nicht verstehe, ist, dass die Behauptung @ Zeit 10 gemäß Ihrem Protokoll übergibt. Ihre ersten posedge ist @ time 10, so der abgetastete Wert von a ist 0 (weil Probenahme vor den posedge und Ihr Anfangswert von a getan wird, ist 0 zum initial Block Accroding). Dieser Wert von a würde die Assertion nicht auslösen (entspricht nicht dem Assertion-Vorgänger, d.h. der linken Seite der Assertion).