I wanted to check when signals a and b are high at the posedge of clk, in same edge signal c is high and reg1 = 17’hF.
After that in a few cycles, c should go low.
from that point in a few cycles reg2 goes 17’h0.
after that in few cycles reg2 goes 17’h1FFFF and so on.
I didnt have any syntax errors. But, one of my test cases where reg2 was forced to 1FFFF, there wasnt any assertion error.
Similarly, some other test cases where i forced value to deliberately fail assertion, they actually passed.
Any help would be appreciated.
// 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.
seq |-> expr1 ## [1:$] seq2 // is equivalent to
seq |-> expr1 ##1 seq2 or
expr1 ##2 seq2 or
...
expr1 ##n seq2; // n= $
// The difference between something like
##1 !c[->1]
##1 (reg2[17:1] == 17'h00000) [->1]
##1 (reg2[17:1] == 17'h1FFFF) [->1]
// and this
##[1:$] (!c)
##[1:$] (reg2[17:1] == 17'h00000)
##[1:$] (reg2[17:1] == 17'h1FFFF)
// is that with the goto operator, when
(!c) // occurs
// no other occurrences of !c is further tested.
// For example, the following 3 sequences are possibilities
##2 (!c)
##4 (reg2[17:1] == 17'h00000)
##6 (reg2[17:1] == 17'h1FFFF)
// or ..
##3 (!c)
##5 (reg2[17:1] == 17'h00000)
##6 (reg2[17:1] == 17'h1FFFF)
// In essence, the use of the goto operator it is equivalent to
first_match(##[1:$] (!c))
##0 first_match(##[1:$] (reg2[17:1] == 17'h00000))
##0 first_match(##[1:$] (reg2[17:1] == 17'h1FFFF))
/////////////////////
// Taking the path out, I would write it as
property example1;
disable iff (!(testmode))
@(posedge clk) (a && b) |-> (1, $display ("Checking SEQ1"))
##0 (c && (reg1[16:0] == 17'h0000F))
##1 !c[->1]
##1 (reg2[17:1] == 17'h00000) [->1]
##1 (reg2[17:1] == 17'h1FFFF) [->1]
##1 c[->1];
endproperty
// BTW, you have too many ()s. Use expr instead (expr)
// You may also want to use the "let" on the path. Thus,
let path=TB.TOP;
path.!c ##1 path.reg2
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
I didnt know about the strong concept. I will read more on that and try it.
// 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
Ok. Im a little confused here. I thought only infinite limit($) had that issue and I won’t be having this issue when Im using goto operator. I need to check more about goto operator.
even then, isnt “(c && (reg2[16:0] == 17’hF))” the expr1. So c low means expr1 is 0.
or is the (1,display(“”); the expr1?
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 |-> …
I might not have been clear.
There are possibilities for multiple matches where antecedent is true. a and b stays high for multiple clock cycles. maybe i should have used $rose instead.
Or do u mean antecednt can have a sequence with multiple events and then if we need first of those events, use first_match?
In short, I was looking for all of these events to happen in exact sequence( when a and b is high at a clock edge for the first time) and if even one of the steps doesnt happen or changes order, assertion should error out.
At every clocking event there is an attempt at the assertion, meaning that a new thread, independent from other threads, starts to evaluate the antecedent and consequent. Use the $rose unless you need to check the consequent for every clocking event when antecedent is true.
You’re correct, “(c && (reg2[16:0] == 17’hF))” is expr1; I misread it.
Or do u mean antecednt can have a sequence with multiple events and then if we need first of those events, use first_match?
when antecedent has “or”.
a ##[1:2] b is equivalent to
a ##1 b or a ##2 b.
C[*1:2] ##1 d is equivalent to
C [*1] ##1 d or C[*2] ##1 d