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.

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
* 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.

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.