SVA to check a N-stage synchronizer output

SystemVerilog
, , , ,
1

Hi all! I want to write an assertion for an N-stage synchronizer output (this synchronizer accounts for metastability modeling, so its delay is non-deterministic and it ranges in between N and M cycles).

This assertion needs to check that: a signal B can only change (from 0 to 1, or from 1 to 0) if and only if a signal A has changed (from 0 to 1, or from 1 to 0) in between [N:M] cycles in the past.

Thanks in advance!

2

property check_signal_b_change;

@(posedge clk)

($fell(signal_b) || $rose(signal_b)) |->

( ##[N:N+1] $changed(signal_a) );

endproperty

3

Hi @liviareis,

Assuming the clock edges occur at T0 ( 1st clock edge ) , T1 , T2 , T3 , … Tx,

N & M are constants with values 3 & 5 respectively.

If signal A changes at T2 then signal B should change at T5 or T6 or T7 ,

is this the expectation ?

4

Hi arshi582! No, according to your example, the assertion should check that: If signal B changes at T6 then signal A should have changed at T3 or T2 or T1.

        T0    T1    T2    T3    T4    T5    T6    T7    
CLK    __/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__
         ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊     
B      ____________________________________/‾‾‾‾‾‾‾‾‾‾‾‾‾
         ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊     
A      ________________/‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
         ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊     
               <===========>                 *
              -5    -4    -3    -2    -1     0
5

property check_signal_b_change;

@(posedge clk)

($fell(signal_b) || $rose(signal_b)) |->

( ##[N:M] $changed(signal_a) );

endproperty

This is checking that, if B changes, then A should change from N to M cycles later.

What I want to check is: if B changes, then A should have changed in between [N:M] cycles in the past.

6

Currently this is what I have:

sequence A_rose;
  @(posedge clk) $rose(A) ##[N:M] 1'b1;
endsequence

sequence A_fell;
  @(posedge clk) $fell(A) ##[N:M] 1'b1;
endsequence

property B_CHANGED_DUE_TO_A;
  @(posedge clk) disable iff (~rst_n)
  $changed(B) |-> (B && A_rose.triggered) or (~B && A_fell.triggered);
endproperty

assert property (B_CHANGED_DUE_TO_A);
7

If signal A changes at T6 then signal B should have changed at T3 or T2 or T1.

sequence b2a_change( N , M );
 $changed(b) ##[N:M] $changed(a);
endsequence

property b_2_a( N , M );
  @(posedge clk) disable iff (!rst_n)
    $changed(a) |→ b2a_change(N,M).triggered;
endproperty

b2a:assert property( b_2_a(3,5) ) else `uvm_error(..)
8

Hi Have_A_Doubt, thanks for you reply but I didn’t see a big difference between your solution and the one I already have.

BTW, the issue I have with this solution is that during simulation, when B changes too close to the rising edge of the clock, the design and the sequence samples different values; the design samples 1 and the sequence samples 0.

 

    D[0]   _______   Q[0]   _______  Q[1]
A ------->|D     Q|------->|D     Q|-------> B
          |       |        |       |
          |  FF0  |        |  FF1  |
          |       |        |       |
CLK ----->|>CK    |     -->|>CK    |
           ‾‾‾‾‾‾‾          ‾‾‾‾‾‾‾

           T0    T1    T2    T3    T4    T5    T6    T7    
    CLK  __/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__/‾‾\__
           ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊     
A, D[0]  ______________/‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
           ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊       
   Q[0]  _______________/‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
           ┊     ┊     ┊     ┊     ┊     ┊     ┊     ┊     
B, Q[1]   _____________________/‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾

At T2, D[0] is 1 and Q[0] goes to 1. I’d expect that $rose(A) is true at T2, but it isn’t - it is only true at T3.

Anyone has an alternative solution or a solution for the issue I am having?

Thanks!