Re: [sv-ac] Mantis 1757 Accepton / rejecton operators

my comments:

1. page 2, at paragraph

"The semantics of accept_on are similar to disable iff, except that it 
operates at the property level rather than
the verification statement level and it uses sampled values.
The semantics of reject_on(expression) property are the same as
not(accept_on(expression) not(property))."

some wording is needed to explain true/false status vs. disabled status.

2. page 2, I think that the following line is redundant and confusing

"not applied to the top property inverts the result of these operators."

3. at the examples at the top of page 3"

"before p1" => "before the evaluation of p1 is completed"
there are other similar phrases.

In general I don't see a need to 3 different examples. I think that one 
example with
explicit p1, p2 would be more informative.

4. page 3 type "the" => "then"

"if a becomes true in the same time step as b and before p1 completes, 
then the p succeeds in that time step.
If b becomes true before a and before p1 completes, the p fails."
^

5. bottom of page 3,

p2 is illegal for two reasons:
a. the recursive instantiation does not match the port list
b. it does not advance in time

The instantiation of p4 in the declaration of p3
does not match the port list of p4.

6. page 6.

the paragraph

"The operator reject_on has the dual semantics. A word w satisfies 
property reject_on(b) P if and only if
w satisfies P and if b happens first time at the position i then 
w[0:i-1] concatenated with any infinite word
must satisfy the property (in other words the property P should be 
completely satisfied before b is
encountered)."

is not true. You should use the \bot sign as in the definition. For 
example think of the property

"reject on (b)((1[*1:$] |-> a) or (!a[->1]))"

suppose that b happen at the first cycle. Every infinite word satisfies 
"((1[*1:$] |-> a) or (!a[->1]))" but the overall property still fails.

7. page 7. The definition of accept_on is broken, align it with the 
definition of page 6.


Doron


Korchemny, Dmitry wrote:

> Hi Lisa,
>
> And my comments also,
>
> Thanks,
>
> Dmitry
>
> ------------------------------------------------------------------------
>
> *From:* Lisa Piper [mailto:piper@cadence.com]
> *Sent:* Monday, June 18, 2007 6:58 PM
> *To:* Korchemny, Dmitry; Thomas.Thatcher@sun.com; Eduard Cerny
> *Cc:* sv-ac@eda-stds.org
> *Subject:* RE: [sv-ac] Mantis 1757 Accepton / rejecton operators
>
> Hi Dmitry,
>
> Some questions below…
>
> Lisa
>
> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of 
> Korchemny, Dmitry
> Sent: Monday, June 18, 2007 11:42 AM
> To: Thomas.Thatcher@sun.com; Eduard Cerny
> Cc: sv-ac@eda-stds.org
> Subject: RE: [sv-ac] Mantis 1757 Accepton / rejecton operators
>
> Hi Tom,
>
> In assertions and assumptions disable iff is similar to accept_on, but
>
> there is nothing acting as reject_on. Using reject_on helps writing
>
> concise and efficient assertions. The only workaround for reject_on is a
>
> throughout operator, but throughout is synchronous and can be used with
>
> sequences only, while reject_on is asynchronous and can be used with
>
> arbitrary properties.
>
> [Lisa Piper >>>] I thought these were to be synchronous – why do you 
> want them to be asynchronous? If they are asynchronous, are the 
> scheduling considerations identical to those for disable iff?
>
> [Korchemny, Dmitry] You can construct a synchronous reset from an 
> asynchronous one in presence of the global clocking, e.g., 
> accept_on(rst && rising_i(clk)) if your clock is posedge clk. The 
> opposite cannot be done. The difference between accept_on and disable 
> iff is that accept_on takes the samples value of the reset, while 
> disable iff is not sampled.
>
> Here is an example: "A sequence beginning with go, followed by two get
>
> during which kill is not asserted, must be followed by a sequence of two
>
> put (not necessarily consecutive) before which stop cannot be asserted".
>
> Here is an implementation using reject_on:
>
> assert property (@(posedge clk) go ##1 (get && !kill)[*2] |-> reject_on
>
> (stop) put[->2]);
>
> Note the difference with the following implementation
>
> assert property (@(posedge clk) go ##1 (get && !kill)[*2] |-> !stop
>
> throughout put[->2]);
>
> In the first implementation stop is caught everywhere when awaiting two
>
> put signals, while in the second one it will be caught only if it is
>
> high on the rising edge of the clock.
>
> accept_on is a dual operator to reject_on, and it plays the same role in
>
> cover statements as reject_on in assertions.
>
> Unfortunately disable iff cannot be reused for the following main
>
> reasons:
>
> * disable iff acts as accept_on in assert and assume statements, and as
>
> reject_on in cover statements
>
> */[Lisa Piper >>>] not since 805. Disable iff is not pass or fail 
> anymore./*
>
> [Korchemny, Dmitry] Yes, my statement is not accurate, But the 
> disabled execution of an assertion essentially means its (vacuous) 
> success, while the disabled execution of a cover statement means its 
> (vacuous) failure.
>
> * When disable iff is active, the thread execution is defined as
>
> disabled, while accept_on and reject_on are regular temporal operators
>
> and lead to a success or a failure of the property
>
> There is also a positive side in this duplication - disable iff defines
>
> the main reset of an assertion and clearly shows when the assertion is
>
> disabled and when not, so the tools can report the vacuous success, etc.
>
> As for accept_on and reject_on, they act as regular temporal operators
>
> and do not result in a vacuous attempt.
>
> */[Lisa Piper >>>] but disable iff is not vacuous either./*
>
> [Korchemny, Dmitry] Sorry, disabled J
>
> I think the names accept_on and reject_on exactly reflect their
>
> semantics: accept_on(rst) p says accept p (if not failed before) when
>
> rst is high. The reject is dual.
>
> Thanks,
>
> Dmitry
>
> -----Original Message-----
>
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
>
> Behalf Of Thomas Thatcher
>
> Sent: Friday, June 15, 2007 12:59 AM
>
> To: Eduard Cerny
>
> Cc: sv-ac@server.eda-stds.org
>
> Subject: Re: [sv-ac] Mantis 1757 Accepton / rejecton operators
>
> Hi Eduard,
>
> I just read the proposal. My first question is: Why do we need these
>
> operators? What type of problem are we solving? It appears that the
>
> only difference from "disable iff" is that the property evaluations will
>
> complete with a given value on a reset, rather than not completing.
>
> The second thought is that the rejecton and accepton names don't really
>
> describe their function too well. I had to read the first part of the
>
> proposal to figure out what these new operators were for.
>
> Tom
>
> Eduard Cerny wrote On 06/14/07 11:19,:
>
>> Hello,
>
>>
>
>> I have uploaded an updated version of the proposal, also attached
>
> here.
>
>>
>
>> best regards,
>
>> ed
>
>>
>
> -- 
>
> ------------------
>
> Thomas J. Thatcher
>
> Sun Microsystems
>
> 408-616-5589
>
> ------------------
>
> -- 
>
> This message has been scanned for viruses and
>
> dangerous content by MailScanner, and is
>
> believed to be clean.
>
> -- 
>
> This message has been scanned for viruses and
>
> dangerous content by MailScanner, and is
>
> believed to be clean.
>
>
> -- 
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. 



-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.