Stimulus problem

SystemVerilog
1

Hi All,
I have a signal A and B. Now, I want B cannot be asserted until signal A asserted. If I don’t want use until_with or other support logic.is it possible to create assumption in fpv?
thanks

2

Would something like this work?

//  B cannot be asserted until signal A asserted. 
  assume property(@posedge clk) 
         A[->1] ##1 1[*0:$] intersect B[->1]);
// Option , edited the !B to !A
assume property(@posedge clk) 
 A[->1] ##1 !A[*0:$] intersect B[->1]);
1 Like
3

thanks for reply.
By the way, the stimulus should be after reset desserted, B cannot be asserted until signal A asserted .
do you think I need add other reset constraint into the assumption in fpv?
Thank you

4

Yes on the rstn (active low

initial assume property(@posedge clk) 
         rstn==1[->1] ##0 A[->1] ##1 1[*0:$] 
                                                   intersect B[->1]);
5

Hi Ben,
Why need adding ##1 1[*0:$]?
is it correct using rst_n ==1[->1] ##0 A[->1] intersect B[->1]?
Thank you!

6 
/* Q: Why need adding ##1 1[*0:$]?
is it correct using rst_n ==1[->1] ##0 (A[->1] intersect B[->1]? */
[Ben] What if B occurs many cycles after A? 
That is whay you do need the  ##1 1[*0:$] ; you need to find a thread if B occurs after A
      rstn  0 0 0   1 1 1 1 1 1 1 1 1 1  1 1 1 1  
     A       x x x x  0 0 1 0 1 1 0 1 
     B       x x x x  0 0 0 0 0 0  1 
                    <--------------->
Note the () after the rstn[->1]
         rstn==1[->1] ##0 (A[->1] ##1 1[*0:$] 
                                                   intersect B[->1]) );
7

Hi Ben,

I am still not able to understand meaning of 1[*0:$].
It says 1 repeats somewhere between 0 to unlimited number of clock cycles. What is the LHS of the intersect operation : A[->1] ##1 1[*0:$] or just 1[*0:$] ?

8 
initital am_AB: assume property(@(posedge clk)
         rstn==1[->1] ##0 (A[->1] ##1 1[*0:$] 
               intersect B[->1]) );
cycle  0123456789ABC
rstn   000011111111111111111111111111
A      0000000010000000000000000000
A[->1])    <--->
B      00000000000010000000000000
B[->1])    <------->
If you don't haVE THE 1[*0:$] THEN 
 (A[->1]   intersect B[->1]) 
A[->1] ends at cycle 8
B[->1] ends at cycle C
thus, the intersect is a NO MATCH
But, with the1[*0:$], you are providing a choice of other threads,  and 
 (A[->1] ##1 1[*0:$] intersect B[->1]) DO MATCH at cycle C.
9

Hi Ben

What is difference between A[->1] ##1 1[*0:$] and  A[->1] ##[*0:$] ?
10

Thank you Ben, this example made things clear.