Sampling 'clk' in concurrent SVA

SystemVerilog
1

One of the designer’s on our team wants to write an assertion to check that ‘clk’ on any edge of ‘clk’ has known value:
assert property( @(clk) disable iff (rst) (~$isunknown(clk)))

what are the implications of sampling ‘clk’ itself on any edge of ‘clk’ ?

2

In reply to Jartar:

If clk remains unknown, you will never get an assertion failure.

There might be performance overhead depending on the frequency of clk relative to other clocks.

A better approach might be to look at conditions that might cause clk to gho to X and perhaps use formal tools to check for that.

3

In reply to Jartar:

One of the designer’s on our team wants to write an assertion to check that ‘clk’ on any edge of ‘clk’ has known value:
assert property( @(clk) disable iff (rst) (~$isunknown(clk)))
what are the implications of sampling ‘clk’ itself on any edge of ‘clk’ ?

The sampled value of signal clk is its value at the Preponed region.
Thus, for clk going from X to 1, the sampled value of clk is X.
For clk going from 1 to X, the sampled value of clk is 1
See my paper: Understanding Assertion Processing Within a Time Step (Horizons Feb 27, 2023 issue)

This paper details how evaluation regions should be handled by a simulator as described in the SystemVerilog LRM; this should give you a better understanding of how assertions work.

EPWave Waveform Viewer waveform



module m; 
  logic clk, rst=0; 
  int pass, fail;
  assert property( @(clk) disable iff (rst) (~$isunknown(clk)))
       pass=pass+1; else fail=fail+1;
  initial begin
    $dumpfile("dump.vcd"); $dumpvars;
    #2 clk=1; #2 clk=1'bX; #2 clk=0; #2 clk=1'bX; 
    #2 $finish;
  end 
endmodule

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

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog