SVA and clock domain crossing

@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;

[Ben] this is equivalent to:

@(posedge ckA) $rose(a) |->
     @(posedge ckA) @(posedge ckB) ##1 !b;

This causes the assertion to sample rose on ckA, then wait one ckA, then wait two ckB before asserting the statement.

[Ben] NO. This causes the assertion to sample rose on ckA, then at next ckB b==0.

What i want is: sample rose on ckA, then wait two ckB before asserting the statement. How can I do this?

@(posedge ckA) $rose(a) |->
     @(posedge ckB) ##2 !b;

This causes the assertion to sample rose on ckA, then at second posedge of ckB b==0.

Ben Cohen http://www.systemverilog.us/

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books