SVA : last_match

SystemVerilog
, , ,
5

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks. Will definitely go through your paper in detail.

Your code looks like it has the correct approach, but I have an issue with its correctness.
You are looking for the last write cycle. Assuming that that you load the register with 2, 3 or 4 consecutive writes, and WrAddr is an active ONE, then the last write would occur when
$fell(WrAddr_pre)&& WrAddr rather than your WrAddr != WrAddr_pre.

I’m not clear with your assumptions here. WrAddr & WrAddr_pre are 7-bit wide. $fell(WrAddr_pre)??? Not sure what you mean by ‘WrAddr’ is an active ONE???.

WrEn is an active high signal in my case.

The idea behind (WrAddr != WrAddr_pre):

  • WrAddr_pre will be 1 WrClk ahead w.r.t WrAddr.
  • Last cycle of current address for WrAddr will be nothing but the first cycle of WrAddr_pre for a new address.
  • Its the last cycle of WrAddr when WrAddr and WrAddr_pre will not be equal.

first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data); is equivalent to
(RdEn && RdAddr == Addr)[->1] ##1 (RdData == Data);

I’m not well proficient with SVA. I’ll try to understand this.

Thanks a lot

Regards,
Prem