RE: [sv-ac] Re: The "forall" construct for sva // a possibility?

Hi Ben,

Checking that restriction could be rather difficult. Also, the variables in or branches are separate copies. Your example can be easily rewritten using |-> and it would show clearly that the reading of the variables can only happen after they have been assigned.

ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Tuesday, August 03, 2010 2:18 AM
To: Korchemny, Dmitry; sv-ac@eda.org
Subject: [sv-ac] Re: The "forall" construct for sva // a possibility?

I had a request to have the local variables being shared and visible by each of the threads of an OR operator.
The issue I see with the local variables being shared by the threads of the ORing is the value to be assigned if each thread assigns to the local variables. However, we could put a restriction that the local variable cannot be assigned in the same time step.
Thus,
property P;
 int v1;
 ((a, v1=b) ##1 c) OR (#2 d==v1);
endproperty :P
This style would allow you to better describe timing diagrams with the implies operator. example

property p_write;
 int v_addr, v_data;
 logic v_parity;
  ((go, v_addr=addr, v_data==data) ##1 v_parity=f_parity(v_data)) implies
   (##2 wr && wr_data==v_data && wr_addr=v_addr && parity==v_parity;
endproperty :p_write
This is currently illegal since each sequence of an OR operator produces its own thread that can get carried through to the next step, such as an end point (no more continuity), concatenation with another sequence, or as antecedent to a consequent.

If we want to keep the current rule on the OR operator, we could add a "forall" to specify this sharing of local variables.
Ben

On Mon, Jul 26, 2010 at 10:08 PM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Hi Ben,

I think that rand const does the work.

Regards,
Dmitry

From: ben cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Monday, July 26, 2010 6:43 PM
To: Korchemny, Dmitry
Subject: The "forall" construct for sva // a possibility?

Dmitry,
I just had a request for a "forall" construct for sva.
Do you see a possibility? The forall does iterations.
Something like psl.
Thanks,
Ben

---------------------------------------------------------------------

Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for

the sole use of the intended recipient(s). Any review or distribution

by others is strictly prohibited. If you are not the intended

recipient, please contact the sender and delete all copies.

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