SVA : last_match

Hi,

I’m developing a checker to ensure data integrity and detect read/write overlap for an asynchronous DPRAM.

property data_integrity_check ();

  logic [7:0] Addr;
  logic [7:0] Data;

 @(posedge WrClk)
    (WrEn, Addr = WrAddr, Data = WrData) |-> @(posedge RdClk) first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data);

  endproperty:data_integrity_check

It is my DUT which initiates Write and Read. The above assertion fails as my DUT might initiate multiple writes to the same address continuously with incremental data (say usually across 2 or 3 clock cycles).But the read for a given address will always be for 1 clock

As a result, 2 or 3 instance of same assertion gets spawned for every write cycle for the same address. Only the assertion-instance for the last write cycle (where the complete stable data is available) passes. The previous assertion-instances fails.

How to filter the last write on the LHS? I’m looking of something like/equivalent to ‘last_match’.

Thanks in advance.

Note: I cannot have an external logic to derive the LastWrEn, LastWrAddr as this would consume atleast 1 WrClk cycle. The ultimate objective of the assertion is to detect read/write overlap. By consuming 1 WrClk cycle the assertion would miss to detect such scenarios.

Below code is almost same as having an external logic having 1 WrClk delay.

property data_integrity_check ();

  logic [7:0] Addr;
  logic [7:0] Data;

 @(posedge WrClk)
((WrEn && (WrAddr != $past(WrAddr))), Addr = $past (WrAddr), Data = $past (WrData)) |-> @(posedge RdClk) first_match (##[0:$] (RdEn && (RdAddr == Addr))) ##1 (RdData == Data);

  endproperty:data_integrity_check

Regards,
Prem

In reply to run2prem:
Your last solution looks OK. I would change
first_match (##[0:$] (RdEn && (RdAddr == Addr))) to
(RdEn && (RdAddr == Addr)[->1] // easier to read.

You definitely need something that determines a LastWrEn, LastWrAddr. I Thought of using straight SystemVerilog code with tasks, as described in my paper SVA Alternative for Complex Assertions available at
https://verificationacademy.com/news/verification-horizons-march-2018-issue
Pseudocode would look something like


 always @(posedge WrClk)
    // local variables for last write 
   if (WrEn, Addr = WrAddr && lastwrite)
   fork test_task(); 
   join_none

task automatic test_task(); 
   write loop to do the check and report error 
endtask
// This approach gives you all the flexibility and features of SystemVerilog  
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. Verification Horizons - March 2018 Issue | 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

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

In reply to run2prem:

you suggest to use SV rather than SVA for this particular check.

This is not necessarily true. What I am saying is:

  • FOr very complex assertions an approach like the one I describe in my paper is often simpler; it is available at https://verificationacademy.com/news/verification-horizons-march-2018-issue
  • That pure SV approach basically computes the antecedent and then fires automatic tasks for the consequent as threads. It overcomes some of the issues with local variables and provides more flexibility since you use the full power of SV. Typical code would look like:

always @ (posedge clk)  begin
// local variable declations
// sequential statements (e.g., loops, @ (posedge clk), return, etc
if(vacuous_condition) return;
fork
task_emulating_the_consequent;
join_none

  • Understanding the equivalent mechanics and limitations of SVA can help create a better SVA model.

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.


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

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

Test your assertions with a simple testbench. I use the following as a test template, then fill-in the details. That template is stored in an Autotext and Text Autocompletion in any application using the application available at no cost at https://www.phraseexpress.com/


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
  timeunit 1ns;     timeprecision 100ps;    
	bit clk, a, b;  
	default clocking @(posedge clk); endclocking
    initial forever #10 clk=!clk;  
    initial begin
      $timeformat(-9, 1, "ns", 8);
      $display("%t", $realtime);
   end 
    always  @(posedge clk)  begin 
    end 
    
    initial begin 
       bit va, vb; 
      repeat(200) begin 
        @(posedge clk);   
        if (!randomize(va, vb)  with 
        { va dist {1'b1:=1, 1'b0:=3};
          vb dist {1'b1:=1, 1'b0:=2};      
      }) `uvm_error("MYERR", "This is a randomize error")
       a <= va; 
       b <= vb;
    end 
    $stop; 
  end 
endmodule    

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. https://verificationacademy.com/news/verification-horizons-march-2018-issue
  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”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment

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

In reply to run2prem:

In reply to ben@SystemVerilog.us:

 
first_match(## [0:$] b ) is same as 
 first_match(##0 b or ##1 b or ##2 b or ...),  basically the first occurence of b 

b[->1] is equivalent to: !b[*0:$] ##1 b, same as 
(!b[*0] ##1 b)or (!b[*1] ##1 b)or (!b[*2] ##1 b) or ... 
 basically the first occurence of b 

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???.

I misunderstood the requirements as I interpreted the WrAddr as a write enable
In any case, the analysis as to how you detect a last write is something you need to determine, and I do not want to get into your specific design. My goal is to help you with the tools. Your verification environment can buffer as many signals as needed to determine that last write and then to the check at a later time. The point of verification is to detect correctness in the design; there is no requirements that the detection be exactly at the cycle the error occurred, it could be a bit latler.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. https://verificationacademy.com/news/verification-horizons-march-2018-issue
  2. SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  3. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment