Re: [sv-ac] checker : quick confirmation question on types allowed/disallowed

wire is illegal in a checker. Model was from a module.
Change
wire mem_aaray_exists; // exists at specified address
  // note: LRM 2009 17.4.1 Operand types does not allow
TO
bit mem_aaray_exists; // exists at specified address
  // note: LRM 2009 17.4.1 Operand types does not allow

On Mon, May 28, 2012 at 12:18 PM, Ben Cohen <hdlcohen@gmail.com> wrote:

> Below is an example that I had. Am looking for legality or illegality of
> something like this.
> Ben
>
> module m;
> // ..
> int top_mem_aarray[*]; // associative array to be used by property
> // can top_mem_aarray be referenced in a cheker?
> // This checker monitors the memory transactions and verifies
> // data integrity of the external memory
> checker memory_data_integrity_check (
> input write, // memory write
> input read, // memory read
> input int wdata, // data written to memory
> input int rdata, // data read from memory
> input int addr, // memory address
> input reset_n, // active low reset
> input clk); // clock
> timeunit 1ns;
> timeprecision 100ps;
> int mem_aarray[*]; // associative array to be used by property
> wire mem_aaray_exists; // exists at specified address
> // note: LRM 2009 17.4.1 Operand types does not allow use
> // of methods on associative array in properties.
> assign mem_aarray_exists = mem_aarray.exists(addr);
>
> always@ (posedge clk)
> if (reset_n==1'b0) mem_aarray.delete; // Clears AA elements
> else if (write) mem_aarray[addr] <= wdata; // store data
>
> // IS THIS LEGAL IN CHECKER?
> ap_read_after_write_LEGAL_QQ: assert property p_read_after_write(
> @(posedge clk)
> (read && mem_aarray.exists(addr) ) // LEGAL ???
> |-> mem_aarray[addr]==rdata);
>
> // IS THIS ALSO LEGAL IN CHECKER?
> ap_read_after_write_LEGAL_QQ: assert property p_read_after_write(
> @(posedge clk)
> (read && top_aarray.exists(addr) ) // ALSO LEGAL ???
> |-> mem_aarray[addr]==rdata);
>
> property p_read_after_write;
> @(posedge clk)
> (read && mem_aarray_exists) |-> mem_aarray[addr]==rdata;
> endproperty : p_read_after_write
> ap_read_after_write : assert property (p_read_after_write);
>
> property p_read_before_write;
> @(posedge clk)
> not (read && !mem_aarray_exists);
> endproperty : p_read_before_write
> ap_read_before_write : assert property (p_read_before_write);
> endchecker : memory_data_integrity_check
>
> On Mon, May 28, 2012 at 6:13 AM, Kulshrestha, Manisha <
> Manisha_Kulshrestha@mentor.com> wrote:
>
>> I meant ‘from the enclosing scope of checker declaration’. Looks like
>> rules for referring to elements of dynamic arrays, queues etc. are
>> different based on where these dynamic variables are declared. If the
>> variable declared in the enclosing scope of checker declaration is passed
>> as an actual then it is OK to refer to its elements (assuming formals of
>> checker can be of dynamic types). Is that right?****
>>
>> ** **
>>
>> Manisha****
>>
>> ** **
>>
>> ** **
>>
>> *From:* Bresticker, Shalom [mailto:shalom.bresticker@intel.com]
>> *Sent:* Monday, May 28, 2012 6:08 PM
>> *To:* Kulshrestha, Manisha; Eduard Cerny; Korchemny, Dmitry;
>> hdlcohen@gmail.com
>>
>> *Cc:* sv-ac@eda-stds.org; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> What do you mean "from outside"?****
>>
>> ** **
>>
>> *From:* Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com]
>> *Sent:* Monday, May 28, 2012 15:36
>> *To:* Bresticker, Shalom; Eduard Cerny; Korchemny, Dmitry;
>> hdlcohen@gmail.com
>> *Cc:* sv-ac@eda-stds.org; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> Hi,****
>>
>> ** **
>>
>> This looks like an inconsistency. Is there any specific reason for having
>> different rules for variables from enclosing scope vs. from outside? I
>> cannot remember discussing this.****
>>
>> ** **
>>
>> Thanks.****
>>
>> Manisha****
>>
>> ** **
>>
>> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Bresticker,
>> Shalom
>> *Sent:* Monday, May 28, 2012 5:55 PM
>> *To:* Eduard Cerny; Korchemny, Dmitry; hdlcohen@gmail.com
>> *Cc:* sv-ac@eda-stds.org; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> Yes.****
>>
>> ** **
>>
>> The original question was about checkers referencing variables from the
>> enclosing scope.****
>>
>> ** **
>>
>> Shalom****
>>
>> ** **
>>
>> ** **
>>
>> *From:* Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
>> *Sent:* Monday, May 28, 2012 15:10
>> *To:* Bresticker, Shalom; Korchemny, Dmitry; hdlcohen@gmail.com
>> *Cc:* sv-ac@eda-stds.org; Eduard Cerny; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> Shalom,****
>>
>> ** **
>>
>> but the proposed LRM does allow such access in assertions. see page 349
>> +/-. ****
>>
>> ** **
>>
>> Best regards****
>>
>> ed****
>>
>> ** **
>>
>> ** **
>>
>> *From:* Bresticker, Shalom [mailto:shalom.bresticker@intel.com]
>> *Sent:* Monday, May 28, 2012 7:52 AM
>> *To:* Korchemny, Dmitry; hdlcohen@gmail.com
>> *Cc:* sv-ac@eda-stds.org; Eduard Cerny; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> Note:****
>>
>> ** **
>>
>> The text Ben quoted does not say that dynamic variables may not be
>> referenced. It says that elements of dynamic variables may not be
>> referenced. There is a difference. ****
>>
>> ** **
>>
>> Suppose you have a (static) dynamic array d[]. d will always exist.
>> However, d[0] may or may not exist. It may exist only part of the time.
>> Thus, d could be referenced, but not d[0].****
>>
>> ** **
>>
>> Shalom****
>>
>> ** **
>>
>> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
>> Dmitry
>> *Sent:* Monday, May 28, 2012 09:54
>> *To:* hdlcohen@gmail.com
>> *Cc:* sv-ac@eda-stds.org; Eduard Cerny; Seligman, Erik
>> *Subject:* RE: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> I think this should be legal.****
>>
>> ** **
>>
>> Dmitry****
>>
>> ** **
>>
>> *From:* Ben Cohen [mailto:hdlcohen@gmail.com]
>> *Sent:* Sunday, May 27, 2012 04:37
>> *To:* Korchemny, Dmitry
>> *Cc:* sv-ac@eda-stds.org; Eduard Cerny; Seligman, Erik
>> *Subject:* Re: [sv-ac] checker : quick confirmation question on types
>> allowed/disallowed****
>>
>> ** **
>>
>> Dmitry, ****
>>
>> Thus, dynamic arrays, etc.. can be declared inside a checker as checker
>> variables,and as random checker variables? Example: ****
>>
>> checker c(input logic x[], …);****
>>
>> logic b[];****
>>
>> …****
>>
>> assert property(b[data] ...); // Legal ? (ignore syntax
>> for now) ****
>>
>> endchecker****
>>
>> ** **
>>
>> Thanks, ****
>>
>> Ben Cohen ****
>>
>> On Wed, May 23, 2012 at 5:13 AM, Korchemny, Dmitry <
>> dmitry.korchemny@intel.com> wrote:****
>>
>> Hi Ben,****
>>
>> ****
>>
>> According to my understanding formal arguments to a checker and checker
>> variables may be dynamic arrays, etc. You cannot reference dynamic arrays
>> from the enclosing scope.****
>>
>> ****
>>
>> E.g., check mycheck(a, …); is legal, even if a is a dynamic array.****
>>
>> ****
>>
>> But in****
>>
>> module m(…);****
>>
>> logic b[];****
>>
>> …****
>>
>> checker check (…);****
>>
>> assert property(…b…); // Illegal to
>> reference dynamic array from here****
>>
>> endchecker****
>>
>> endmodule****
>>
>> ****
>>
>> Regards,****
>>
>> Dmitry****
>>
>> ****
>>
>> *From:* Ben Cohen [mailto:hdlcohen@gmail.com]
>> *Sent:* Wednesday, May 23, 2012 00:47
>> *To:* sv-ac@eda-stds.org; Korchemny, Dmitry; Eduard Cerny; Seligman, Erik
>> *Subject:* [sv-ac] checker : quick confirmation questionon types
>> allowed/disallowed****
>>
>> ****
>>
>> Below are some LRM extractions. Thus, I am correct in stating that ****
>>
>> 1) formal arguments of a checker and variable of a checker *can *also be
>> of type real, time, string ****
>>
>> 2) formal arguments of a checker and variable of a checker* canot be*of type dynamic array, queue, associative array
>> ****
>>
>> LRM states that "*Automatic variables and members or elements of
>> dynamic variables*" *shall not be referenced;* thus, if no reference,
>> what's the use of declaring them if legal? ****
>>
>> . ****
>>
>> Anything else that is illegal in a checker? ****
>>
>> Thanks, ****
>>
>> Ben ****
>>
>> 17.2 Checker declaration****
>>
>> ... The legal data types for checker formal arguments are those legal for
>> a property****
>>
>> ...The following elements from the scope enclosing the checker
>> declaration shall not be referenced in a****
>>
>> checker:****
>>
>> — Automatic variables and members or elements of dynamic variables (see
>> 6.21).****
>>
>> — Elements of fork...join, fork...join_any, or fork...join_none blocks.**
>> **
>>
>> ****
>>
>> 16.6 Boolean expressions****
>>
>> ... An expression shall result in a type that is cast compatible with an
>> integral type. Subexpressions****
>>
>> need not meet this requirement as long as the overall expression is cast
>> compatible with an integral****
>>
>> type.****
>>
>> — Elements of dynamic arrays, queues, and associative arrays that are
>> sampled for assertion expression****
>>
>> 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.****
>>
>> ****
>>
>> ****
>>
>> ---------------------------------------------------------------------
>> Intel Israel (74) Limited
>>
>> This e-mail and any attachments may contain confidential material for
>> the sole use of the intended recipient(s). Any review or distribution
>> by others is strictly prohibited. If you are not the intended
>> recipient, please contact the sender and delete all copies.****
>>
>> ** **
>>
>> ---------------------------------------------------------------------
>> Intel Israel (74) Limited
>>
>> This e-mail and any attachments may contain confidential material for
>> the sole use of the intended recipient(s). Any review or distribution
>> by others is strictly prohibited. If you are not the intended
>> recipient, please contact the sender and delete all copies.
>> --
>> This message has been scanned for viruses and
>> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and
>> is
>> believed to be clean. ****
>>
>> ---------------------------------------------------------------------
>> Intel Israel (74) Limited
>>
>> This e-mail and any attachments may contain confidential material for
>> the sole use of the intended recipient(s). Any review or distribution
>> by others is strictly prohibited. If you are not the intended
>> recipient, please contact the sender and delete all copies.****
>>
>> ---------------------------------------------------------------------
>> Intel Israel (74) Limited
>>
>> This e-mail and any attachments may contain confidential material for
>> the sole use of the intended recipient(s). Any review or distribution
>> by others is strictly prohibited. If you are not the intended
>> recipient, please contact the sender and delete all copies.
>> --
>> This message has been scanned for viruses and
>> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and
>> is
>> believed to be clean. ****
>>
>> ---------------------------------------------------------------------
>> Intel Israel (74) Limited
>>
>> This e-mail and any attachments may contain confidential material for
>> the sole use of the intended recipient(s). Any review or distribution
>> by others is strictly prohibited. If you are not the intended
>> recipient, please contact the sender and delete all copies.****
>>
>
>

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.