Creating an assertion to verify that a change in one signal corresponds to the posedge of another

SystemVerilog
, ,
1

Hey,

What I’m trying to do is essentially verify that the input port of some module is driven by the correct clock domain. To check this, I want to write an assertion that looks sort of like this:

@(input_signal) |-> @(posedge clk)

In order to verify that any change in input_signal happens only on posedge of a given clock. To the best of my knowledge, it isn’t possible in SystemVerilog. Is there a way to implement this sort of functionality in an assertion (or via some other tool)?

Thanks in advance for any help!

2

I took 2 approaches,explore these solutions and get back to us.

It provides error counters or a pass counter for each edge of sig1.


/* What I'm trying to do is essentially verify that the input port of some module
 is driven by the correct clock domain. To check this,
 I want to write an assertion that looks sort of like this:
@(input_signal) |-> @(posedge clk)
In order to verify that any change in input_signal
 happens only on posedge of a given clock. To the best of my knowledge,
  it isn't possible in SystemVerilog. Is there a way to implement
   this sort of functionality in an assertion (or via some other tool)?

*/
module top;
  bit clk, sig1, dis, reset_n=1; 
  int err1, err2, ok2, debug2, tfire;
 // always @(sig1)  // approavh 1 
 //   assert final($past(sig1,1,1, @(posedge clk)) != sig1) else 
 //     err1=err1+1;
   function void f; err1=err1+1; endfunction
  always @(sig1)   // approach 1, value based 
       #1 // needed for the $past
        assert ($past(sig1,1,1, @(posedge clk)) != sig1) else f(); 

  task automatic t_stable(); // 
     realtime t; 
    tfire=tfire+1;
     t=$realtime; // new sig1 change after posedge clk 
     //#1; // debug2=debug2+1; // debug
    @(posedge clk)  debug2=debug2+1;
    assert($realtime - t <= 21ns && 
                               $realtime -t >= 20ns) ok2=ok2+1; 
                 else err2=err2+1; 
  endtask

  always @(sig1) begin 
    fork t_stable(); join_none; // time based
  end

  initial forever #10 clk = !clk;
  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    #5 sig1 = 1; 
    @(posedge clk) sig1<= !sig1;
    #3 sig1 <= !sig1; 
    @(posedge clk) sig1<= !sig1;
    @(posedge clk) sig1<= !sig1;
    #8 sig1 <= !sig1;
    repeat(4)  @(posedge clk) sig1<= !sig1;
    #20 $finish(); 
  end
endmodule

1870×600 38.2 KB

1870×600 38.2 KB

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

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:
The assertion with the task could have been written as

property p_dfromclk; 
 realtime t;
 @(sig1) (1, t=$realtime) ##1
 @(posedge clk) $realtime -t <= 21ns && 
 $realtime -t >= 20ns;
 endproperty 
 ap_dfromclk: assert property(p_dfromclk) ok3=ok3+1; 
 else err3=err3+1;

The reason I initially wrote it with the task is because that’s how I saw it: at the leading clocking event (the @(sig1) I fire an automatic task that has a life of its own. This is explained in my paper "Understanding the SVA Engine Using the Fork-Join Model
Verification Horizons - July 2020 | Verification Academy
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.
You should read this paper if you want to relly understand a good modeling of assertions.
The updated model with this new property is at (4) - EDA Playground
The simulation results are at

4

In reply to ben@SystemVerilog.us:

This diagram explains why we need the #1 in

function void f; err1=err1+1; endfunction
 always @(sig1)  // approach 1, value based 
 #1 // Needed for the $past of the posedge of clk just prior
 assert ($past(sig1,1,1, @(posedge clk)) != sig1) else f();

1461×849 49.9 KB

1461×849 49.9 KB

5

Thanks Ben, I appreciate the answer. I figured that at the very least I could use $realtime, but your solution was more elegant than what I hacked together.