Re: [sv-ac] subroutines attached to sequences

Hi Bassam,

I disagree with the assumption that the tight approach can be mimicked 
by the
loose approach by moving it after the join, for the following reasons:

1. On the property level, joins are not defined.

2. For sequence intersect, we may loose the ability to use the local 
variables.
    For example  for signals a,b,c , lvar v, and action Z(v), if we have
    R =
    (1, v=1)
    ##1
    (
           (a ##0 (1, v = 2) ##1 (1, Z(v)) ##1 b)
    intersect
           ((c ##0 (1, v = v+1)) [*3])
    ),
 
    The sequence 
     R' =
    (1, v=1)
    ##1
    (
           (a ##0 (1, v = 2) ##1 1 ##1 b)
    intersect
           ((c ##0 (1, v = v+1)) [*3])
    ) ##0 (1,Z(v)),
  
    is not legal because v does not flow out of the intersection

3. In cases like

    R =
    ##1
    (
           (a  ##1 (1, Z) ##1 b)
    intersect
           (c [*3])
    ),
 we can write

    R' =
    ##1
    (
           (a  ##1 1 ##1 b)
    intersect
           (c [*3])
    ) ##0 (1, Z),

but it does not mimic the  tight approach. To see that consider a 
computation
that satisfies c at the first 3 cycles, satisfies a on the first cycle, 
but does not satisfy
b on the third cycle. Then Z should be executed in R according to the 
tight approach,
bur should not be executed in R' according to the loose approach.

Regards

Doron





Bassam Tabbara wrote:

>Hi Doron,
>
>Actually in retrospect, when I raised lvars my intent was to analyze why
>this issue has percolated up for subroutines and was not apparent before
>for local vars. I think it's because the subroutine call -- assume for
>now it is $display, argument applies to others-- intrudes on the
>subsequence and forces visibility inside whereas before we were content
>in treating the lvar assignments "local" to thread path and only
>referencing after join -- effectively leaving the visibility function to
>a) evaluation (decides to shortcut or not may be based on user input
>...), b) debug keeps track of data (optionally glitching) within (if
>recorded). It really did not matter to "outside" ... Data could only
>propagate outward after the join.
>
>That said in my opinion we should keep LRM flexible and adopt the loose
>approach -- meaning treat this action loosely just like we effectively
>did for lvars (also when LRM describes composition operators). The tight
>interpretation can be mimic-ed by user putting the action after the join
>not inside. Moreover, the loose approach of course minimizes context
>dependence of sub-evaluation -- good for both evaluation and also user
>analysis/debug -- and still maintains users' ability to model all
>situations since it's more general.
>
>** So in my mind, putting an action inside is requesting visibility
>inside and making this sub-evaluation observable to the outside ...
>rather *preventing* evaluation from shorting. Now, beyond a $display, a
>truly actionable task is also better done for every sub-match and not
>shorted ... If users wished to do a shortcut (aka tight) they can store
>the data within sub-evaluation and add a "join action" after the join
>(aka composition).
>
>We can decide to add some pragma/keyword/operator (variants) later but
>first we should agree on the default underlying interpretation in LRM --
>I argue loose. BTW we should also recommend that users put a %m in
>$display raising an issue to tackle -- scoping inside assertion ...
>
>Thx.
>-Bassam.
>
>
>--
>Dr. Bassam Tabbara
>Synopsys, Inc.
>(650) 584-1973
>
>-----Original Message-----
>From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of
>dbustan
>Sent: Saturday, February 11, 2006 1:11 PM
>To: sv-ac@eda.org
>Subject: [sv-ac] subroutines attached to sequences
>
>Here are two examples with local variables, I don't see where the
>problem is.
>
>  
>