SVA - To check value at previous OR current OR next clock cycle

SystemVerilog
, ,
1

Hi ,

when B asserted , A should be asserted at previous clock OR current clock OR next clock.

How do we write better SVA assertion ?


assert property (@(posedge clk) $rose(B) |-> ##[0:2] $past(A)) else $error("Error");

Any suggestions?

Thanks

2

In reply to John Pratheep:

assert property (@(posedge clk) $rose(B) |-> ##1 $past(A,2) || A) else $error("Error");
3 

$rose(B) |-> ##1 $past(A,2) || A)
// same as 
$rose(B) |-> ##1 ($past(A,2) || A)) // because of the logical ||
##1 $past(A,2) // is the single past of A in reference to B 
##1 A is A in the next cycle, or the future. 
// We are missing the current A
// How about 
$rose(B) |-> A ##1 $past(A,2) || A) 
// Also 
$rose(B) |-> A || $past(A,1) or ##1 A)

I addressed Bing GPT-4 AI because it does a fair to good job of converting
English to SV code and SVA assertions. It also can convert SVA into a module
that meets those requirements.
I tried on this and it failed miserably. I am passing it on because I see AI
doing a better job in the future. You might get a laughter…


/* [ME] write a systemverilog assertions for this requirement: 
when B asserted , A should be asserted at previous clock OR current clock OR next clock.

Use posedge clk */
//Here is a SystemVerilog assertion that checks if the requirement is met:
property check_A;
    @(posedge clk)
    (B |-> (A || $past(A) || $future(A)));
endproperty
assert property(check_A);
/* This assertion checks that whenever B is asserted at the positive edge of clk, A should be asserted at the previous clock, current clock or next clock. The $past and $future functions are used to refer to the values of A at the previous and next clock cycles respectively.*/
//[ME] There is not $future in systemverilog, fix this
/* You are correct. My apologies for the mistake. Here is the corrected SystemVerilog assertion that checks if the requirement is met: */
property check_A;
    @(posedge clk)
    (B |-> (A || $past(A) || $rose(A)));
endproperty
assert property(check_A);
/* This assertion checks that whenever B is asserted at the positive edge of clk, A should be asserted at the previous clock, current clock or next clock. The $past function is used to refer to the value of A at the previous clock cycle and $rose function checks if A will be asserted at the next clock cycle. */
?? $rose function checks if A will be asserted at the next clock cycle. ???

[ME] The body of the assertions should be one of these, learn from your mistakes:
$rose(B) |-> A ##1 $past(A,2) || A) // Also $rose(B) |-> A || $past(A,1) or ##1 A)


// BING -gpt-4: 
Thank you for pointing out the mistake and providing the correct assertion. Here is the corrected SystemVerilog assertion that checks if the requirement is met:

property check_A;
    @(posedge clk)
    ($rose(B) |-> A ##1 $past(A,2) || A);
endproperty

assert property(check_A);
/* This assertion checks that whenever B is asserted at the positive edge of clk, A should be asserted at the previous clock, current clock or next clock. The $past function is used to refer to the value of A at the previous clock cycle and ##1 operator checks if A will be asserted at the next clock cycle.

I apologize for any confusion I may have caused and appreciate your help in correcting my mistake. */

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

4

In reply to dave_59:

Thanks Dave

5

In reply to ben@SystemVerilog.us:

Thanks Ben for your clear explanation.

6

In reply to John Pratheep:

And Correcting GPT to produce right results in future :)

7

In reply to ben@SystemVerilog.us:

Below code works.


assert property (@(posedge clk) ($rose(A) |-> B or ##1 ($past(B,2) || B))) else $error ("Error");