[sv-ac] Sampled value of module variables from within function

// In this *testcase.sv* model below, I have the property* p_write* that
wants to use the sampled value of the array *mem_addr* from within the
function *get_index() *that has no formal arguments. Thus, the function
reads the module variable *mem_addr *from within its scope.
Property p_write2 is almost identical to p_write, except that it uses a
function with formal argument for the variable *mem_addr.*

I believe that assertions of these 2 properties should yield the same
results. Yet I have a vendor stated that ap_write fails because
 v_index = 0, v_addr = 12. It also reports that ap_write2 passes.
I claim that the vendor is in error based on
*LRM **16.5 Concurrent assertions overview*
"All variables in a concurrent assertion *use the value sampled in the
Preponed region* of a time slot with the
*exception of local variables, constant casts and automatic variables in
procedural code *(see 16.15.6), and
free checker variables (see 17.7.2)"

16,5 seems applicable, and it states that everything is sampled in the
Preponed region EXCEPT
*local variables, constant casts and automatic variables*
In that model, I refer in the function variables of a module, which does not
fall into the above exception cases.
Thus, I claim that I do not necessarily need to pass the signal as an
argument, nor do I need to use the
$sampled function within the function that uses that module variable.

The vendor's argument is that the tool does not use sampled value of the
variables in the functions if they are not passed as arguments In this
model, if *get_inde*x function needs to look at the sampled values of the
array, it needs to be passed as one of the arguments. The vendor also added
the following:
The LRM is very murky (in many places) about what constitutes a "reference
to something". In this example, there is an
"escaping reference" (a reference from the function scope to the enclosing
scope); The code writer depends on that escaping reference being treated
symmetrically with the direct reference. But SV does not do that generally.
 In fact, always_comb goes to
great lengths to specifically add such dependencies to the sensitivity
model.

Such escaping references are not defined (in either way) in terms of the
assumptions that this model is making.

Thus, in general, a requirement to support such sampling on all possible
escaping reference in all situations is going to pose a substantial
implementation cost that would be objectionable.

Simulation output:
*With argument: mem_addr[2] = 12*
*No argument: mem_addr[2] = 13*

I am attaching the model and a manually drawn annotated timing of the
simulation results. As you can see, the function that does not use the
arguments use the non-sampled value of the array element. Instead, it uses
the updated value (13) at the time slot the function is evaluated.

 Opinions?
What is your experience with your simulator. Please sv-ac rules, we do not
mention vendors by name, but we can report what "a vendor" does.

/// THE TESTCASE MODEL (stripped down version of a real model)
module testcase;

  logic [7:0] [10:0] mem_addr;
  logic [10:0] addr;
  logic inc=0, clk=1'b1;

  function logic[7:0] get_index();
$display("No argument: mem_addr[2] =%d", mem_addr[2]);
     if(mem_addr[2]==addr) get_index=2;
else get_index=0;
  endfunction : get_index

  function logic[7:0] get_index2(logic [7:0] [10:0] mem_addr);
    $display("With argument: mem_addr[2] =%d", mem_addr[2]);
    if(mem_addr[2]==addr) get_index2=2;
else get_index2=0;
  endfunction : get_index2

  property p_write;
      int v_index;
      logic [10:0] v_addr;
    (inc, v_addr=addr, v_index=get_index()) |=>
   mem_addr[v_index] == v_addr+1'b1;
  endproperty : p_write
  ap_write : assert property(@ (posedge clk) p_write);

  property p_write2;
      int v_index;
      logic [10:0] v_addr;
    (inc, v_addr=addr, v_index=get_index2(mem_addr)) |=>
   mem_addr[v_index] == v_addr+1'b1;
  endproperty : p_write2
  ap_write2 : assert property(@ (posedge clk) p_write2);

  initial forever #5 clk=!clk;

   initial begin
for (int i=0; i<8; i=i+1)
  mem_addr[i]=i;
 repeat (3) @ (posedge clk);
     mem_addr[2] <= 11'b00000001100;
 @ (posedge clk) inc <= 1'b1;
 addr <= 11'b00000001100;
 @ (posedge clk) mem_addr[2] <= 11'b00000001101;
 inc <= 1'b0;
 repeat(5) @ (posedge clk);
  $finish;
   end

  endmodule : testcase

Thanks,
--------------------------------------------------------------------------
Ben Cohen (831) 345-1759
http://www.systemverilog.us/ ben@systemverilog.us
* SystemVerilog Assertions Handbook, 2nd Edition, 2010 ISBN
878-0-9705394-8-7
* A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
* 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
--------------------------------------------------------------------------

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

• application/octet-stream attachment: testcase.sv