Subject: Synchronous properties in temporal 'e'
From: Bernard Deadman (bdeadman@sdvinc.com)
Date: Wed May 02 2001 - 13:06:07 PDT
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?
>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?
>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'?
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?
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?
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
This archive was generated by hypermail 2b28 : Wed May 02 2001 - 13:09:38 PDT