SVA : last_match

SystemVerilog
, , ,
3

Hi Ben,

Thanks for the quick suggestion. If I understand correctly, you suggest to use SV rather than SVA for this particular check. Yes, there is no handy ‘last_match’ construct available.

But for now, I’ve taken the below approach.

  • The WrAddr is my DUT’s output port.
  • The driver of this port would be somewhere deep inside the RTL.
  • We shall use a signal which is one flop-stage before the actual driver (say WrAddr_pre). Do port mapping in the assertion module using HDL path of this signal.
  • Luckily, my DUT has a clear register stage for this signal.

The code will now look like


 property data_integrity_check ();
 
   logic [7:0]Addr;
   logic [7:0]  Data;
    
    disable iff (~RG_ResetN)
    @(posedge WrClk)
    (WrEn && (WrAddr != WrAddr_pre), Addr = WrAddr, Data = WrData) |-> @(posedge RdClk) first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data);
 
  endproperty:data_integrity_check

As WrAddr_pre will be 1 WrClk ahead than the WrAddr, (WrAddr != WrAddr_pre) will take us to the last write for a given address.

But yes, it comes with some compromises

  1. We should assume the register stage logic in RTL is golden (may be after some careful analysis)
  2. The checker will become slightly a white-box checker(and no more a black-box).

I think considering the complexity, these compromises are kind of acceptable I guess.

Please let me know your thoughts.

Thanks,
Prem