Will the assertion trigger if my clock is Unknown

[sj1992]

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

[ben2]

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

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

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

[sj1992]

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

[dave_59]

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.

[sj1992]

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.

[dave_59]

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.

[sj1992]

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.