Write an assertion ,after the clk has arrived within 5 clk cycles write or read should not occur

SystemVerilog
, , ,
1

I’m writing an assertion to check at the initial stage of clk my read & write should not happen until 5 clk cycles.
I written as below


sequence w_r
##[1:5] (read & write )
endsequence

sequence not_w_r
 not w_r
endsequence

assert property (@posedge clk) first_match not_w_r else $display("----- assertion failed -----");

Here I have 2 doughts

  1. can i write w_r sequence without any event or clk semantics
  2. Is my understanding is correct for not w_r : It means my sequence w_r should not happen, if w_r seq occurred my assertion will show fail

Actually, we can write it simply like below

 
@(posedge clk) $rose(clk) |-> ##[0:5] ((!write) || (!read));

I just want to try with not and understand first_match

Correct me on this.

Thanks Regards
Sunodh

2

In reply to SUNODH:
Since this is a homework question, I’ll give guidelines into the solutions.

I’m writing an assertion to check at the initial stage of clk my read & write should not happen until 5 clk cycles.

One of the main requirements is “at the initial stage of clk”.
That is not well defined, but it typically means during the forst “n” clock after boot.
Assuming n==10, you could use an initial statement with a loop for 10 clocking events.
There you can write a concurrent or an immidiate assertion.

I written as below


sequence w_r
##[1:5] (read & write )
endsequence
sequence not_w_r
not w_r
endsequence
assert property (@posedge clk) first_match not_w_r else $display("----- assertion failed -----");

the not is aproperty operator. You need to understand what first_match is and where it is used. See my papers to get a good understanding of assertions.

Here I have 2 doubts:

  1. can i write w_r sequence without any event or clk semantics

Yes, as long as you do not use an endpoint when tht sequence is used.

  1. Is my understanding is correct for not w_r : It means my sequence w_r should not happen, if w_r seq occurred my assertion will show fail

Yes

Actually, we can write it simply like below

 
@(posedge clk) $rose(clk) |-> ##[0:5] ((!write) || (!read));

NO, you do not want to do that with a rose of the clock. $rose is used with a module variable.

Links to my papers are in my signature below.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:
  1. Papers:
    Understanding the SVA Engine,
    https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II
    Understanding and Using Immediate Assertions
    Understanding and Using Immediate Assertions
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
    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
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/
3

In reply to ben@SystemVerilog.us:

In reply to SUNODH:
One of the main requirements is “at the initial stage of clk”.
That is not well defined, but it typically means during the forst “n” clock after boot.
Assuming n==10, you could use an initial statement with a loop for 10 clocking events.
There you can write a concurrent or an immidiate assertion.

Thank You Ben as per your instruction I used below logic it worked for me


  initial
    begin
    repeat(10)
      begin
        @(posedge clk)
        assert (!read && !write)
          $display ($time, " PASS:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time);
        else
          $fatal ($time, " FAIL:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time); 
      end
    end

But I like to use

not (!read && !write)

&

first_match (not_read_write)

and what I know is we can’t use them in an immediate assertion.
Are they any way we can check this assertion using the assert property?

4

In reply to SUNODH:
You can use the current assertion with the not(property).
An imediate asserion uses expressions and does not use properties.


initial
    begin
    repeat(10)
      begin
        @(posedge clk)
        // That clocking event flows into the property 
        ap_rdwr_init: assert property (not(read || write))
          $display ($time, " PASS:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time);
        else
          $fatal ($time, " FAIL:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time); 
      end
    end

On first_match (not_read_write), You need to study what first_match of a sequence means,
and ask yourself what the first_match of a expression results into.
Ben

5

In reply to ben@SystemVerilog.us:

Hi Ben ,
I executed the above code

assert property (not(read || write))

in edaplayground it is showing below error
Error-[PAOCNAILS] Procedural assertion in a loop
Procedural assertion ( i.e., assert, assume or cover property) is not allowed in looping statement.Only immediate assertions are allowed in this context.

6

In reply to SUNODH:
I made an error on the clock flowing through.
//OK


module nl;
  bit clk, read, write;
  initial forever #10 clk = !clk; 
  initial
    begin
    repeat(10)
      begin
        @(posedge clk)
        // That clocking event flows does not flow into the property 
        ap_rdwr_init: assert property( @(posedge clk) not(read || write))
          $display ($time, " PASS:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time);
        else
          $fatal ($time, " FAIL:: write = %0d, read = %0d   |  @_Time = %0t\n", $sampled(write),$sampled(read),$time); 
      end
          $finish;
    end
          endmodule