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

  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.