Will the assertion trigger if my clock is Unknown

Hi,

Will the assertion trigger if my clock is Unknown. Example code below:

example: assert property (@(posedge clk) (!rst) |-> out !== 1’bx) else $error(“Error”);

will this assertion trigger and produce an error message when all clk, reset and out are 'X

Thanks

In reply to sj1992:
Try it!
However, if clk==1’bX, the @(posedge clk) produces NO event, thus will not assertion will not trigger.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

I tried the below code on EDA and it triggers the assertions. So wanted to double check

module GRG_assert2;

  logic clock;
  logic a, b, c, d;
  
  assign #5 clock = x;
  
  initial begin
    
    $asserton;
    repeat (30) @(posedge clock)
      void'(std::randomize(a, b, c)  ); 

    $stop;    
    
  end

  assert property (@(posedge clock) a |-> b |-> c) 
    $display("implication property passed with a=%b, b=%b, c=%b, clk=%b",
             $sampled(a), $sampled(b), $sampled(c), $sampled(clock));
    else
      $display("implication property failed with a=%b, b=%b, c=%b, clk=%b",
               $sampled(a), $sampled(b), $sampled(c), $sampled(clock));

endmodule

In reply to sj1992:

The code you show has a syntax error (x instead of 'x), and clock never changes.

A transition from a state other than 1’b1 to 1’bx is considered a posedge event. An unknown expression is considered the same as false. So a, b, c, and d are all false.

In reply to dave_59:

Hi Dave,

Just to be clear, always@(clk) block does not execute only when clk transitions from 1->x, in all other cases(0->x, x->0, x->1) it gets executed. Am I right?

Thanks.

In reply to sj1992:

Incorrect. @(clk) “executes” on any transition. Table 9-2 in the IEEE 1800-2017 LRM explains all of the possible transitions. In your example, clock is initially x, then you assign it to x. There is no transition.

In reply to dave_59:

Hi Dave,

I made a mistake I meant to say @(posedge clk). But now its clear thanks for pointing me to the LRM.