Assertion to check for signal propagation

SystemVerilog
1

Hi,
I am trying to write an assertion to check signal propagation. I want to see that if a “src” signal changes, then after some constant number of local clk cycles, the “dest” signal is equal to the “src” signal.

I tried writing the following way:

module try();
    logic clk = 0;
    logic src_s; 
    logic src_stable;
    logic src;
    logic dest;
    initial begin
        clk = 0;
        src = 0;
        dest = 0;
        #100;
        src = 1;
        #100;
        dest = 1;
        #20
        $finish;
    end
    initial forever begin
        #20;
        clk = ~clk;
    end

    always_ff @(negedge clk) begin       
        src_s <= src;
    end 

    assign src_stable = (src == src_s);

    MY_PROP: assert property ( 
        @(posedge clk)
        disable iff (src_stable)
        (1) |=> ##10 (src == dest))
    else $error("Propagation check failed");
endmodule

I expect this assertion to fail - but it does not fail.
Seems like the “disable_iff” argument is always 1, and I do not understand why, since src signal indeed toggles.

2

Indeed your property stays all the time ‘INACTIVE’ because src and src_s have on each rising edge of clk the same value.
Additionally your simulation is too short (shorter than 10 clk cycles. If you are disabling the condition the property becomes ACTIVE. But it completes never.

3
  1. Your assertion does not meet your requirements for
    // if a “src” signal changes, then after some constant number of local clk
    // cycles, the “dest” signal is equal to the “src” signal.
    I corrected it below.
let n=2; // constant
property p_src_dest; 
  bit v;
  @(posedge clk) ($changed(src), v=src) |-> ##n v== dest; 
endproperty : p_src_dest
ap_src_dest: assert property(p_src_dest) p1++;
else f1++; //  $error("Propagation check failed");

// https://www.edaplayground.com/x/NxVL code
// EPWave Waveform Viewer wave
2) Your TB should use nonblocking assignments as a good practice rule.
3) Aside from directed rtest, you should consider randomization.
4) U strongly suggest that you read my reply on “Getting started with verification with SystemVerilog”
https://rb.gy/f3zhh
file is also attached.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemveri
roadmaptosva.pdf (172.0 KB)

4

I prefer to use $past in this scenario - it is FV friendly besides other aspects:

property p_src_dest; 
  bit v;
  @(posedge clk) ($changed(src) ) |-> ##n $past(src, n) == dest; 
endproperty : p_src_dest
ap_src_dest: assert property(p_src_dest)
8

Thanks!

9

Thanks!

10

Thanks!

11

If the property is:

($changed(src), v=src) |-> ##n v== dest;

You’re basically saying “when src changes, dest will be at the same value after n clocks”.

I think the problem is that if src doesn’t change, then dest can be wiggling randomly but the property would still be happy. And I guess this is not the point of the test. So, I would maybe change the property to check src vs dest on every clock cycle (and hope that there’s are no glitches that fall between clk edges).

12

That was the original requirement. Yes, the following meets that req.

($changed(src), v=src) |-> ##n v== dest;

You’re basically saying “when src changes, dest will be at the same value after n clocks”.
[YOU] think the problem is that if src doesn’t change, then dest can be wiggling randomly but the property would still be happy. And I guess this is not the point of the test. So, I would maybe change the property to check src vs dest on every clock cycle (and hope that there’s are no glitches that fall between clk edges).
[Ben] then you have to redefine the requirements if this is what you want.
See Reflections on Users’ Experiences with SVA, part 1

Important concepts on EXPRESSING REQUIREMENTS,
Terminology, threads in ranges and repeats in antecedents, multiple antecedents.

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