Subject: Re: Temporal e
From: David Van Campenhout (dvc@verisity.com)
Date: Wed Jul 11 2001 - 07:46:22 PDT
Bernard Deadman writes:
> At 03:45 PM 7/10/2001 -0700, David Van Campenhout wrote:
>
>
> >2. Your specific concern with 45.2 appears to be that we have a property
> > of the form
> >
> > expect p45_2 is @a => @b;
> >
> > , and that the event definitions of 'a' and 'b' reveal that the match
> > of @a and the match of @b must 'start' at the same cycle. You were
> > expecting that there were no overlap between the subsequence over which
> > @a succeeds and that over which 'b' succeeds.
> >
> > It turns out, however, that the definition of b is of the form:
> >
> > event @b1 is t1;
> > event @b2 is t2;
> > event @b is {t1;t2};
> >
> > (t1 and t2 are temporal expressions).
> >
> > and that the nature of t1 is such that if @a holds then @b1 holds too,
> > and that the nature of t2 is such that it does not overlap with t1.
> > Then p45_2 is equivalent to
> >
> > expect p45_2_prime is @a => @b2;
> >
> > In p45_2_prime overlap between the match of @b2 and @a is no longer
> > required.
> > (Sorry for the handwaving, but ....)
> >
> > Also note that the the definition of @a and @b both start with
> > @frame_fall. Together with the @frame_assr and (fail @frame_chng)
> > terms, this will ensure that the dataphas (@a) and the targetabort
> > (@b) belong to the same transaction.
>
> If I understand you correctly, you are arguing the property can be handled
> by a Formal Model checker if @a == @b1, and I wouldn't dispute that. The
> problem is in this case they are not obviously the same which makes for a
> lot of issues when building tools to handle this without user intervention.
You misunderstood. Whatever set of event definitions, assume
declarations, and expect declaration the user expresses, we can
translate into sets of finite automata and Buechi automata, and
therefore model check.
>
>
> > User defined events allow the user to decompose complex properties
> > and raise the level of abstraction. On the other hand the
> > definitions must be chosen with care, since we can only observe
> > the point where an event succeeds -- the starting point of the
> > sequence over which the event succeeds is not visible. Prop 45.2
> > illustrates how users cope with this concern.
>
> Don't misunderstand me. I certainly believe in the expressiveness of your
> event based solution, the only problem I have is with how many properties
> can actually be supported directly, as written by any Formal Model checker
> that exists at present. And I'm something of a pessimist in this respect,
> because I figure that if I can find examples that can't be handled
> automatically there are a lot more out there I haven't seen.
>
> My conclusion is therefore the user has to use a sub-set of the features of
> temporal 'e' if he anticipates his properties being used for Formal
> Verification, and what I'm attempting to understand the boundary of the
> sub-set today. Incidentally there are many precedents for this, most
> obviously the synthesis sub-set of Verilog.
>
>
> >Hope this helps. Otherwise, I'd be glad to continue our discussion
> >next week in Paris.
>
> I think the whole subject of how one language can be used in both Formal
> and simulation-based verification this is an area everyone ought to be
> considering because I can see the opposite issue arising from supporting,
> for example, the "forall" construct in Sugar in a simulation environment.
>
> No doubt we can talk about this on Tuesday, though I think I am slowly
> getting my mind around the issues associated with 'e'.
>
> Thanks
>
> Bernard
This archive was generated by hypermail 2b28 : Wed Jul 11 2001 - 07:46:58 PDT