Subject: Re: the importance of events in temporal 'e'
From: Yaron Kashai (yaron@verisity.com)
Date: Tue Apr 24 2001 - 15:14:13 PDT
Bernard and all,
Thanks for the questions. Please see my embedded comments:
Bernard Deadman wrote:
>
> Yaron,
>
> First I should acknowledge that you have given me additional information
> and examples beyond the material presented in the last meeting. I am
> phrasing this question using the material from your presentation for the
> benefit of the entire group and hope I am not accidentally breaking the
> terms of the NDA I have with Verisity.
>
> I sympathize with the problems you encountered in portraying a language
> over the phone to a group of people spread out across the World but it
> seems from the examples that "events" are the key to temporal 'e'. My
> understanding is a typical verification strategy would be to define a
> number of "events", then to create an assertion that if eventA happens it
> must be followed by eventB. You seem to express this as:
>
> expect assertion_name is @ eventA => eventB @ sampling_event
Indeed, the usage of events as building blocks goes a long way
toward simplifying the properties. It is a typical usage style
for the language.
>
> As an example, we can consider page 12 of your presentation
>
> assertion_name == pci_spec_8
> eventA == frame_fall
> eventB == { [..7] ; @ irdy_assr }
> sampling_event == qclk
>
> therefore
>
> expect pci_spec_8 is @frame_fall => { [..7] ; @ irdy_assr } @qclk
>
> If this understanding is correct, the example on page 14 is for an "event"
> and in itself does not perform any verification. Is this correct?
Yes, this observation is correct.
>
> The problem I am wrestling with is the "events" around which temporal 'e'
> is structured don't need to be from a single clock domain, indeed I believe
> they could be equivalent to Verilog posedge or negedge transition of a
> signal (see the use of "any" on page 6).
I'm afraid you are taking this a bit too far. Events are monitors
that augment the model under verification. They could be thought
of as state machines added to the model.
>
> This seems to be fundamentally different from Formal Verification languages
> such as CTL & LTL & super-sets such as Sugar, which I believe were
> initially developed to check FSM's that are inherently synchronous. I
> believe all Formal Model Checking engines to date have been built with the
> expectation of a single sampling clock, indeed I think there was an earlier
> discussion within the committee which revolved around verification using a
> single clock which would be either the fastest or a product of multiple clocks.
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.
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.
>
> I can see the value of your event based language within a simulation
> environment however, when looking at the possibility of using temporal 'e'
> in our applications, I can see we would need to 'map' the event based
> structure of temporal 'e' to a single clock domain description for the
> analysis we perform. I believe this is would also be necessary before
> using these assertions in a Formal Model Checking engine though I am sure
> other members will correct me if this is not the case!
>
> My question (sorry it's taken so long to get there!) is
>
> 1) do you agree this mapping would be required for the adoption of temporal
> 'e' within the group of applications we are discussing? Or is there some
> way to avoid mapping for Formal Model Checking?
NO. When the model under verification is synchronous, all e events
are synchronous. No mapping is needed.
>
> 2) if it is essential has anyone proven an algorithm that performs this
> mapping? If so, does it have coding style limitations such as requiring a
> single clock, or is it more flexible?
>
> 3) does this imply that Formal Model Checking could be performed using a
> subset of temporal 'e' while the wider facilities of the language could be
> used for simulation-based checks?
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.
In general, the subset of features that apply depend on the
capabilities of the model checker. For instance, most model checkers
can't deal with real time delays (which can be expressed in e
using delay(n)), but there are some that can...
>
> Thanks for your help,
>
> 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
Best regards,
-- yaron
__________________________________________________________________
Yaron Kashai mailto:yaron@verisity.com
Director of Research cell: +1 (408) 203 4481
Verisity office: +1 (650) 934 6855
http://www.verisity.com
This archive was generated by hypermail 2b28 : Tue Apr 24 2001 - 15:17:11 PDT