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

Filed Mantis 0002947
http://www.eda-stds.org/svdb/view.php?id=2947
 <http://www.eda-stds.org/svdb/view.php?id=2947>

On Tue, Jan 19, 2010 at 9:02 AM, ben cohen <hdlcohen@gmail.com> wrote:

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