Can i use Associative array in property or sequence?

Hi all;
Can i use an associative type of array in sequence or property? If it is possible, can you give a small piece of code for understanding purpose.
I tried a small code

module axi4_assertions(input all signals);
int len_array[int];
int count[int];

property wlast;
@(negedge ACLK)
(AWVALID && AWREADY) |-> (len_array[AWID] = AWLEN) |-> if(WVALID)
(count[AWID]+1)[*0:$] |-> (count[AWID] == len_array[AWID]);
endproperty

WLAST_ASS : assert property(wlast);

endmodule

Is it correct or not?
Thanks
Siva

In reply to Siva91221:
Your example does not show associative arrays.
Comment: How to determine if something is legal?
When I was learning VHDL, I often asked that question to my instructor. He taught me a simple lesson: If you want to know if something is legal or illegal, write a test code and check it out with a good simulator; a reputable vendor has a far better understanding of the LRM than you.

Anyway, 1800’2017 16.6 Boolean expressions:
evaluation may get removed from the array or the array may get resized before the assertion expression is evaluated. These specific array elements sampled for assertion expression evaluation shall continue to exist within the scope of the assertion until the assertion expression evaluation completes.
from my book SVA Handbook 4th Edition
Thus, other types that are allowed under the consideration of the same rule include elements of dynamic arrays, queues, and associative arrays, records, multi-dimensional arrays. The following examples demonstrate the use of such types.

 // ch2/2.6/types.sv
int dataQ [$]; // queue, can store/read incoming data
int mem_aarray[*]; // associative array (AA)
ap_test : assert property (mem_aarray[addr]==rdata);
ap_never_read_on_emptyOK: assert property(not (dataQsize == 0 && rd));

Guidelines: 1800’2012 allowed the use of dynamic array, queues, and associative arrays in assertions. However, these new language features may not be adopted right away by all vendors, as that will take some time, depending upon customers’ needs. Thus we recommend that assertions use static variables, and any information needed for the assertion be copied into static variables. The following example demonstrates the concept using dynamic arrays.


module dynamic_array; // Ch2/2.6/dynamic_array.sv
    int dyn[], d2[]; // Empty dynamic arrays
    int a_size, d2_value; bit clk;
    initial forever #10 clk=!clk;
    always_comb if (d2.size>0 && d2.size <= 5) d2_value = d2[5];
    initial begin
        dyn = new[5]; // Allocate 5 elements
        $display("dyn.size=%d", dyn.size);
        foreach (dyn[j])
          dyn[j] = j; // Initialize the elements
        d2 = dyn; // Copy a dynamic array
        d2[0] = 5; // Modify the copy
        $display(dyn[0],d2[0]); // See both values (0 & 5)
        dyn = new[20](dyn); // Expand and copy
        $display("dyn.size=%d, d2.size=%d", dyn.size, d2.size);
        dyn = new[100]; // Allocate 100 new integers
        $display("dyn.size=%d, d2.size=%d", dyn.size, d2.size);
        repeat(20) @ (posedge clk);
        // Old values are lost
        dyn.delete; // Delete all elements
        $display("dyn.size=%d, d2.size=%d", dyn.size, d2.size);
    end
     
endmodule :dynamic_array

A local formal argument can be of types int, bit, byte, vectors (e.g., logic[15:0]), shortreal, real, realtime, packed array, packed structure, packed union, dynamic arrays, queues, and associative arrays, enum. The following example demonstrates legal assertion constructs.


..
    byte q1[$], y1=3, y2; // q1 is a queue of bytes sequence q_test(byte q[$]); // (Ch/2.7/type_m.sv)
    byte v_q[$];
    
    sequence q_test(byte q[$]);
        byte v_q[$];
        ($rose(a), v_q.push_back(y1)) ##1 q[0]==v_q.pop_front();
    endsequence
    ap_q: assert property(q_test(q1));
    // -------------
    string s1="TEST", s2="test";
    ap_test: assert property(s1==s2.toupper());
    // -------------
    typedef enum {BK_RED , BK_GREEN, BK_BLUE } colors_e;
    colors_e color;
    ap_colors: assert property(color==BK_BLUE);
    // -------------
    int mem_aarray[*]; // associative array
    ap_test : assert property (mem_aarray[addr]==rdata);
    // -------------
    real r1=1.03, r2=1.03;
    shortreal sr1, sr2;
    int data;
    realtime rt1=101.11, rt2;
    sequence q_r(real ra, rb, realtime rt);
        ra==rb ##1 rt > rt1;
    endsequence
    ap_q_r: assert property(q_r(r1, r2, rt2));
    always @ (posedge clk) rt2<= $realtime;
    ap_test: assert property(s1==s2);

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy