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?

 

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.

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

 

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, and is
believed to be clean.