Subject: Re: Overlapping sequences in temporal 'e'
From: Yaron Kashai (yaron@verisity.com)
Date: Mon May 07 2001 - 08:59:58 PDT
Bernard,
I think I understand your point about the yield operator.
> 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
Actually, the way to write this is as follows:
expect spec_1 is (fail @A or {@A and @B}) or (@A => {[..3]; @B})
Which is admittedly a bit clumsy. I'd like to offer the observation
that causal systems typically require a delay between the cause and
the effect, but I can think of cases where such immediate
relations may be of use.
It is easy enough to define an "imply" operator (say "->") that
fuses the two expressions. The general case involves sequences
hence:
TE1 := A1; ... Ai; ... An
TE2 := B1; ... Bj; ... Bm
TE1 -> TE2 :=
fail( TE1) or
{A1; ... ; An-1}; (An and B1); {B2; ... Bm}
The conjunctive expression is sampled by the sampling event of
the implication, so we need not worry about An and B1 having
different lengths (which would fail the conjunction).
This is one of many operators that were left on the drawing
board in our attempt to define a small and useful language.
Such operators can be added at any time without introducing
instability or disrupting the ongoing usage of the language,
since they agree with the fundamental concepts.
I'll be happy to comment on your example, regarding the
discrete event to synchronous model mapping. If this is too off
topic to be of interest to the group (Harry?) we could just
correspond privately.
Best regards,
-- yaron
Bernard Deadman wrote:
>
> 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 : Mon May 07 2001 - 09:03:39 PDT