Assertion for unique data values

[syedtaahirahmed]

Hi Ben ,

Creating a new thread if in case the other thread is missed , later we can merge accordingly if duplicated.

There is scenario.

1. for every posedge of request signal, after N(1 to 50) number of request high ,valid signal gets triggered and the request goes low the next cycle along with valid.
2. for every request & valid high, there is data value which should not be equal to previous data value, this keeps repeating for N number of times.

How do I make sure that first data and consecutive data are unique

I tried the solution with above pointers, i am able to make my solution working until assertion is failing for the below condition ::
a)When Request=1, $rose(valid) data =value , the next cycle data = 0.
i couldn’t able to sync the data for comparison kindly help

This is my full code::

module Data_unique;
  reg clk = 1;
  logic request,ack;
  bit [255:0] data;
  bit [255:0] out;
  bit [255:0]  q_data[$];
  logic True = 1;
 
  always #50 clk = ~clk;  
  initial 
    begin 
      $dumpfile("dump.vcd"); $dumpvars;
    request=0;ack=0;
    #200
    request=1; #100 ack=0;          // request started
    #500
    #100 ack=1;     // ack and data
       data = 256'habcd_5555;//data 1
   //   data = 0;   // error condition when data =0      
    #100
    request=0; ack=0;data=0;       
    #200
    request=1; #200 ack=1;
    data = 256'h1234_5678; // data2
    #100
    request=0; ack=0;data=0;          
    #200
    request=1; #100 ack=1;
    data = 256'h9876_5430;  //data 3 
    //   data = 256'h1234_5678; //same data causes violation 
    #100
    request=0;ack=0;data=0;  
    #300
    request=1; #300 ack=1;  // 
    data = 256'hdcba_5555; // data 4
   //data = 256'h9876_5430; //same data causes violation 
    #100
    request=0; ack=0;data =0;  
      #500
    $finish;
  end
 
 
  task automatic t_check_data(bit ack_sync,bit request_sync);
       @(posedge clk)
       if(request_sync && ack_sync ==True) begin : is_valid	
            if (q_data.size == 0)begin
              q_data.push_back(data);
              if(data == 0)
                $error("Data should be non zero\n");
            end
            else begin
              out = data;     
              foreach(q_data[i]) begin
                assert(out !== q_data[i]);
              end
              q_data.push_back(data);
            end                 
            $display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
        end 
	return;	
    // end
  endtask 
 
 
  // As From
  property Data_handshake;
    @(posedge clk)    
   ($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1)) ##1 (!request && !ack);
  endproperty
  assert property (Data_handshake);
 
endmodule

[ben2]

In reply to syed taahir ahmed:

You understand the problem better than I do, but I have an issue with the style of your testbench. Specifically,

1. Your test vectors are not based on a clock. Instead, you rely on absolute delays.
   Instead of #500, use repeat(5) @(posedge clk)
2. You use blocking assignments instead of nonblocking assignments. These two combinations (the one above and this one) are begging for timing problems.
3. As a general rule, I tend to avoid directed tests. Below is an example of my style to test assertions:

My generic method for the creation of test vectors. I modify the constraints as needed by the model.

initial begin 
       bit va, vb; 
      repeat(200) begin 
        @(posedge clk);   
        if (!randomize(va, vb)  with 
        { va dist {1'b1:=1, 1'b0:=3};
          vb dist {1'b1:=1, 1'b0:=2};      
        })  `uvm_fatal("RAND", "This is a randomize error")
        #1; a <= va; 
            b <= vb;
       end 
      $stop; 
    end 
 

I modified your model by making all test vectors nonblocking.
I added debugging events.
I use the immediate assertion instead of the if(!x) $error
I put all the tests in the task. As you noticed, the task fired from the sequence_match_item is a fire and forget. It does not return to the sequence.

Take a look at these changes and see if that works for you.

module Data_unique;
    reg clk = 1; // <<< use bit !!!!!!
    logic request,ack;
    bit [255:0] data;
    bit [255:0] out;
    bit [255:0]  q_data[$];
    int  dsize; 
    logic True = 1;
    event e1, e2, e3; 

    assign dsize=q_data.size; 

    function automatic void gen_event(int a); 
        if(a==1) -> e1; 
        if(a==2) -> e2; 
        if(a==3) -> e3;
      endfunction : gen_event 
    
    always #50 clk = ~clk;  
    initial 
    begin 
        $dumpfile("dump.vcd"); $dumpvars;
        request=0;ack=0;
        repeat(2) @(posedge clk); //#200
        request<=1; @(posedge clk) ack<=0; //#100 ack=0;          // request started
        repeat(5) @(posedge clk); // #500
        @(posedge clk) ack<=1; //#100 ack=1;     // ack and data
        data <= 256'habcd_5555;//data 1
        //   data = 0;   // error condition when data =0      
        @(posedge clk); //#100
        request<=0; ack<=0;data<=0;       
        repeat(2) @(posedge clk); // #200
        request<=1; repeat(2) ack<= 1; // #200 ack=1;
        data <= 256'h1234_5678; // data2
        @(posedge clk); // #100
        request<=0; ack<=0;data<=0;          
        repeat(2) @(posedge clk); #200
        request<=1; @(posedge clk) ack<=1; // #100 ack=1;
        data <= 256'h9876_5430;  //data 3 
        //   data = 256'h1234_5678; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0; data<=0;  
        repeat(3) @(posedge clk); // #300
        request<= 1; repeat(3) ack<=1; // #300 ack=1;  // 
        data <= 256'hdcba_5555; // data 4
        //data = 256'h9876_5430; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0;data <=0;  
        repeat(5) @(posedge clk); // #500
        $finish;
    end
    
    
    task automatic t_check_data(bit ack_sync,bit request_sync);
        ->e2; 
        @(posedge clk)
        if(request_sync && ack_sync ==True) begin : is_valid	
            if (q_data.size == 0)begin
                q_data.push_back(data);
                if(data == 0)
                $error("Data should be non zero\n");
            end
            else begin
                out = data;     
                foreach(q_data[i]) begin
                    assert(out !== q_data[i]);
                end
                q_data.push_back(data);
            end                 
            $display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
        end 
        @(posedge clk) a_handshake: assert(!request && !ack);
        return;	
        // end
    endtask 
    
    /* property Data_handshake_V0;
        @(posedge clk)    
       ($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1)) 
                            ##1 (!request && !ack);
    endproperty */ 

         // As From
    property Data_handshake;
        @(posedge clk)    
        ($rose(request), gen_event(1)) |-> 
            ##[1:50] (($rose(ack) && request), t_check_data(1,1)) 
              ##1 (1, gen_event(3)); // (!request && !ack);
    endproperty
    ap_Data_handshake: assert property (Data_handshake);
    
endmodule  

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[syedtaahirahmed]

In reply to ben@SystemVerilog.us:

HI Ben,

Seems like the issue is still persisting.The issue is the data variable out could not able to sync the data when ack&&request , data is high on that cycle. This might be due to sampling region.

i will explain my assertion need one more time::
1)when there is request, the ack comes after some cycle suppose 1 to 50 cycles.
then at the $rose(ack) && request, the data is valid.
2)The ack and request goes low immediately in the next cycle & data= 0, and this sequence of request and ack occur many times with unique data values

the eda playground link:: Edit code - EDA Playground

Thanks

[ben2]

In reply to syed taahir ahmed:

Data is initially equal to 0, from the code at declaration, by default.
Thus, if(data == 0)
$error(“Data should be non zero\n”);
Will show as error.
BTW, that should be an immediate assertion instead of the “if”. But in any case, do you need this line?.
I try to run the code again.
Ben Ben@systemverilog.us

[syedtaahirahmed]

In reply to ben@SystemVerilog.us:

Yes you are right Ben, I’ll fix that code for initial data == 0 and use immediate assertion.
Thanks for that pointers but I am still yet to figure it out on how to sample the data when (request and ack)?

[syedtaahirahmed]

In reply to ben@SystemVerilog.us:

Hi Ben,

I have used $past to capture the data and looks like i am able to sync the data.
I am assuming that the condition (($rose(ack)&& request) ,t_check_data(1,1)).The first expression which sample in next clock due to system verilog scheduling, so i used $past to capture the data.

Please let me know if this is fine.

module Data_unique;
    reg clk = 1; // <<< use bit !!!!!!
    logic request,ack;
    bit [255:0] data;
    bit [255:0] out;
    bit [255:0]  q_data[$];
  //  int  dsize; 
    logic True = 1;
    event e1, e2, e3; 
 
  //  assign dsize=q_data.size; 
 
    function automatic void gen_event(int a); 
        if(a==1) -> e1; 
        if(a==2) -> e2; 
        if(a==3) -> e3;
      endfunction : gen_event 
 
    always #50 clk = ~clk;  
    initial 
    begin 
        $dumpfile("dump.vcd"); $dumpvars;
        request=0;ack=0;
        repeat(2) @(posedge clk); //#200
        request<=1; @(posedge clk) ack<=0; //#100 ack=0;          // request started
        repeat(5) @(posedge clk); // #500
        @(posedge clk) ack<=1; //#100 ack=1;     // ack and data
        data <= 256'habcd_5555;//data 1
        //   data = 0;   // error condition when data =0      
        @(posedge clk); //#100
        request<=0; ack<=0;data<=0;       
      repeat(4) @(posedge clk); // #200
      request<=1;@(posedge clk) ack<= 1; // #200 ack=1;
        data <= 256'h1234_5678; // data2
        @(posedge clk); // #100
        request<=0; ack<=0;data<=0;          
      repeat(4) @(posedge clk); 
        request<=1; @(posedge clk) ack<=1; // #100 ack=1;
        data <= 256'h9876_5430;  //data 3 
        //   data = 256'h1234_5678; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0; data<=0;  
        repeat(3) @(posedge clk); // #300
      request<= 1; @(posedge clk) ack<=1; // #300 ack=1;  // 
        data <= 256'hdcba_5555; // data 4
        //data = 256'h9876_5430; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0;data <=0;  
        repeat(5) @(posedge clk); // #500
        $finish;
    end
 
 
    task automatic t_check_data(bit ack_sync,bit request_sync);
        //->e2; 
        @(posedge clk)
        if(request_sync && ack_sync ==True) begin : is_valid	
      //if($rose(ack) && request) begin
            if (q_data.size == 0)begin
              if(data == 0)
                $error("Data should be non zero\n");
              q_data.push_back($past(data));                
            end
            else begin
              out = $past(data);     
                foreach(q_data[i]) begin
                    assert(out !== q_data[i]);
                end
              q_data.push_back($past(data));
            end                 
            $display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
        end 
      //  @(posedge clk) a_handshake: assert(!request && !ack);
        return;	
        // end
    endtask 
 
    /* property Data_handshake_V0;
        @(posedge clk)    
       ($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1)) 
                            ##1 (!request && !ack);
    endproperty */ 
 
         // As From
    property Data_handshake;
        @(posedge clk)    
       // ($rose(request), gen_event(1)) |-> 
       //     ##[1:50] (($rose(ack) && request), t_check_data(1,1)) 
       //       ##1 (1, gen_event(3)); // (!request && !ack);
      ($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1)) ##1 (!request && !ack);
    endproperty
    ap_Data_handshake: assert property (Data_handshake);
 
endmodule

Eda playground:: Edit code - EDA Playground

Thanks

[ben2]

In reply to syed taahir ahmed:

1. For SystemVerilog timing slots, see from my boook
   Sampling point of Assertions | Verification Academy
2. In a property, you want all the variables used in that property to be sampled in the Preponed region. If the needed variable is to be used in a function or a task, use a property local variable and save that module variable into the local variable. Thus,

property Data_handshake;
bit [255:0] v_data;
bit v_fail;
@(posedge clk)
($rose(request), v_data=data, gen_event(1)) |-> ...

3. Looking at your code, it looks that the task does not need to extend over multiple cycles, and is used more like a function. If that is the case, use a function. The function returns a value (bit pass) tha can be used in the assertion to log in the failure.

property Data_handshake;
bit [255:0] v_data;
bit v_pass;
@(posedge clk)
($rose(request), v_data=data, gen_event(1)) |->
first_match(##[1:50] (($rose(ack) && request), v_pass= t_check_data(1,1,v_data)))
##0 v_pass ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
endproperty
ap_Data_handshake: assert property (Data_handshake); 

Note that the **first_match()**is needed because of the ##[1:50]
4. The function then becomes:

function automatic t_check_data(bit ack_sync,bit request_sync, bit [255:0] ldata);
automatic bit pass=1;
->e2;
// @(posedge clk)
if(request_sync && ack_sync ==True) begin : is_valid
if (q_data.size == 0)begin
q_data.push_back(ldata);
a_size0: assert(ldata != 0) else pass=0;
// $error("Data should be non zero\n");
end
else begin
out = ldata;
foreach(q_data[i]) begin
assert(out !== q_data[i]) else pass=0;
end
q_data.push_back(ldata);
end
$display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
end
// @(posedge clk) a_handshake: assert(!request && !ack);
return pass;
// end
endfunction

testbench module

module Data_unique;

    reg clk = 1;
    logic request,ack;
    bit [255:0] data;
    bit [255:0] out;
    bit [255:0]  q_data[$];
    int  dsize; 
    logic True = 1;
    event e1, e2, e3; 

    assign dsize=q_data.size; 

    function automatic void gen_event(int a); 
        if(a==1) -> e1; 
        if(a==2) -> e2; 
        if(a==3) -> e3;
      endfunction : gen_event 
    
    always #50 clk = ~clk;  
    initial 
    begin 
        $dumpfile("dump.vcd"); $dumpvars;
        request<=0; ack<=0; data <= 1; // <<<<********NEW
        repeat(2) @(posedge clk); //#200
        request<=1; @(posedge clk) ack<=0; //#100 ack=0;          // request started
        repeat(5) @(posedge clk); // #500
        @(posedge clk) ack<=1; //#100 ack=1;     // ack and data
        data <= 256'habcd_5555;//data 1
        //   data = 0;   // error condition when data =0      
        @(posedge clk); //#100
        request<=0; ack<=0;data<=0;       
        repeat(2) @(posedge clk); // #200
        request<=1; repeat(2) ack<= 1; // #200 ack=1;
        data <= 256'h1234_5678; // data2
        @(posedge clk); // #100
        request<=0; ack<=0;data<=0;          
        repeat(2) @(posedge clk); #200
        request<=1; @(posedge clk) ack<=1; // #100 ack=1;
        data <= 256'h9876_5430;  //data 3 
        //   data = 256'h1234_5678; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0; data<=0;  
        repeat(3) @(posedge clk); // #300
        request<= 1; repeat(3) ack<=1; // #300 ack=1;  // 
        data <= 256'hdcba_5555; // data 4
        //data = 256'h9876_5430; //same data causes violation 
        @(posedge clk); // #100
        request<=0; ack<=0;data <=0;  
        repeat(5) @(posedge clk); // #500
        $finish;
    end
    
    
    function automatic t_check_data(bit ack_sync,bit request_sync, bit [255:0] ldata);
        automatic bit fail;
        ->e2; 
        // @(posedge clk)
        if(request_sync && ack_sync ==True) begin : is_valid	
            if (q_data.size == 0)begin
                q_data.push_back(ldata);
                a_size0: assert(ldata != 0) else fail=1; 
                // $error("Data should be non zero\n");
            end
            else begin
                out = ldata;     
                foreach(q_data[i]) begin
                    assert(out !== q_data[i]) else fail=1;
                end
                q_data.push_back(ldata);
            end                 
            $display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
        end 
        // @(posedge clk) a_handshake: assert(!request && !ack);
        return fail;	
        // end
    endfunction 
    
    /* property Data_handshake_V0;
        @(posedge clk)    
       ($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1)) 
                            ##1 (!request && !ack);
    endproperty */ 

         // As From
    property Data_handshake;
        bit [255:0] v_data;
        bit v_fail;
        @(posedge clk)    
        ($rose(request), v_data=data, gen_event(1)) |-> 
            ##[1:50] (($rose(ack) && request), v_fail= t_check_data(1,1,v_data)) ##0 v_fail 
              ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
    endproperty
    ap_Data_handshake: assert property (Data_handshake);
    
endmodule


Test results 

# @                 1000 out_data = 0 q_data=0
# ** Error: Assertion error.
#    Time: 1 us Started: 300 ns  Scope: Data_unique.ap_Data_handshake File: C:/ben_play/./uniq2.sv Line: 94 Expr: v_pass
#    Local vars : v_data = 0, v_pass = 0
# @                 1800 out_data = 12345678 q_data=0 305419896
# @                 2200 out_data = 98765430 q_data=0 305419896 2557891632
# ** Note: $finish    : C:/ben_play/./uniq2.sv(51)
#    Time: 2700 ns  Iteration: 1  Instance: /Data_unique 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

[syedtaahirahmed]

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

Thanks for detailed explanation on this.
I executed the code as is in eda playground::Edit code - EDA Playground,
but i am observing following::

1)The data 1 , data 3 and data 4 are not assigned to out data variable as seen in waves.
2)Also i would like to mention that , the valid data is available only when request & ack is high and next cycle data = 0.
3)So since we are using ldata(local data ) and from the antecedent the value of data is getting sent which seems not as expected as we have to get the data when request&ack high.

can you please suggest on this?

Thanks

[ben2]

In reply to syed taahir ahmed:

Quick reply on item 2, store v_data at the correct cycle

 
         // As From
    property Data_handshake;
        bit [255:0] v_data;
        bit v_fail;
        @(posedge clk)    
        ($rose(request), gen_event(1)) |-> 
            ##[1:50] (($rose(ack) && request),   v_data=data,
v_fail= t_check_data(1,1,v_data)) ##0 v_fail 
              ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
    endproperty
    ap_Data_handshake: assert property (Data_handshake);
 
  

[syedtaahirahmed]

In reply to ben@SystemVerilog.us:

Hi Ben,

Exactly thanks for reply, i tweaked it the similar way you mentioned and also (##0 v_fail ) was giving issues in capturing the data in queue ,so i kind of removed and now it seems working fine.

Also the property will fail to capture the data if $rose(request) & $rose(request), is there a way to fix for the condition $rose(request) && $rose(ack).

below is my modification code:: still the property fail to capture when request and ack high at the same time.

    property Data_handshake;
        bit [255:0] v_data;
        bit v_fail;
        @(posedge clk)    
        $rose(request) |-> 
         first_match(##[1:50] ((($rose(ack) && request) || ($rose(ack) && $rose(request))),v_data=data,t_check_data(1,1,v_data))
      ##1 (!request && !ack)); // (!request && !ack);
    endproperty
    ap_Data_handshake: assert property (Data_handshake);

[ben2]

In reply to syed taahir ahmed:

(($rose(ack) && request) || ($rose(ack) && $rose(request))

// By definition, $rose(a) is same as ! $past(a)!==1 && a
// Thus ((($rose(ack) && request) || ($rose(ack) && $rose(request)) is same as
((($rose(ack) && request) || ($rose(ack) && $past(request)==0 && request)
// The $past(request)==0 is not needed. Above is reduced to
($rose(ack) && request)
2. (##0 v_fail )
In the function, I used “pass”. The copy/paste copied the wrong testbench, sorry!
a_size0: assert(ldata != 0) else pass=0;
3. giving issues in capturing the data in queue ,
I don’t see how the pass or fail variable relates to the capture of data.
It’s irrelevant
4. still the property fail to capture when request and ack high at the same time.
// I dont get your issue.

    property Data_handshake;
bit [255:0] v_data;
bit v_pass;
@(posedge clk)
($rose(request), gen_event(1)) |->
first_match(##[1:50] (($rose(ack) && request),
v_data=data, v_pass= t_check_data(1,1,v_data)))
##0 v_pass ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
endproperty
ap_Data_handshake: assert property (Data_handshake); 

When ($rose(ack) && request) is true, you activate the function and pass to it the value of data stored in v_data prior to the function call. BTW, in this particular case, sice the time of the function call is the same as the time (or cycle) you capture the data, you can directly pass the data to the function without storing it into the local variable. That data will be sampled in the Preponed region.
5.

repeat(2) @(posedge clk); #200
request<=1; @(posedge clk) ack<=1; // #100 ack=1;
data <= 256'h9876_5430;  //data 3  

After the 2nd posedge clk, request==1, then at then posedge clk ack ==1 and data change value. At the next posedge clk, those values are sample in the Preponed region and $rose(ack) && request is true. The data is captured at that cycle.
I really do not understand your issues.
Updated testbench

module Data_unique;
reg clk = 1;
logic request,ack;
bit [255:0] data;
bit [255:0] out;
bit [255:0]  q_data[$];
int  dsize;
logic True = 1;
event e1, e2, e3;
assign dsize=q_data.size;
function automatic void gen_event(int a);
if(a==1) -> e1;
if(a==2) -> e2;
if(a==3) -> e3;
endfunction : gen_event
always #50 clk = ~clk;
initial
begin
$dumpfile("dump.vcd"); $dumpvars;
request<=0; ack<=0; data <= 0; // 1; // <<<<********NEW
repeat(2) @(posedge clk); //#200
request<=1; @(posedge clk) ack<=0; //#100 ack=0;          // request started
repeat(5) @(posedge clk); // #500
@(posedge clk) ack<=1; //#100 ack=1;     // ack and data
data <= 256'habcd_5555;//data 1
//   data = 0;   // error condition when data =0
@(posedge clk); //#100
request<=0; ack<=0;data<=0;
repeat(2) @(posedge clk); // #200
request<=1; repeat(2) ack<= 1; // #200 ack=1;
data <= 256'h1234_5678; // data2
@(posedge clk); // #100
request<=0; ack<=0;data<=0;
repeat(2) @(posedge clk); #200
request<=1; @(posedge clk) ack<=1; // #100 ack=1;
data <= 256'h9876_5430;  //data 3
//   data = 256'h1234_5678; //same data causes violation
@(posedge clk); // #100
request<=0; ack<=0; data<=0;
repeat(3) @(posedge clk); // #300
request<= 1; repeat(3) ack<=1; // #300 ack=1;  //
data <= 256'hdcba_5555; // data 4
//data = 256'h9876_5430; //same data causes violation
@(posedge clk); // #100
request<=0; ack<=0;data <=0;
repeat(5) @(posedge clk); // #500
$finish;
end
function automatic t_check_data(bit ack_sync,bit request_sync, bit [255:0] ldata);
automatic bit pass=1;
->e2;
// @(posedge clk)
if(request_sync && ack_sync ==True) begin : is_valid
if (q_data.size == 0)begin
q_data.push_back(ldata);
a_size0: assert(ldata != 0) else pass=0;
// $error("Data should be non zero\n");
end
else begin
out = ldata;
foreach(q_data[i]) begin
assert(out !== q_data[i]) else pass=0;
end
q_data.push_back(ldata);
end
$display("@ %t out_data = %0h q_data=%0p", $time,out,q_data);
end
// @(posedge clk) a_handshake: assert(!request && !ack);
return pass;
// end
endfunction
/* property Data_handshake_V0;
@(posedge clk)
($rose(request)) |-> ##[1:50] (($rose(ack) && request) , t_check_data(1,1))
##1 (!request && !ack);
endproperty */
/* property Data_handshake;
bit [255:0] v_data;
bit v_fail;
@(posedge clk)
$rose(request) |->
first_match(##[1:50] ((($rose(ack) && request) || ($rose(ack) && $rose(request))),v_data=data,t_check_data(1,1,v_data))
##1 (!request && !ack)); // (!request && !ack);
endproperty
ap_Data_handshake: assert property (Data_handshake); */
// As From
property Data_handshake;
bit [255:0] v_data;
bit v_pass;
@(posedge clk)
($rose(request), gen_event(1)) |->
first_match(##[1:50] (($rose(ack) && request),
v_data=data, v_pass= t_check_data(1,1,v_data)))
##0 v_pass ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
endproperty
ap_Data_handshake: assert property (Data_handshake);
property Data_handshake_option2;
bit [255:0] v_data;
bit v_pass;
@(posedge clk)
($rose(request), gen_event(1)) |->
first_match(##[1:50] (($rose(ack) && request),
//v_data=data,
v_pass= t_check_data(1,1,data)))
##0 v_pass ##1 (!request && !ack) ##0 (1, gen_event(3)); // (!request && !ack);
endproperty
// sim results  http://systemverilog.us/vf/data_unique2.png
# @                 1000 out_data = 0 q_data=2882360661
# @                 1800 out_data = 98765430 q_data=2882360661 2557891632
# @                 2200 out_data = dcba5555 q_data=2882360661 2557891632 3703199061
endmodule 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. SVA Alternative for Complex Assertions
   https://verificationacademy.com/news/verification-horizons-march-2018-issue
2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
3. SVA in a UVM Class-based Environment
   https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

[syedtaahirahmed]

In reply to ben@SystemVerilog.us:

Hi Ben ,

Now i understood my issues, Thanks for detailed explanation.
I executed your code in Eda Playground , everything looks as expected but i see the second data is not assigned to out variable from waves.Meanwhile i also debug the same.

Link::Edit code - EDA Playground

I was not able to upload the screen shot of it, as the post asking to URL link for Picture , i am not sure how to do that.

Thanks