Subject: Overlapping sequences in temporal 'e'
From: Bernard Deadman (bdeadman@sdvinc.com)
Date: Thu May 03 2001 - 13:38:21 PDT
At 08:46 AM 5/3/01 -0700, Yaron Kashai wrote:
Yaron,
Thanks for your response.
I am afraid I am still not clear about event to cycle-based mappings, but I
think the best solution may be to take one of the PCI examples and try to
code it in an extreme but (hopefully!) legal form. Hopefully by working
through the example you can show me the problem is all in my head though I
guess it's going to take a couple of days to prepare the example.
Meantime,
> > ~~~~~~~~~~
> > 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?
> >
>
>I must disagree with Adam's position. In a nutshell Adam argues
>that { @A; [0] ; @B} should be equivalent to {@A and @B}. This
>is wrong. Here is a list of expressions and satisfying sequences:
> <A,_,_,B> |= { @A; [2]; @B}
> <A,_,B> |= { @A; [1]; @B}
> <A,B> |= { @A; [0]; @B}
> <A,B> |= { @A; @B }
>
>I hope it is obvious that the behavior of [0] (AKA epsilon) is
>consistent, and is not a "design flaw".
My reading of the question was Adam was asking for an overlap, ie his event
B might occur as early as the same sampling clock period as A is satisfied,
I think he was arguing that "A and then B within the next 1 to 4 cycles"
can be satisfied by
A,_,_,_,B
A,_,_,B
A,_,B
A,B
and can presumably coded as
expect spec_1 is @A => { [0..3]; @B } @my_clk
He would like "A and then B within the next 0 to 4 cycles" to be satisfied by
A,_,_,_,B
A,_,_,B
A,_,B
A,B
A&&B
though he says it has to be coded using
A&&B or { [0..3]; @B }
I confess I can't see how to write this as part of an 'expect'! Is it
legal to write the following?
expect spec_1 is (@A && @B)
or (@A => { [0..3]; @B }) @my_clk
When you cut through the syntax issues, I think the real problem is the
semantics of the => 'yield' expects the right hand side sequence (event) to
start one cycle after the left hand side sequence (event) is satisfied
which is why
expect spec_1 is @A => { [-1..3]; @B } @my_clk
might satisfy his requirement.
Is it essential for the semantics of 'yield' to assume the next cycle or is
there some way around this?
Is there a more elegant way to support sequence overlaps in 'e' if the
language were to be adopted?
>The special case -1 is really fusion, which exists
>in other languages - even in Sugar, I think.
This seems to be why Sugar / CTL contains the ~ concatenation and so many
"while", "within" etc operators to support overlaps.
>The general case requires some additional thought. As long as
>the negative parameters are limited to constants, this may be
>feasible. I'm very skeptical about being able to handle variables,
>in particular unbounded ones that may go back in time before the
>start point of the formula.
In my opinion the general case of negative (ie prior) times as
(apparently!) supported by Open Vera poses a bunch of problems but delivers
little real value. Not the least of the problems will be the need for a
*LOT* of speculative processing and consequent simulation performance
degradation in extreme cases. Limiting evaluation of the right hand side
until the left hand side starts isn't necessarily a perfect solution either
though maybe the property list being compiled will reveal whether this is
adequate or not.
Thanks again 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 : Thu May 03 2001 - 13:42:02 PDT