Assertion for check between signals changing on different edges of same clock

SystemVerilog
, ,
1

Hi All,

How to write an assertion for following case-
There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
clk is same for a, b.

Any alternative to assertion will also be helpful.

Any help would be appreciated

2

In reply to verif4life:
As an educator, I am reluctant to answer what you can easily write yourself and learn something in the process. Thus, I suggest that you look into 1800’2017: 16.13.1 Multiclocked sequences. Your requirements are a simple application of that along with the use of the implication operator (|->).
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to ben@SystemVerilog.us:

Hi Ben,
This is working in my case.
Can you please check this.
Additionally can you give any way to implement this without assertions.For checking signal fell it checks on two consecutive clock edges, for signal ‘a’ in my case it is two consecutive negedge, by the time I get a 2nd negedge my signal b falls at posedge. so I am not getting when to start the check on signal b


property p1;
 // @(negedge clk)  !a |-> @(posedge clk)  !b ;  does not actually checks the falling edge
    @(negedge clk)  $fell(a)  |-> @(posedge clk)  $fell(b)  ;
endproperty

assert property (p1) ;
4

Try this (Haven’t tested)


//  There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
//Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
//clk is same for a, b.

 ap_arbiter: assert property(first_match(@(negedge clk) $fell (a)) |-> (@(posedge clk) $fell (b)))
            $display ("Assertion passed",$time);
            else $display ("Assertion failed",$time);
5

In reply to rag123:

Thanks for your reply. It is working.
Can you provide a way so that it does not throw an error for the first clock edge??
Here the clock starts after power on reset so cannot use disable iff (rst)… and default value of signal is x and sampled value at first clocking event is 0. So $fell will be true and hence the antecedent…

Also cannot change signal ‘a’ to bit type because it is an internal DUT signal… is it good way to take variable in assertion interface as bit type so that it would be automatically typecast x, z to 0???

6

In reply to verif4life:

Two options:

  1. you can use ##1 delay to avoid the first clocking event.

ap_arbiter: assert property(first_match(@(negedge clk) ##1 $fell (a)) |-> (@(posedge clk) $fell (b)))
2) Use tasks recommended by Ben.
https://verificationacademy.com/forums/systemverilog/paper-understanding-sva-engine-simple-alternate-solutions

For casting, It is always better to do typecast first.

7

In reply to rag123:

Thanks a lot

8

In reply to rag123:

first_match is NOT NEEDED in a single threaded antecedent.
Let’s not the kitchen sink at an assertion and hope that it works.
Ben systemverilog.us