SV assertion for verifying a sequence of events not working

In reply to Adarsh24:

In reply to ben@SystemVerilog.us:
Looks like its not working. I tried with goto operator just as you mentioned.
I tried forcing reg2 with 17’h1FFFF throughout the testmode high. Didnt fail, even though i had check for 17’h00000.
REG2 17’h1FFFF


// Looked at the waveforms   
@(posedge clk) (a && b) |-> (1, $display ("Checking SEQ1"))
            ##0 (c && (reg1[16:0] == 17'h0000F)) 
            ##1  !c[->1] // <**** you got to here 
            // The next occurrence of (reg2[17:1] == 17'h00000) never happened 
            // reg2== FFFF, thus simulator is waiting for 
            // (reg2[17:1] == 17'h00000) [->1]
            // Simulator is stuck in active mode, no failure at end of sim
            // unless you qualify the consequent as "strong"
            ##1  (reg2[17:1] == 17'h00000) [->1]
            ##1  (reg2[17:1] == 17'h1FFFF) [->1]
            ##1  c[->1];

Also, tried making c low when antecedent true. Didnt error out.
c low when antecedent true
But, it did error out when reg1 was 17’h0 instead of 17’hF.
reg1 17’h0

// did you READ MY PREVIUS COMMENT?
// An assertion of the form
// seq |-> expr1 ## [1:$] seq2
// can only fail if expr1 is false. <<<**********
// If expr1==1 then there are an infinite number of possibilities
// for seq2 to be true

i tried using first match for antecednt as below. But, it didnt help my case.

    @(posedge clk) first_match(a && b) |-> (1, $display ("Checking SEQ1"))

[/quote]
You’re throwing the kitchen sink!
An antecedent with a single possible match need not a first_match.
a first_match is needed when there are multiple possible matches, like in
a ##[1:$] b |-> …
Ben