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

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.