Re: [sv-ac] Re: [SV-AC] Local Variables Flow Out Issue in and/or/intersect/implies

I updated my proposal. Please read localvariables_in_implies_v4.pdf in
http://www.eda-stds.org/svdb/view.php?id=3195
Attached is same file.
*The point of this proposal is that the language must be flexible enough to
allow its use in a variety of ways, *
*particularly if it adapts to a style that eases the verification of
completeness in formal verification*

On Sun, Sep 5, 2010 at 12:40 PM, ben cohen <hdlcohen@gmail.com> wrote:

> 1. Changed title to:
> Local Variables Flow-in Issue in and/or/intersect/implies
> 2. Changed #4 to:
> The local variable shall not be read in the same time unit it is
> written.
> 3. Updated the docx file.
>
> On Fri, Sep 3, 2010 at 9:19 AM, ben cohen <hdlcohen@gmail.com> wrote:
>
>> (Same reply is also in pdf/docx format in
>> http://www.eda-stds.org/svdb/view.php?id=3195 )
>>
>> John,
>>
>> I know that the implication operator can be used as an alternative.
>> However, there are several motivations to allow
>>
>> the flow in of local variables into property statements / sequences that
>> are ANDed or ORed.
>>
>> *1. Formal verification for completeness tests. *
>>
>> This capability allows for the description of operational properties
>> where data values (e.g,, value of an addr_bus) must be saved in one property
>> statement and then compared in a concurrent property statement. Allowing
>> this coding style is needed for completeness check. See "Complete
>> Functional Verification" Joerg Bormann
>> http://fmv.jku.at/fmcad09/slides/bormann.pdf
>>
>>
>>
>> *2. More easily write assertions where concurrent processes are needed to
>> be expressed. *
>>
>> Consider this example:
>>
>> With a "go" the machine performs a one word transfer into memory from a
>> bus interface. Machine has pipeline registers . In this transaction, there
>> are four concurrent operations:
>>
>> 1) The *go* operation that may have information about the address of
>> where to store the data *// call this P_go*
>>
>> 2) The CPU DMA control stuff *// Call this property P_cpu*
>>
>> 3) The bus interface that feeds the data *// Call this property P_if*
>>
>> 4) The data transfer into the memory (maybe some cache involved) *// Call
>> this property P_mem*
>>
>>
>>
>> In straight SystemVerilog, one can use concurrent tasks with the
>> fork/join; each task has the capacity to write/read module variables. For
>> SVA, I can write this assertion as:
>>
>> *property* P_machine;
>>
>> *automatic* *int* v_data; // holds data from bus to be sent to
>> memory.
>>
>> *automatic* *int* v_addr; // holds the size of the dma transfer
>>
>> P_go *implies* P_cpu *and* P_if *and *P_mem;
>>
>> *endproperty* : P_cpu_dm_bus
>>
>> aP_machine
>>
>>
>>
>> Expanding this hypothetical machine, for demo as I am doing this on the
>> fly:
>>
>> This machine has pipeline registers. the *addr *module variable is held
>> for 1 cycle.
>>
>> *module* m;
>>
>> *int* addr, dma_reg, bus_data;
>>
>> *logic* go, start_dma, dma_enb, bus_sve_data, mem_wr;
>>
>> *property* P_machine;
>>
>> *automatic* *int* v_data; *// holds data from bus to be sent to memory
>> *.
>>
>> *automatic* *int* v_addr; *// holds the address of the memory*
>>
>> ((go, v_addr=addr) ##1 start_dma) *implies* // P_go, addr is
>> held for 1 cycle in module
>>
>> (##2 dma_reg==v_addr ##1 other_stuff) *and* // P_cpu,
>> the dma saves this address
>>
>> (##[3:10] (bus_save_wr, v_data=bus_data) ##1 other_stuff2) *and *//
>> p_if, interface data save
>>
>> (##[3:11] dma_enb ##1
>>
>> mem_addr==v_addr && mem_data==v_data && mem_wr); //
>> P_mem
>>
>> *endproperty* : P_machine
>>
>>
>>
>> The language must be flexible enough to allow use of it in a variety of
>> ways. This this case, writing operational properties in the style of
>>
>> *antecedent implies consequent* // This is the IEEE 1800-2009
>> "implies"
>>
>> was shown to be very useful in formal verification. Of course, the "*
>> implies*" is nothing more than "not(P1) or (P2)", and local variable of P
>> do not flow from P1 into P2.
>>
>> This is a language limitation. Your examples suggest a different coding
>> style. But that is not the point.
>>
>>
>>
>> There might be other cases where a user want to use local variable used in
>> sequences/properties that are specified with "*and/or/intersect/implies*"
>> operators. Section 16.10 goes to great lengths to explain the flow out of
>> local variable in such cases. But I strongly believe that SVA needs to have
>> local variables must *flow in* (or flow into) property/sequence
>> statements, with the restrictions that I mentioned in mantis 3195<http://www.eda-stds.org/svdb/view.php?id=3195>.
>>
>>
>>
>>
>> Currently, the only workaround is to copy the desired value into a module
>> variable using a task from within the sequence match item using a task or
>> function, and then ping-ponging the value of that module variable into the
>> local variable of the other property. See property *P_ok* in my
>> proposal.
>>
>>
>>
>> OK John, I can almost hear you say: why not write your machine example in
>> this other way ...
>>
>> Now, you're forcing a style on me. Also, in that machine, I have pipeline
>> regs, and the assertions checks that data from the bus is correctly written
>> into the memory. I want to have the option to write the assertion in that
>> style. Again, formal verification needs this feature to ease the
>> computation of completeness.
>>
>> Ben
>>
>>
>>
>> On Thu, Sep 2, 2010 at 3:41 PM, Havlicek John-R8AAAU <
>> r8aaau@freescale.com> wrote:
>>
>>> Hi Ben:
>>>
>>>
>>>
>>> I don’t see the compelling motivation for this proposal.
>>>
>>>
>>>
>>> property P_illegal;
>>>
>>> int v_t1;
>>>
>>> ((a, v_t1=data) ##1 b) implies // cause, v_t1 can be read in LHS
>>>
>>> (##1 d==v_t1); //effect, v_t1 cannot be read in RHS
>>>
>>> endproperty : P_illegal
>>>
>>>
>>>
>>> can be written legally today as
>>>
>>>
>>>
>>> property P_legal;
>>>
>>> int v_t1;
>>>
>>> ((a, v_t1=data) ##1 b) |-> // cause, v_t1 can be read in LHS
>>>
>>> d==v_t1; //effect, v_t1 can be read in RHS
>>>
>>> endproperty : P_legal
>>>
>>>
>>>
>>>
>>>
>>> Similarly,
>>>
>>>
>>>
>>> property P_race;
>>>
>>> automatic int v;
>>>
>>> (a, v=data) ##[1:3] b) implies
>>>
>>> (c==v ##2 d);
>>>
>>> endproperty : P_race
>>>
>>>
>>>
>>> can be written legally today as
>>>
>>>
>>>
>>> property P_no_race;
>>>
>>> int v;
>>>
>>> (a, v=data) |->
>>>
>>> (
>>>
>>> (##[1:3] b) implies
>>>
>>> (c==v ##2 d)
>>>
>>> );
>>>
>>> endproperty : P_no_race
>>>
>>>
>>>
>>>
>>>
>>> Best regards,
>>>
>>>
>>>
>>> J.H.
>>>
>>>
>>>
>>>
>>>
>>> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
>>> cohen
>>> *Sent:* Thursday, September 02, 2010 2:40 PM
>>> *To:* sv-ac@eda.org; Korchemny, Dmitry; Eduard Cerny
>>> *Subject:* [sv-ac] Re: [SV-AC] Local Variables Flow Out Issue in
>>> and/or/intersect/implies
>>>
>>>
>>>
>>> Update the file in http://www.eda-stds.org/svdb/view.php?id=3195 , and
>>>
>>> Added:
>>> "The local variable shall not be read in the same cycle it is written. "
>>>
>>> [Ben] I believe that there would be a race condition because one property
>>> can write a value to the local variable while a concurrent property reads
>>> the property. For example:
>>> property P_race;
>>> automatic int v;
>>> (a, v=data) ##[1:3] b) implies
>>> (c==v ##2 d): // This consequent may be processed before the
>>> antecedent.
>>> endproperty :P_race
>>>
>>>
>>>
>>> On Wed, Sep 1, 2010 at 6:47 PM, ben cohen <hdlcohen@gmail.com> wrote:
>>>
>>> However, there is a need to be able to set and read local variables in
>>> one sequence or property (the LHS), and to read those local variables in
>>> another sequence / property (RHS).
>>>
>>> Please see http://www.eda-stds.org/svdb/view.php?id=3195
>>>
>>> I uploaded a proposal.
>>>
>>> Ben Cohen
>>>
>>>
>>>
>>> --
>>> This message has been scanned for viruses and
>>> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and
>>> is
>>> believed to be clean.
>>>
>>
>>
>

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