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

It appears that it is a common practice by vendors to not sample any global
variable accessed by functions or tasks,
Understandably, from the vendors's perspective it simplifies things a lot,
and puts less burden on the simulator. If you want it to use the sampled
values, then pass $sampled(arg) to the function or use arguments. That
gives more flexibility, but it also makes that sampling issue "tricky".

That common practice does violate the letter of the law: the LRM.
 Specifically:
*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.6.2 Variables*
*The variables that can appear in expressions shall be static design
variables, function calls returning values*
*of types described in 16.6.1, or local variables. Static variables declared
in programs, interfaces, or clocking*
*blocks can also be accessed. If a reference is to a static variable
declared in a task, that variable is sampled*
*as any other variable, independent of calls to the task.*

Unless thee is a place in the LRM that states what is commonly done on this
issue, we need to file a Mantis to clarify this very point.
http://www.eda-stds.org/ is currently down

Ben

On Mon, Jan 18, 2010 at 6:04 PM, ben cohen <hdlcohen@gmail.com> wrote:

> // 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.