Subject: Re: Temporal e
From: Bernard Deadman (bdeadman@sdvinc.com)
Date: Tue Jul 10 2001 - 11:37:48 PDT
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?
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
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,
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 Jul 10 2001 - 11:41:32 PDT