Subject: the importance of events in temporal 'e'
From: Bernard Deadman (bdeadman@sdvinc.com)
Date: Tue Apr 24 2001 - 12:24:26 PDT
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
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?
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).
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 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?
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?
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
This archive was generated by hypermail 2b28 : Tue Apr 24 2001 - 12:27:45 PDT