SVA and clock domain crossing

SystemVerilog
, , , ,
5

In reply to ben@SystemVerilog.us:

Thank you! I think I understand a bit more, although asynchronous clocks produces a lot of hard cases for my assertions.

For reference I solved my $rose(a) firing later than I wanted it to with delaying my clocking edge by #1:


logic ckWriteDel, ckReadDel;
assign #1 ckWriteDel = ckWrite;
assign #1 ckReadDel = ckRead;

property pr_ifAnotBstable(a, b, ckA, ckB);
     disable iff(arstWrite | arstRead) 
     @(posedge ckA) $rose(a) |->
     @(posedge ckB) ##1 !b;
  endproperty
     
assert property 
  (pr_ifAnotBstable(fifoEmpty, fifoFull, ckReadDel, ckWriteDel))
    else $error("Assertion failed");

Not pretty, nor particularly clever. But I believe it works for my case.