SVA

SystemVerilog
,
1

Hi,

I am revising SVA concepts, went through this question got stucked please help me.

How can you write an assertion to ensure that a signal ‘done’ is asserted within 100 clock cycles after ‘start’ is asserted, and ‘error’ is never asserted during this period?

2

In reply to Yogeshk:


// a signal 'done' is asserted within 100 clock cycles after 'start' is asserted, 
// and 'error' is never asserted during this period?
$rose(start) |-> (done[=1] and !error[*1:100]) intersect 1[*100];

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

3

In reply to Yogeshk:

You can try

property k1;
@(posedge clk) disable iff (~rstN)
$rose(start) |-> (done[->1] intersect !error[*1:100]);
endproperty

or use |=> instead of |->, depending on whether done can overlap with start.
Here I am assuming start is single cycle.

4

In reply to plin317:

  • The requirements were 100 cycles of no errors, thus the [*1:100] is not correct.
  • OK for: $rose(start) |-> done[=1] intersect !error[*100];
  • NO on: $rose(start) |-> done[=1] within !error[*100]; // DO NOT USE
    NO, that will not woek!
    I explain this in my paper Understanding SVA Degeneracy, link below.
    In the paper, I presented an actual user case where the requirements stated that between two rises of req starting from the next cycle, there should be one and only one new gnt. Intuitively, or perhaps naively, one would write something like the following property: $rose(req) |=> $rose(gnt)[=1] within $rose(req)[->1]// BAD
    Simulation of the above property showed that if failed to throw an assertion error when 2 or more new occurrences of gnt occurred. But why? The culprit is the Nonconsecutive repetition operator [= in combination with the within operator.
    https://systemverilog.us/vf/Degeneracy111923Ben.pdf
    Ben Cohen
5

In reply to ben@SystemVerilog.us:

Ben,
I agreed if the requirement is no error within 100 cycles. My original understanding is that done needs to come in 100 cycles, and before done come, there can not be error asserted.
Maybe Yogeshk can clarify which case is it.

Best,

6

A1:assert property(@(posedge clk) rose(start) |-> !error[*1:] intersect ##[1:100] $rose(done))

These approach is correct?..

7

In reply to Madhu C:

A1:assert property(@(posedge clk) rose(start) |-> !error[*1:] intersect ##[1:100] $rose(done))
These approach is correct?..

Requirements: to ensure that a signal ‘done’ is asserted within 100 clock cycles after ‘start’ is asserted, and ‘error’ is never asserted during this period.
rose(start) |-> !error[*1:] intersect ##[1:100] $rose(done))
Looks OK. There will be a thread (e.g., !error[*15] that intersects ##15 $rose(done).
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.