Subject: Re: Synchronous properties in temporal 'e'
From: Yaron Kashai (yaron@verisity.com)
Date: Thu May 03 2001 - 08:46:26 PDT
Bernard and all,
There are quite a few issues here, I hope I have addressed
them all in the embedded text.
I suspect we may have created a bit of a confusion, so here is
an executive summary for the benefit of those who won't dive
into the details:
1) Temporal e is a synchronous language, like the other proposed
languages.
2) Any synchronous language interacting with an event based
simulator needs a mapping from the discrete event model to
the synchronous model.
3) This mapping is done in e via the sampling operator.
For details, please see below.
Bernard Deadman wrote:
>
> At 03:14 PM 4/24/01 -0700, Yaron Kashai wrote:
>
> Yaron,
>
> Sorry about the delay in responding, however I hit a mountain of work that
> had to be completed by the end of April.
>
> You wrote :
>
> >I disagree. This relates to the discussion we had over computational
> >models. The source of time is the model under verification and not
> >the property language. If the model is an event based model, executed
> >by a simulator, then e events may occur in an asynchronous manner.
> >If the model is a synchronous model, such as a cycle based simulation
> >or a CTL style model checker, the e events will occur on the
> >synchronous clock tick.
>
> and later you wrote
>
> >NO. When the model under verification is synchronous, all e events
> >are synchronous. No mapping is needed.
>
> therefore I believe your argument is if the user were to write in a
> synchronous style when he was intending his properties to be used in a
> synchronous Formal Model Checker, the semantics are easy to understand,
> while he could write more flexibly using all the features of temporal 'e'
> if he was targetting an event based simulation environment.
>
> I think I can understand this so I hope my interpretation is correct?
I can't think of a single operator that's available for event
based simulators but not for, say, cycle based. Therefore I'd
rather say that the user must refrain from using a small number
of operators if she targets traditional model checkers - an
example would be the delay() operator, or exec {}.
I don't think there are different "styles" for temporal e, like
you suggested.
>
> >The sampling semantics ensure that the evaluation of temporal
> >expressions are always within a synchronous framework. In an event
> >based simulation, the synchronous tick is the disjunction of all
> >events that are taken directly from the simulator (without sampling).
> >This unification of semantics over different time domains is
> >important: it allows the same properties to be checked against
> >event based models, cycle based simulated models and model checking.
> >This is done in practice often enough.
>
> One of the 'e' features I value is the greater flexibility to, as you put
> it, use "the same properties ... against event based models, cycle based
> simulated models and model checking" and I see this as an essential trend
> in verification methodologies, but the concern I have is still over what
> you term "the unification of semantics" because I believe re-use of one
> property set is critical to efficiency.
>
> I think 'e' offers a great opportunity in this area but to maximize this, I
> think the author should be free to write properties using any features of
> the language and the tools should automatically adapt in more restrictive
> environments such as our cycle-based simulation application, or in a
> synchronous Formal Model checker.
>
> I know there are many occasions when I fail to see obvious answers, but
> having the tool handle the "unification" looks far from trivial to me. Is
> there anyone else out there who has looked at this issue? Can someone help
> me recognize my concern is unfounded?
>
> I assume this is an area Verisity has been researching, therefore will you
> publish information on this unification as part of the release of temporal
> 'e'? Or will we have to figure this out for ourselves if the committee
> opts for 'e'? If the committee opts for 'e', must the "unification of
> semantics" become a part of the language specification?
Unifying the semantics is achieved by using a consistent computational
model for all environments. This computational model is synchronous
in nature, so it requires some mapping from an event based simulation
model.
I believe I have described how that mapping is done in principle.
Here is a short recap:
1) A small number of events are taken directly from the simulation.
these are denoted by sampling @sim. An example would be:
event sys_clk is rise('/top/clk')@sim;
2) The disjunction of these events defines the synchronous tick,
or the "fastest clock" called any.
3) All other temporal expressions are sampled by an event, creating
a closure. This results in a system where all transitions are
simultaneous with "any".
I don't think there is anything more to it as far as the language
semantics are concerned, so I'm not sure that further disclosure
is necessary. Anyway, the intention is to provide all the semantic
information to the committee - not to make people figure it out
for themselves, so if there are questions - please let me know.
>
> >There are some features that are intended for a dynamic environment,
> >such as the ability to embed imperative code within a temporal
> >expression. These should not be considered for model checking.
>
> I am intrigued by "the ability to embed imperative code within a temporal
> expression" because it seems to have relevance in our application. Is this
> a feature of the temporal subset or is it only available in "full" 'e'?
I meant the exec statement, which is part of temporal e but only
applies to simulation. For example the sequence:
{ @A; @B exec { print foo; }; @C }
Will cause the imperative clause "print foo" to execute when event
B succeeds in the sequence. The imperative code we support is e
of course, but this feature could be preserved and allow Verilog
code for instance.
>
> Finally, I noticed the following comment today from Adam Krolnik on the
> Verification Guild
>
> ~~~~~~~~~~
> One design flaw is that the temporal expression sequence operation {;} does
> not handle the degenerate case of 0 clocks between the sequence of items.
> The implication operator => thus suffers from this flaw due to it's
> definition: TE1 => TE2 === (fail TE1) or {TE1; TE2} E.g. The temporal
> expressions for:
> "A and then B within the next 1 to 4 cycles"
> {A; [..3]; B}
> "A and then B within the next 0 to 4 cycles"
> A&&B or {A;[..3]; B}
>
> differ more than just the 0/1 difference. It would have been better for
> these to be the same, except for the number, E.g.
>
> A -> B {1:4}
> A -> B {0:4}
> ~~~~~~~~~~
>
> Is this structural to the language, or can it be 'fixed' if the committee
> opts for temporal 'e'? And if it is 'fixed' what will happen to existing
> Verisity users?
>
I must disagree with Adam's position. In a nutshell Adam argues
that { @A; [0] ; @B} should be equivalent to {@A and @B}. This
is wrong. Here is a list of expressions and satisfying sequences:
<A,_,_,B> |= { @A; [2]; @B}
<A,_,B> |= { @A; [1]; @B}
<A,B> |= { @A; [0]; @B}
<A,B> |= { @A; @B }
I hope it is obvious that the behavior of [0] (AKA epsilon) is
consistent, and is not a "design flaw".
> On a related subject, the temporal extensions to OpenVera allow negative
> (ie prior) time so that you can define sequences to overlap. I can see a
> limited value to this in some circumstances, though so far there has always
> been another, often less elegant, way to define the property. Is there any
> structural reason why this flexibility couldn't be adopted in temporal 'e'
> if it proves essential?
If I understand correctly, this will allow, e.g. [-1] such
that {@A; [-1] ; @B} is equal to { @A and @B } - this will make
Adam happy. The special case -1 is really fusion, which exists
in other languages - even in Sugar, I think.
The general case requires some additional thought. As long as
the negative parameters are limited to constants, this may be
feasible. I'm very skeptical about being able to handle variables,
in particular unbounded ones that may go back in time before the
start point of the formula.
>
> Thanks,
>
> Bernard
>
> ====================================================================
> SDV Inc. 9111 Jollyville Rd, Suite 102, Austin, TX 78759 USA
> Phone: (512) 231-9806 xt 101 FAX: (512) 231-9807 Mobile: (512)
> 431-5126
> Email: bdeadman@sdvinc.com Website: www.sdvinc.com
Thanks again for all the interest and the good questions.
-- yaron
This archive was generated by hypermail 2b28 : Thu May 03 2001 - 08:51:15 PDT