Use of an Associative array or Queue in System Verilog Assertion Property


I want to write an assertion for the below requirement.
AWPROT[0] value should be stored at one clock tick with AWID and should be compared with TPROT[0] after a certain(random) clock ticks with the same TWID.

I am trying to use an associative array but It is not helping out. Also tried the same approach with the queue but no luck.

property value_chk(bit[2:0] override_bit);
  int value_array[int];
  @(posedge clk) disable iff(reset) ((AVALID && AREADY), value_array[AWID]=AWPROT[0]) |-> (TVALID && TREADY) |-> 
  if(override_bit == 2'b00) TPROT[0] == 0 else
  if(override_bit == 2'b01) TPROT[0] == 1 else
  if((override_bit == 2'b10 && AWPROT[0] == 0)) TPROT[0] == !(AWPROT[0]) else
  if((override_bit == 2'b11 && AWPROT[0] == 1)) TPROT[0] == AWPROT[0];
endproperty: value_chk

value_check: assert property(value_chk(override_bit_value))

Please help to fulfill the requirement.

Thanks in advance !!


The code you show

  • contains references to many signals not in your requirements.
  • writes to value_array but never reads it.
  • only spans one clock cycle
  • has nested implications which never works the way you think it does

Note that a local variable in a property declaration gets allocated for each attempt (start of the property), it will not accumulate values.

Hi Dave,

Thanks for the prompt response.
If a local variable doesn’t accumulate values, Is there any way that can store value at one clock tick and we can use it to compare on any other clock tick?


You don’t need an array for that. A local variable can store a value and “keep” it around for the life each assertion thread.

Using an assertion woth  ultple antecedents is not recommended. 
a |-> seq |-> seq2  // not recommended 
here is an example of assertions using associative arrays for simulation. 
From my SVA book 
module memory_data_integrity_check (
    input bit write, // memory write
    input bit read,  // memory read
    input bit[31:0] wdata, // data written to memory
    input bit [31:0] rddata,  // ** NEW: data read from memory 
    input bit[31:0]  addr,  // memory address -- small for simulation 
    input bit reset_n, // active low reset
    input bit clk);   // clock 

    timeunit 1ns;   timeprecision 100ps;
    default clocking cb_clk @ (posedge clk);  endclocking 
    int mem_aarray[*]; // associative array (AA) to be used by property
    bit [31:0] raadata;  // data read from AA
    bit  mem_aarray_exists;  // exists at specified address
    assign mem_aarray_exists  = mem_aarray.exists(addr); 
            raadata  = mem_aarray[addr];  //  
    always@ (posedge clk)
        if (reset_n==1'b0) mem_aarray.delete; // Clears AA elements
        else if (write) mem_aarray[addr]  = wdata; // store data

    // ** Using an associative array to store the last data written **
    // If a write, save addr into v_wraddr, data is saved into the associative array 
    // by support logic. 
    // if at some time we have a read, and the address exists in the associative array 
    property p_read_after_write;
        bit [31:0] v_wraddr;
        (write, v_wraddr=addr) ##1  // if write, save data and addr
        (read && mem_aarray_exists && addr==v_wraddr) [->1] |-> // @read and data there at same written addr
        rddata==raadata;  // *** read data from IO is same as what was written 
    endproperty : p_read_after_write
    ap_read_after_write : assert property (p_read_after_write)
        $info("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata)); else 
        $error("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata));

    // ** METHOD 2. Vacuity if 2nd write to same address 

    property p_read_after_1_write;
            bit [31:0] v_wraadata, v_wraddr;
            (write, v_wraddr=addr, v_wraadata= wdata) ##1  // if write, save data and addr
            (!write && addr==v_wraddr)[*1:$] ##1 (read  && addr==v_wraddr) [->1]  
              // @read and data there at same written addr
               // and NO 2nd write to same address 
            |-> rddata==v_wraadata;  // *** read data from IO is same as what was written 
    endproperty : p_read_after_1_write
    ap_read_after_1_write : assert property (p_read_after_write)
            $info("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata)); else 
            $error("addr =%h, raadata=%h", $sampled(addr), $sampled(raadata)); 
    property p_read_before_write;
        not (read && !mem_aarray_exists); // never a read on an non written address
    endproperty : p_read_before_write
    ap_read_before_write : assert property (p_read_before_write);
endmodule : memory_data_integrity_check
// *** Testbench needs to be updated, it is not correct 
class c_xactn;
    rand bit write; // memory write
    rand bit read;  // memory read
    rand int wdata; // data written to memory
    rand bit[31:0] addr;  // memory address 
    rand bit [31:0] rddata;   // memory data 
    constraint addr_range_cst { addr dist {111:=1, 2222:=1};} //, 3333:=1};}
    constraint no_wr_and_rd_cst { !(read && write);}
    constraint rddata_cst  {rddata dist {32'hF:=1, 32'hFFFF:=1};} //, 32'hFFFF:=1};}
    constraint wrdata_cst  {wdata  dist {32'hF:=1, 32'hFFFF:=1};} //, 32'hFFFF:=1};}
endclass : c_xactn
module top;
    timeunit 1ns;   timeprecision 100ps;
    bit write; // memory write
    bit read;  // memory read
    int wdata; // data written to memory
    bit [31:0] rddata;   // memory data 
    bit[31:0] addr;  // memory address 
    bit reset_n=1'b1; // active low reset
    bit clk=1'b1;   // clock
    // Because you have used “c1” as a variable name and a block name.
    //  Normal search rules say the block name hides the name of the variable name.

    c_xactn c1;
    memory_data_integrity_check mem_check1 (.*);

    initial forever #5 clk=!clk;

    initial begin : i1
      repeat(300) begin :r1
         @ (posedge clk) begin :cl1
          if(!c1.randomize())  $error("c1 randomization failure"); 
          write <= c1.write; 
          read  <=; 
          wdata <= c1.wdata;  
          addr  <= c1.addr; 
          rddata <= c1.rddata; 
       end :cl1
      end :r1
    end : i1
endmodule : top 

en Cohen
Link to the list of papers and books that I wrote, many are now donated.


Probably, you need to keep AWPROT value and AWID value as local variables.

    int prot;
    int id;
    (AVALID && AREADY, prot = AWPROT, id = AWID) |-> (TVALID && TREADY && (TWID == id))[->1] ##0 TPROT == prot;

You don’t need associative array. Keep in mind that assertion is parallel process. That is, different check processes are invoked every time whenever the condition AVALID && AREADY meets.

This solution is working @Orimitsu .

Thank you all for your help.