[sv-ac] SVA: Can local variable of sequence used as array index?

Can a local variable be used as an index?
Also, can a formal parameter be used as an index? For example,
property p (a, b, c, addr, index);
   int v;
    (a, v=addr) |=> b[index] == c[v];
endproperty : p

My thoughts: Probably yes. From SV3.1a LRM
    17.4.1 Operand types
...— dynamic arrays
Fixed size arrays, packed or unpacked, can be used as a whole or as part
selects or as indexed bit or part
selects. The indices can be constants, parameters, or variables.
Comments are appreciated.
Thanks,
Ben

-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
_http://www.vhdlcohen.com/_ (http://www.vhdlcohen.com/) vhdlcohen@aol.com
Author of following textbooks:
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004 isbn
 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
------------------------------------------------------------------------------
Received on Thu Jun 17 12:21:47 2004