Subject: Re: Temporal e
From: David Van Campenhout (dvc@verisity.com)
Date: Tue Jul 10 2001 - 15:45:44 PDT
Bernard:
1. The properties 45.X were taken from a larger set of properties that
attempted to cover the complete PCI spec. In the methodology we
promote, users describe the elements of their protocol by defining
events. This raises the level of abstraction. The properties of the
protocol are then expressed in terms of the events rather than the
raw propositions.
An artifact of the methodology is that if each property is
scrutinized in isolation, the events appearing in the property may
not always be completely tailored to the property. The event
definitions may contain parts that appear redundant with respect to
the property in isolation.
So, if we defined target_abort as:
event target_abort is { @frame_fall; {[..] * fail @frame_chng;
@devsel_fall}; {[..] * fail @devsel_chng; (@devsel_chng and
@stop_fall)} }@qclk;
It was the writer's understanding that the event requires an ongoing
transaction, hence the first term of the defining sequence is
@frame_fall.
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.
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.
> At 08:13 AM 7/10/2001 -0700, David Van Campenhout wrote:
>
>
> >We can translate any property + set of constraints formulated in
> >temporal e so that it can be model checked with SMV.
>
>
> David,
>
> I've seen this claim several times and I still can't get my mind around
> it. I have separately sent a message to Yaron Kashai about the same
> subject, but maybe you can help me understand this. Forgive me but I'm not
> an expert in Formal Verification and SMV, but all of the examples I've seen
> are based on simple implications, ie "if A happens then it must be
> followed by B"
>
> If we take property 45.2 as an example, we find in Sugar:
>
>
> define target_abort := rose(devsel_) & fell(stop_);
> define io_cmd := PCI_BE(3..0) in {IOREAD, IOWRITE};
> define byte_enable_mismatch := (current_trans_ad(1..0)=1 & PCI_BE(0)!=1b) |
> (current_trans_ad(1..0)=2 & PCI_BE(1..0)!=11b) | (current_trans_ad(1..0)=3
> & PCI_BE(2..0)!=111b);
> define disconnect := !devsel_ & !stop_;
>
> AG {(fell(frame_) & io_cmd), byte_enable_mismatch} (target_abort before
> (!trdy_ | disconnect))::clk=qclk
>
>
> Forgive me if I made a mistake, but I think the "before" operator is
> syntactic sugaring, and the real functionality is:
>
> {(fell(frame_) & io_cmd), byte_enable_mismatch} |=>
> (trdy_&(devsel_|stop_))[*], rose(devsel_) & fell(stop_) ::clk=qclk
>
>
> Similarly, in ForSpec we find:
>
> f := change_if(qclk) always io_cycle & less_significant(BE,
> current_trans_ad) -> next !frame*, target_abort;
>
> I'm suspicious of the detail here because
>
> target_abort := fall(frame), !frame*, fall(devsel), !devsel*, devsel &
> fall(stop);
>
> but leaving aside the fact I think the real requirement doesn't require so
> many references to frame and should read:
>
> f := change_if(qclk) always io_cycle & less_significant(BE,
> current_trans_ad) -> next !frame*, fall(devsel), !devsel*, devsel & fall(stop);
>
> the concept is remarkable similar to Sugar (CTL if you prefer). In both
> these cases the first part of the implication is satisfied when there is
> found to be a mis-match between the byte-enables and the address, and then
> there is a description of what should follow, starting from the next clock
> cycle and ending in the abort cycle.
>
>
> The thing I'm still puzzled about is when you look at the 'e' equivalent
> you find:
>
> expect (@io_data_phase and true( << mismatch expression >>)) => { [..] *
> @frame_assr; @target_abort }@qclk;
>
> with the events defined as:
>
> event io_data_phase is { @frame_fall and true('`PCI_BE'.as_a(PCI_COMMAND)
> in [IOREAD, IOWRITE]); ~[..] * (@frame_assr or irdy_assr); @data_phase
> } @qclk;
>
> event target_abort is { @frame_fall; {[..] * fail @frame_chng;
> @devsel_fall}; {[..] * fail @devsel_chng; (@devsel_chng and @stop_fall)}
> }@qclk;
>
>
> The thing I find difficult is the "target_abort" event starts
> *simultaneously* with the "io_data_phase" event, and not when the
> "io_data_phase" event has been satisfied.
>
> I know this is possible in your simulation environment but can you (or
> anyone else for that matter) *please* either:
>
> a) show me my understand of CTL and/or Sugar is wrong and they handle the
> situation where the right hand side of the implication overlaps the left
> hand side by a significant but unknown amount. Also, if SMV can handle
> this, does it have any impact on capacity or performance?
>
3. I think your understanding of Sugar with respect to 45.2 is just fine.
> or
>
> b) reassure me the conversion to CTL can be accomplished in *all* cases
> without further knowledge of the protocol by showing me the steps required
> to automatically convert this example from 'e' to useable Sugar / CTL
4.
- For each event declaration, i.e., event target_abort is { ... }@qclk, we
use our star-semantics tableau construction to generate a finite
automaton with a single output. At any cycle the output is true if
the corresponding event holds in that cycle. Event declarations
can be seen as a way to augment the environment. Event declarations
give the user a means to extend set of proposition symbols.
- For each assume or (expect) declaration we use our omega-semantics
tableau construction to generate a Buechi automaton for the
corresponding (negated) temporal experssion. If the temporal expression
depends on user-defined events, the Buechi automaton will take the
output signals of the finite automata that compute the events as input.
- At this point it is straightforward to use SMV to model check the
property+constraints.
>
>
> Without this my fear is should the committee endorse 'e' we could end up
> with users being able to write properties that cannot be handled by any
> Formal Model checker that exists.
>
> Thanks in advance for showing me where I am wrong,
>
Hope this helps. Otherwise, I'd be glad to continue our discussion
next week in Paris.
David
This archive was generated by hypermail 2b28 : Tue Jul 10 2001 - 15:46:26 PDT