RE: [sv-ac] subroutines attached to sequences

Hi Doron,

Thx for the discussion, some more comments I have.

1) I initially dismissed property layer because we were discussing
merits of actions in sequences and how to interpret. But actually the
fact that the "top" property layer blocks flows kinda goes to validate
the bigger notion I am putting forth -- visibility/hiding/encapsulation.
Properties encapsulate sequence (layers) within and hide all their
internals. If I want to execute an action I put it inside some sequence
*layer* and it executes at *that layer* (loose approach). Indeed another
way to look at this discussion is build a hierarchy of sequence layers,
does it make sense for upper layer to circumvent lower layers in an
implicit way (I mean the default) ? Seems easier/cleaner to move action
to upper layer.

In essence my argument: An action somewhere really means execute there
(loose) and cannot be circumvented by the upper layer context (as tight
does). The "tight" interpretation can be mimic-ed by storing all actions
(at "lower" layer) then "joining"/"resolving" them (at "upper" layer).

2) ok.

3) Doron if goal is to get a mimic for "R under tight approach", then
this is same as (2) I believe, just store action (myZ = Z) and issue
after join.

** Summary: "The main problem in the loose approach is, that some
redundant threads may run more than we want them to run, causing both
computational overhead, and redundant actions."

Agreed, I think:
- computational overhead: This is a tool issue and should not be
defined, LRM should only make sure that the semantics (user intent) is
preserved. Tools can shortcut of course -- the "right way" provided
action placement allows it. 
- redundant actions: (by default) User responsibility to move to upper
sequence layer. Otw they really mean to say evaluate/track more. [BTW
this is nothing new, this is how debug works, in loose interpretation
the user action is an extra instrumentation forcing data collection
there and limiting optimization.]

** Suggested Goal of proposal: Have the best of both worlds. 

Doron, I think we're just discussing the default, likely adding some
hint to force one or other is a given for user/tool flexibility. The
default should be able to "simulate" both behaviors with some kind of
rewrite, otherwise we're losing something we can't recover.

Thx.
-Bassam.

--
Dr. Bassam Tabbara
Synopsys, Inc.
(650) 584-1973

-----Original Message-----
From: Bustan Doron-DBUSTAN [mailto:doron.bustan@freescale.com] 
Sent: Tuesday, February 28, 2006 7:12 AM
To: Bassam Tabbara
Cc: sv-ac@eda.org
Subject: RE: [sv-ac] subroutines attached to sequences


Hi Bassam,

I am still not convinced.

> 1) I don't think is relevant to discussion

Consider the property:

(
  (
     a ##1 (a,Z) ##1 a |-> b
  and
     c |-> d[*3]
   }
or
   e |-> f [->1] ##1 !f
)

suppose that 'a', 'c', 'e' hold at the first cycle, 'a' also holds on
cycles 2, 3, 'd' does not hold at cycles 1,2,3, and 'f' holds at cycle 5
for the first time.

Then, according to the loose approach, Z should be execute, but
according to the tight approach, Z should not be executed. Since you
cannot join properties, you cannot mimic the tight approach in the way
you suggested

> 2) Easy to add a new var to store  .... ##1 (1, myv = v) .... Z(myv)

I agree

> 3) R under loose already does the action (1, Z) in this case loose is 
> default so don't need to rewrite.

I guess I was not clear. In the example I gave, I claimed that R under
the tight approach is not mimicked by R' under the loose approach. Since
you

suggest to mimic R by R', this leads to a contradiction.

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

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

R' under the loose approach does not mimic R under 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.

___________________________________________________________

The main problem in the loose approach is, that some redundant threads
may run more than we want them to run, causing both computational
overhead, and redundant actions.

Consider for example the following property that displays all the
packages that were missed from the time the system crushed until it has
been recovered, Then the property requires the update signal to be high
before the signal ready is high. 

crushed |->
(
    (pack_arrived [->1], $display("missed package - %0d",
package_id))[*0:$] intersect
     !recover [*1:$]
)
##1
recover
##0
(!update && ! ready)[*0:$] ##1 (!ready && update);

Then by the loose approach, the sub sequence (pack_arrived [->1],
$display("missed package - %0d", package_id))[*0:$] will be evaluated
until the end of the evaluation of the overall property.
Meaning until the update signal is high. Thus ,there will be extra
messages for the packages that arrived from the time recover is high
until the time update is high.



then 








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