Assertion to check signal change between 2 events

SystemVerilog
,
1

Hi folks,

I want to write an assertion to check the signal B has ever changed from 1->0 then 0->1 only once between rising edge of A and rising edge of C.

/-----------------------------------
 A  ----/

    --------\                         /------
 B           \-----------------------/

                                         /---
 C -------------------------------------/

And the rising edge of A to falling edge of B, the number of clock cycle is uncertain;
the rising edge of B to rising edge of C, the number of clock cycle is uncertain.

Thanks,

2

In reply to mlsxdx:

And I tried to write a property in this way, somehow, it doesn’t show pass or fail during the simulation. What could be the problem? How to write a better one to do the check?

   property p_rb_n_chg(s, e);
      @(posedge clk)
        $rose(s) |-> (rb_n_sel !== 1'b0)[*1:$] ##1 !rb_n_sel[*1:$] ##1 (rb_n_sel !== 1'b0)[*1:$] ##1 $rose(e);
   endproperty // p_rb_n_chg
3

In reply to mlsxdx:

Please use code tags making your code easier to read. I have added them for you.

It’s very difficult to get an assertion to fail when there are unbounded cycles. Without seeing your stimulus, it is difficult to know why it did niot pass.

I suggest using strong operators that make sure the assertion must pass before the simulation ends.

property p;
    @(posedge clk) $rose(a) |->
    (!c throughout (!b ##1 b[->1] ##1 !b[->1])) 
    #-# !b s_until c ;
endproperty
4

In reply to dave_59:
I prefer the intersect operator.


// Check the signal B has ever changed 
// from 1->0 then 0->1 only once between rising edge of A and rising edge of C.
assert property(
    @(posedge clk) $rose(a) |->
      (##1  $fell(b)[->1] ##1 b[->1]) intersect c[->1]);

See my paper “Reflections on Users’ Experiences with SVA, part 2”

Addresses the usage of these four relationship operators:**throughout, until, intersect, implies
**

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

5

In reply to dave_59:

Thanks for your fix on my code and make it much better, Dave.

I will put the test code and question together next time when I post the question.

6

In reply to ben@SystemVerilog.us:

Hi Ben,

You solution is very straightforward for checking the sequence. If changing the intersect to within, that will make B rising edge not necessarily align with C rising edge.


assert property(
    @(posedge clk) $rose(a) |->
      (##1  $fell(b)[->1] ##1 b[->1]) within c[->1]);
7

In reply to mlsxdx:
Good point. Thanks.
Ben

8

In reply to ben@SystemVerilog.us:

In reply to mlsxdx:
Good point. Thanks.
Ben

Hi Ben,
If I want the assertion check that signal b only changed(1->0->1) once, the assertion will not work. Can you point out how to improve so that it can check such case?