RE: Final Assertion Spec -- problem noted.

Subject: RE: Final Assertion Spec -- problem noted.
From: Bassam Tabbara (bassam@novas.com)
Date: Fri Apr 05 2002 - 12:20:13 PST

Hey Adam,

First of all thanks for catching those "glitches" in the grammar. I think we
should proof-read the doc a bit.

As for your comment about the case of req .... req .... done trace, and
the spec of: if (req) assert ([1:10]; done);
Indeed, this is a balancing act between adding more generality (for abstract
spec), and trying to keep things precise (for implementation). Erich more
than adequately addressed this.... I would echo his comments that in order
to target "low-level" (implementation) assertions, which is primarily what
the DAS is (cover low-level well, and as many higher level notions by
combining many assertions statements ...), adding the (rather implicit)
"consumption" semantics into the statement i.e. embedding the meaning that
each req has a unique done seems a bit much ...

So, I think since assertions will be incorporated in a -design- (i.e. (one
possible) implementation of the spec) "simple" semantics as above asserts a
req should be followed by a done... are in order. If a user wants to check
the additional requirement of "Each req has a unique done" they would have
to state this abstract notion in "implementation terms" which could vary
from:
        "No 2 requests can follow without an intermediate done" for some
implementations
        "..." some other implementation may have adequate handshake and thus more
accurately control the check spawning (if req && ...) ... done && ...
        ....

-Bassam. 

--
Dr. Bassam Tabbara
Technical Manager, R&D
Novas Software, Inc.

http://www.novas.com
(408) 467-7893

> -----Original Message-----
> From: krolnik@dts0.lsil.com [mailto:krolnik@dts0.lsil.com]On Behalf Of
> Adam Krolnik
> Sent: Friday, April 05, 2002 7:50 AM
> To: fitz@co-design.com
> Cc: assertion@eda.org; Bassam Tabbara; Erich Marschner; Gail Dagan
> Subject: Final Assertion Spec -- problem noted.
>
>
>
> Good morning;
>
> I also found that the keyword 'triggers' is stillthere in the BNF,
>  but is not explained in the text and should be removed.
>
> The top paragraph on page 9 brings up a question that we did not
> address - that of (to use Verisity's term) consuming an event.
>
> The paragraph states:
>
> If the assert statement is executed again before the sequence spawned
> by the original execution has expired, then a new process shall be
> spawned that looks for the sequence starting at the current timestep.
> It is therefore possible to have multiple processes in-flight, each
> monitoring the same sequence but offset in time. It is possible for
> these multiple processes to be satisfied by the same sequential
> behavior, even though the processes are offset in time.
> ** In such a case, both processes will terminate at the same
> timestep, in which both sequences are satisfied."
>
> One problem is this paragraph terminates in 'Consider:' with an
> example that does not relate at all to this paragraph.
>
> Second - the last sentence that I emphasized (**) will prevent
> assertions with variable occurrences from being useful.
>
> Consider the case of this assertion:
>
> if (req) assert ([1:10]; done);
>
> This allows 'done' to be asserted 1 to 10 clocks after 'req'.
> Now consider two 'req's in consecutive cycles. Is this assertion
> the proper form to ensure that the second 'req' will receive a 'done'
> within the specified time period?
>
> According to the emphasized sentence above, the answer is no.
> Both processes for the assertion will terminate with the first done
> (assuming it does not occur on the very next clock.)
>
> clk        __    __    __    __    __    __    __    __
>       ____|  |__|  |__|  |__|  |__|  |__|  |__|  |__|
>            _____       _____
> req   ____|     |_____|     |__________________________________
>                              ___________
> done  ______________________|           |______________________
>                              _____
> done2 ______________________|     |____________________________
>
> Would the assertion pass if the wavefrom 'done2' was used for
> the 'done' signal. As currently defined both processes would
> pass, though that waveform is missing another 'done' pulse.
>
> Is this consistent with VFV semantics for overlapping sequences?
>
> This is a serious problem as currently defined. One will be in
> danger of providing false positives!
>
> IMHO I propose:
>
> "In such a case, the first process requiring that event will
> have priority to consume it. Subsequent processes will need to
> wait for the next time the event occurrs."
>
> We have not seen any cases where the current behavior is desirable
> over this proposed behavior. Anyone else on the committe have
> alternate experiences? I know there are people with existing
> assertion tools/languages.
>
> --------------------
>
> BTW, what was the concensus on the assume/guarantee question from VFV?
> I presume that it will be a tool issue to allow specification of
> which properties to assume or prove.
>
>
>    Adam Krolnik
>    Verification Mgr.
>    LSI Logic Corp.
>    Plano TX. 75074
>

This archive was generated by hypermail 2b28 : Fri Apr 05 2002 - 12:21:41 PST