ACK goes high for 1 clk ONLY after 10 cycle of Req going high but never before 10 cycles

SystemVerilog
, , , ,
1

Hello,

Scenario: Req goes High, after 10 cycle ACK should go high for 1 clk cycle.
Check : 1. Above condition 2. ACK doesnt get asserted before 10 clk 3. it remains high for 1 clk

The following code capture Check_1.
int xyz=10; //variable coming from an equation and not a constant
property assert_check_loop;
int v;
@(posedge clk) disable iff(disable_assertion)
($rose(m), v=xyz+1, $display(“2: Assertion Started %t”,time)) |-> (v>0, v=v-1'b1)[*0:] ##0 v==0 ##0 $rose(n);
endproperty : assert_check_loop

Can you please help me with Check_2 and Check_3 in the same assertion.

Thanks

2

In reply to SVA_USR:

Hi,
For Check_1: $rose(m) |-> ##10 $rose(n) ##1 $fell(n);
For Check_2: use $rose (n) |-> ( $past(m,10));
for Check_3: use $rose and $fell
($rose(m), v=xyz+1, $display(“2: Assertion Started %t”,time)) |-> (v>0, v=v-1'b1)[*0:] ##0 v==0 ##0 $rose(n) ##1 $fell(n) ;

3

In reply to SVA_USR:

As I suggested in another thread here, split them to multiple - it is easy to maintain. debug and formal friendly.


// Req goes High, after 10 cycle ACK should go high for 1 clk cycle.
// Check : 1. Above condition 2. ACK doesnt get asserted before 10 clk 
// 3. it remains high for 1 clk 

  property p1;
    $rose(req) |-> ##10 $rose(ack);
  endproperty : p1

  property p2;
    $rose(req) |-> !ack [*9];
  endproperty : p2

  property p3;
    $rose(req) |-> ##11 !ack;
  endproperty : p3

Regards
Srini
www.go2uvm.org

4

In reply to vdangeti:

Thanks vdangeti for the reply.
“For Check_2: use $rose (n) |-> ( $past(m,10));”
Observation: The assertion only triggered once. Even though Rose(n) appeared later in simulation, the Assertion remained in Finished state forever after once triggering.
Query: as I mentioned “10” is not fixed and hence I took “xyz”. So 10 cant be used directly in $past(m,10) at the same time being a variable it cannot be used either. Any solution?

Cheers.

5

In reply to Srini @ CVCblr.com:

Thanks Srini for the reply. I perfectly understand your point and concern for not mixing all three together and make it complex for debug and readability both.
But being a learner and exploring the field am interested to know how can Check_2 be clubbed together with Check_1. I tried multiple options few failed, few “Never Finished”, few gave compilation errors.
So if you can suggest me a piece of code that would be very helpful.

Cheers.

6

In reply to SVA_USR:

How about?


// Req goes High, after 10 cycle ACK should go high for 1 clk cycle.
// Check : 1. Above condition 2. ACK doesnt get asserted before 10 clk 
// 3. it remains high for 1 clk 
 
  property p1_2_3;
    $rose(req) |-> !ack [*9] ##1 ack ##1 !ack;
  endproperty : p1

Srini
www.verifnews.org

7

In reply to Srini @ CVCblr.com:

In reply to SVA_USR:
How about?


// Req goes High, after 10 cycle ACK should go high for 1 clk cycle.
// Check : 1. Above condition 2. ACK doesnt get asserted before 10 clk 
// 3. it remains high for 1 clk 
property p1_2_3;
$rose(req) |-> !ack [*9] ##1 ack ##1 !ack;
endproperty : p1

Thanks Srini. It looks perfect but when it comes to Variable delay and not a Fixed constant-10, is where I am stuck.

int xyz=10; //variable coming from an equation and not a constant
property assert_check_loop;
int v;
@(posedge clk) disable iff(disable_assertion)
($rose(m), v=xyz+1, $display(“2: Assertion Started %t”,time)) |-> (v>0, v=v-1'b1)[*0:] ##0 v==0 ##0 $rose(n);
endproperty : assert_check_loop

Here I wanted to use **!n in conjunction with the repeat util operator[*0:]**. something like: (v>0, v=v-1'b1,!n )[*0:]

@(posedge clk) disable iff(disable_assertion)
($rose(m), v=xyz+1, $display("2: Assertion Started %t",$time)) |-> |->(v>0, v=v-1'b1,!n )[*0:$] ##0 v==0 ##0 $rose(n);

As expected, It didnt work :(

Can you please throw some light here.

8

In reply to SVA_USR:

Hi

Try this snippet for all three checks

`timescale 1ns/1ps
module assert_tb;

reg req;
reg ack;
bit clk = 0;
int xyz = 10; 

initial
begin
  forever
  #0.5 clk = ~clk;
end

initial
begin
  req = 0;
  ack = 0;
  // FAIL CRITERIA
  #1  req = 1;
  #9  ack = 1;
  #1  ack = 0;
  // PASS CRITERIA
  #1  req = 0;
  #1  req = 1;
  #10 ack = 1;
  #1  ack = 0;
  #20;
$finish;
end

property assert_check_loop;
int v;
@(posedge clk) 
($rose(req), v=xyz, $display("Assertion Started %t",$time)) |-> (v>0 && !ack, v=v-1)[*0:$] ##0 v==0 ##1 ack ##1 !ack;
endproperty : assert_check_loop 

assert property( assert_check_loop)
$info("PASS");
else
$error("FAIL");

endmodule
9

In reply to srikanth_6313:

Thanks a lot Srikanth for the help and pointer. It worked.

One query, how to use variable with $past(ack, 10) → int xyz=10; past(ack,xyz) I tried using loop (v=0, v-v-1[*0:]) it didnt accept.

Any clues.

Cheers.