Assertion Check

SystemVerilog
, ,
11

In reply to ben@SystemVerilog.us:

Hi Ben,

Thank you for reply. let me tell my requirement. I have basically two reequipment. one is for fll_lock assertion and second is for fll_lock deassertion.

1st requirement (fll_lock_assertion):- FLL LOCK is asserted on detecting two positive edges of FLL INC or FLL DEC only when (fll_sar_eoc == 1). and two positive edge of fll_inc or fll_dec ([b]consecutive is not necessary ) between 1 to 6 clock cycle of sampled_clk[/b]

property p_lock_condition_check_unlock_prog_00;

        int inc_count, dec_count;
 @(posedge sampled_monclk) disable iff (!i_en_fll)
  ( ( o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |=> 
            (##1 (1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec)))[*1:6] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
    endproperty

2nd requirement (fll_lock de assertion ) :- FLL lock is de-asserted on detecting of four consecutive of o_fll_inc signal or fll_dec signal. here the.
Note :- 1. for requirement two : positive edge is not needed but consecutive of fll_dec or
fll_inc is must. 1 to 6 clock cycle is [b]not required[/b].

property p_unlock_condition_check_unlock_prog_00; 
        int inc_count, dec_count;
 @(posedge sampled_monclk) disable iff (!i_en_fll)
   ( $rose (o_fll_lock) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |-> 
            ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0 
            !o_fll_lock==(inc_count==4 || dec_count==4) 
     ##0 !o_fll_lock[->1]; // if needed

I have added the waveform for lock assertion and de- assertion :

12

In reply to rkg_:
See if the following works. Make sure you use the |-> ##1 (consequent)[*n] and NOT the
|-> (##1 consequent)[*n]


module m; 
    bit[1:0] o_fll_sar_eoc, i_fll_unlock_prog;
    bit o_fll_inc, o_fll_lock, sampled_monclk, i_en_fll, fll_dec; 
// 1st requirement (fll_lock_assertion):- FLL LOCK is asserted on detecting two positive edges 
// of FLL INC or FLL DEC only when (fll_sar_eoc == 1). 
// and two positive edge of fll_inc or fll_dec (**consecutive is not necessary ) 
//between 1 to 6 clock cycle of sampled_clk**

property p_lock_condition_check_unlock_prog_00; // Using |-> ##1 (consequent)
    int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |-> 
            ##1 (1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
endproperty

property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
    int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |=> 
            (1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
//---------------------------------------
//2nd requirement (fll_lock de assertion ) :- FLL lock is de-asserted on detecting of four consecutive 
// of o_fll_inc signal or fll_dec signal. here the.
// Note :- 1. for requirement two : positive edge is not needed but consecutive of fll_dec or
// fll_inc is must. 1 to 6 clock cycle is **not required**.

property p_unlock_condition_check_unlock_prog_00_v1; // NOT per requirements
  int inc_count, dec_count;
  @(posedge sampled_monclk) disable iff (!i_en_fll)
  ($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0) |-> 
            ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0 
            // does not satisfy "consecutive of fll_dec or fll_inc is must"
            !o_fll_lock==(inc_count==4 || dec_count==4) 
     ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty 

// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then 
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of 
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00_v2; //One option
    // int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
    ($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00)  |-> 
       first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4]) ##0  !o_fll_lock;
         // ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0 
              // does not satisfy "consecutive of fll_dec or fll_inc is must"
              // !o_fll_lock==(inc_count==4 || dec_count==4) 
              // ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
endproperty 

// If the "at anytime" is constrained to "n" static cycles, 
let n=10; 
// Upon a rose of 0_fll_lock and i_fll_unlock_prog == 2'b00 then 
// at anytime thereafter (the ##[1:$]) any 4 sequential occurrence of 
// o_fll_inc or 4 sequential occurrence of fll_dec the o_fll_lock==0 at that 4th occurrence
property p_unlock_condition_check_unlock_prog_00; //One option
    // int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
    ($rose (o_fll_lock) && i_fll_unlock_prog == 2'b00)  |-> 
       first_match(##[1:$] (o_fll_inc==1)[*4] or (fll_dec==1)[*4] intersect 1'b1[*n]) ##0  !o_fll_lock;
         // ##1 (1, inc_count+= (o_fll_inc==1),dec_count+= (fll_dec==1))[*6] ##0 
              // does not satisfy "consecutive of fll_dec or fll_inc is must"
              // !o_fll_lock==(inc_count==4 || dec_count==4) 
              // ##0 !o_fll_lock[->1]; // This !o_fll_lock occurs at any time later
  endproperty 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
13

In reply to ben@SystemVerilog.us:

An option for your 1st property using the Non-consecutive repetition, Boolean([=n]

property p_lock_condition_check_unlock_prog_00_Voption; // Using |-> ##1 (consequent)
    //int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00)   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:6])
            ##0 o_fll_lock;
endproperty
14

In reply to ben@SystemVerilog.us:

In reply to ben@SystemVerilog.us:
An option for your 1st property using the Non-consecutive repetition, Boolean([=n]

property p_lock_condition_check_unlock_prog_00_Voption; // Using |-> ##1 (consequent)
//int inc_count, dec_count;
@(posedge sampled_monclk) disable iff (!i_en_fll)
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00)   |-> 
##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:6])
##0 o_fll_lock;
endproperty

Hi Ben

Thank you for all your suggestion. and “p_lock_condition_check_unlock_prog_00_Voption” is not working. But others are working well.

15

In reply to rkg_:
The following test model worked OK for me


ap_a2b2c: assert property(@ (posedge clk) 
       $rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));

1539×836 117 KB

http://systemverilog.us/vf/twoabc.sv

1539×836 117 KB

//code


module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"     import uvm_pkg::*;
    bit clk, a, b, c, reset_n;
    default clocking @(posedge clk);
    endclocking
    initial forever #10 clk = !clk;
    
    ap_a2b2c: assert property(@ (posedge clk) 
       $rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));  

    initial begin
      repeat (200) begin
        @(posedge clk);
        if (!randomize(a, b, c) with {
          a dist {1'b1 := 1, 1'b0 := 3};
          b dist {1'b1 := 1, 1'b0 := 2};
          c dist {1'b1 := 1, 1'b0 := 2};
        })
          `uvm_error("MYERR", "This is a randomize error");
      end
      $finish;
    end
  endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
16

In reply to ben@SystemVerilog.us:

Hi Ben,

property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
    int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |=> 
            (1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
endproperty

This assertion is failing even after lock is asserted ( just after 6 posedge of sampled_monclk after lock assertion ). Do we need to put some extra logic so that one lock is asserted it should not check until the next packet will come ?

17

In reply to rkg_:
After every successful antecedent, a new thread is fired, and that thread is independent of any other previously fired thread. That can cause errors if you want to check the packets independently. Below is a simulatable example where I used the block.


/*property p_lock_condition_check_unlock_prog_00_v0; // OK too, using the |=> (consequent)
    int inc_count, dec_count;
    @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |=> 
            (1, inc_count+= $rose(o_fll_inc), dec_count+= $rose(fll_dec))[*1:6] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
endproperty
This assertion is failing even after lock is asserted ( just after 6 posedge of sampled_monclk after lock assertion ). 
Do we need to put some extra logic so that one lock is asserted it should not check until the next packet will come ? */ 
module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"     import uvm_pkg::*;
    bit clk, a, b, c, reset_n, block; 
    initial forever #10 clk = !clk;
    
    function void set_block(bit x);
        block=x;        
    endfunction

    ap_a2b2c: assert property(@ (posedge clk) 
       $rose(a) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6]));  

    ap_a2b2cBLOCK: assert property(@ (posedge clk) 
       ($rose(a) && block==0, set_block(1)) |-> ##1 ((b[=2] or c[=2]) intersect 1[*1:6])) 
         set_block(0); else set_block(0) ;  

    initial begin
      repeat (200) begin
        @(posedge clk);
        if (!randomize(a, b, c) with {
          a dist {1'b1 := 1, 1'b0 := 3};
          b dist {1'b1 := 1, 1'b0 := 4};
          c dist {1'b1 := 1, 1'b0 := 4};
        })
          `uvm_error("MYERR", "This is a randomize error");
      end
      $finish;
    end
  endmodule
18

In reply to ben@SystemVerilog.us:

In reply to rkg_:
Addressing your second question first
http://systemverilog.us/vf/rpt2.sv

1704×832 161 KB


// After the |-> ##1 the sequence (b} is repeated twice
ap2: assert property(a |-> ##1 (b)[*2]); 
// After the |-> the sequence (##1 b) is repeated twice
ap2_1: assert property(a |-> (##1 b)[*2]);

1704×832 161 KB

Hi Ben, I don’t get the difference. When I see both and try to rewrite the repetition operator I get

##1 b ##1 b

for both style. What am I missing?

19

In reply to emin:
In this case, there is no difference because the sequence is one term. However, let the sequence to be repeated is longer than one term.


|-> ##1 (b ##2 c)[*2]); // same as 
##1 (b ##2 c) ##1 (b ##2 c)

|-> (##1 b ##2 c)[*2]); // same as 
(##1 b ##2 c) ##1 (##1 b ##2 c)  
// The difference : 
##1 (b ##2 c) ##1     (b ##2 c)  // |->  ##1 (b ##2 c)[*2]); 
(##1 b ##2 c) ##1 (##1 b ##2 c)  // |-> (##1  b ##2 c)[*2]); 
//                 ^^^
20

In reply to ben@SystemVerilog.us:

Ben,

a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a
a[->3] ##1 b; //3 non consecutive/consecutive a and then b immediately after one clock cycle of a

If above understanding is correct , then can we use ##5 instead of ##1 in the first case?

21

In reply to ben@SystemVerilog.us:

In reply to emin:
In this case, there is no difference because the sequence is one term.

Great. Thank you for clarifying!
But we see different behaviour here,

In reply to ben@SystemVerilog.us:

In reply to rkg_:

1704×832 161 KB

How did ap2_1’s first thread did pass even though there we have b deasserted? I thought that must fail as well at the same time as ap2 since you said there is no difference.

22

In reply to emin:
OOPs! I spoke too fast, my apologies, the two ARE different.
Humans make mistakes :)


|-> ##1 (b)[*2]); 
##1 b ##1 b 

|-> (##1 b)[*2]
(##1 b) ##1 (##1 b)
23

In reply to ben@SystemVerilog.us:

That makes sense :) Thank you Ben! I appreciate.

24

In reply to emin:

Hi Ben,

Property :-
// 1st requirement (fll_lock_assertion):- FLL LOCK is asserted on detecting two positive edges
// of FLL INC or FLL DEC only when (fll_sar_eoc == 1). and fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (posedge of dec or inc) comes second comes between 1 to 8 (since prog_unlock is 1 here) then only lock should asserted.
// and two positive edge of fll_inc or fll_dec (consecutive is not necessary )
//between 1 to 6 clock cycle of sampled_clk

Type - 1

property p_lock_condition_check_unlock_prog_01; 
        int inc_count, dec_count;
 @(posedge sampled_monclk) disable iff (!i_en_fll)
   ( o_fll_sar_eoc == 1 && i_fll_unlock_prog == 2'b01, inc_count=0, dec_count=0 )   |=> 
             (1, inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec))[*1:8] ##0 
            o_fll_lock==(inc_count==2 || dec_count==2);
    endproperty

Problem 1 :-lock is asserted after 22 clk cycle of sample_monclk. and above assertion is not able to caught. (marked in purple)
Problem 2 :- assertion failing after de-assertion of lock. (marked in red )
problem 3:- Unexpected triggered (marked in blue colour)

waveform attached.

Type -2 :

property p_lock_condition_check_unlock_prog_01; 
         @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;
    endproperty

Problem -1 :- Assertion triggered but it start checking fll_inc or fll_dec right after the sar_eoc assertion till the 1 to 8 clock cycle of sample clk (instead it should wait and check fll_inc or fll_dec anytime after (sar_eoc==1) but once any thing (two posedge of dec or inc whoever come early ) between 1 to 8 of sample_monclk (since prog_unlock is 1 here) then only lock should asserted.[/b])

Waveform :-

do you see any issue ?

25

In reply to rkg_:

  • Looking at the waveforms, I see the antecedent being true for many cycles.
    ( o_fll_sar_eoc == 1 && i_fll_unlock_prog == 2’b01, inc_count=0, dec_count=0 )
    That creates multiple successful attempts, and each attempt triggers its own consequent thread that is independent of other threads. That can provide unexpected failures.
    See my paper - Understanding the SVA Engine.
    Verification Horizons - July 2020 | Verification Academy
    Try ($rose(o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2’b01[/b], inc_count=0, dec_count=0 )
  • It is very difficult for someone (me included) to debug an assertion without understanding the complete image. My best advice is to run your assertion in a small testbench environment with the simulation tool in a debug mode. In that mode, you can view the threads and the local variables and understand why the tool is telling of a pass or failure. The tool (if correct, most likely so) will do what SVA expresses, not what you wish. Thus you need to understand why SVA is behaving this way.
  • Assertion never got triggered Check your testbench. Test your assertions separately in a small testbench.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
26

In reply to ben@SystemVerilog.us:
Hi Ben,

Thanks for suggestion and i am totally agree with you.

Just one doubt on below assertion

property p_lock_condition_check_unlock_prog_01; 
         @(posedge sampled_monclk) disable iff (!i_en_fll)
      ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;
    endproperty

** intersect 1’b1[*1:8] , will it start matching just after sar_eoc==1. is it correct understanding ?

** if yes, how to put condition so that it should only match after first posedge of fll_inc and fll_dec (anytime after sar_eoc==1)

27

In reply to rkg_:


( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;
// Rearranging the ()s
      antecedent |-> 
         ##1 ( (a_sequence or b_sequence) intersect 1'b1[*1:8]
             )
         ##0 o_fll_lock;
 
// Thus, in 
               ($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8]
// the following two threads start at the same cycle 
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) // One thread 
1'b1[*1:8]                                   // a parallel thread

intersect 1’b1[*1:8] , will it start matching just after sar_eoc==1. is it correct understanding ?

NO, sar_eoc==1 is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])

Ben

28

In reply to ben@SystemVerilog.us:

Hi Ben ,

I have enabled the debug mode and i have few observation.

NO,$rose (sar_eoc) modified is in the antecedent. As mentioned above, the intersect starts after the ##1 at
($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) → one thread start just after 1 clock cycle on detection of posedge of sar_eoc and it will run based on intersect 1’b1**[1:8]* here for 8 clock cycle , (if i change to 20 thread will finish at 20 clock cycle ).

case: 2 And one place even, there is no toggle in inc and dec, it has triggered .

*it seems, what i asked question looking right here "intersect 1’b1[1:8] , will it start matching just after sar_eoc==1" (in my case )

I guess it is not taking care $rose of (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2])

thus it is triggering case 2 (my assumption )

And from above comment : (a[=3] ##1 b; //3 non consecutive/consecutive a and then b anytime after last a ) we have used [=] operator so if anytime inc or dec goes high 2 times continuously it will start intersect which is happening in my case 2 (i guess).

I have attached the waveform :

if you can suggest changes , for after detection of posedge of sar_eoc , if ($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2] (gap between two posedge of non- consecutive of inc or dec should be 8 sampled_monclk ) lock should asserted.

And in the same way

property p_lock_condition_check_unlock_prog_00; 
        int inc_count, dec_count;
 @(posedge sampled_monclk) disable iff (!i_en_fll)
   ( $rose (o_fll_sar_eoc ) && i_fll_unlock_prog == 2'b00, inc_count=0, dec_count=0)   |-> 
         **##1  ((inc_count==1 ||dec_count==1 ), inc_count+= $rose(o_fll_inc),dec_count+= $rose(fll_dec),$display("\t **time=%t inc_count**= %d, dec_count ",$time,inc_count,dec_count))**[*1:6] ##0 
            o_fll_lock===(inc_count==2 || dec_count==2);
    endproperty

** inc_count and dec_count is always zero in my log even i can see the posedge of fll_inc and dec in my simulation (Seems $rose it is not taking)

29

In reply to rkg_:
I am having trouble deciphering your question.
I modeled your code using the variables a, b, c
http://systemverilog.us/vf/may7b.sv

1269×967 165 KB

1717×895 174 KB

Below is the insertion of the code and images.
Your code looks ok
1877×1005 160 KB

What is the issue?


// DO you want this? 
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; 

// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
             (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;

I suggest that you play with my code, and add debugging features.
You may also want to rephrase your requirements in English.


module top;
    timeunit 1ns;  timeprecision 100ps;    
    `include "uvm_macros.svh"
    import uvm_pkg::*;
    bit clk, a, b, c, frame; 
    event start, one, two, isct0, endc; 
    initial forever #10 clk = !clk;

    /* ( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; */ 
    function automatic void gen_e(int i);
        if(i==0) -> start;
        if(i==0)  frame = 1'b0;
        if(i==1) -> one;
        if(i==2) ->  two;
        if(i==3) ->  isct0;
        if(i==3) frame = 1'b1;
        if(i==4) begin frame = 1'b0; ->  endc; end   
    endfunction

    always @(posedge clk) begin 
       ap_test: assert property(@ (posedge clk)  ($rose(a),gen_e(0)) |-> 
        ##1 (1, gen_e(1)) ##0 ( ($rose(b)[=2], gen_e(2)) intersect 
            (1,  gen_e(3))  ##0 1 [*1:8]  )
        ##0 (c, gen_e(4))) else  frame <= 1'b0;   
       repeat(15) @(posedge clk) ; // separate threads for analysis 
    end 

    initial begin
      repeat (200) begin        
        @(posedge clk);  #2; 
        if (!randomize(a, b, c) with {
          a dist {1'b1 := 1, 1'b0 := 4};
          b dist {1'b1 := 1, 1'b0 := 1};
          c dist {1'b1 := 1, 1'b0 := 1};
        })
          `uvm_error("MYERR", "This is a randomize error");
      end
      $finish;
    end
  endmodule

1269×967 165 KB

1717×895 174 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
30

In reply to ben@SystemVerilog.us:

Hi Ben,

As you asked,

What is the issue?

// DO you want this?   ---> **i want this** 
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
            ##1 (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock; 
 
// OR this "intersect 1'b1[*1:8] , will it start matching just after sar_eoc==1"
( (o_fll_sar_eoc == 1) && i_fll_unlock_prog == 2'b01 )   |-> 
             (($rose(o_fll_inc)[=2] or $rose(fll_dec)[=2]) intersect 1'b1[*1:8])
            ##0 o_fll_lock;

http://systemverilog.us/vf/your_screen.png → In this snippet,(at your green arrow marker ) why is assertion is getting triggered since I do not see two non-consecutive inc or dec.
I am writing assertion to check lock is happening only if two posedge of inc or dec (means only two non consecutive ) and gap between two posedge inc or dec is 1 to 8 cycle of sample_monclk.