RE: [sv-ac] Mantis 1900 comments - Part 5

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Thu Feb 07 2008 - 09:09:56 PST
Hi Shalom,

 

Please, see my comments below.

 

Thanks,

Dmitry

 

________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Bresticker, Shalom
Sent: Monday, February 04, 2008 2:12 PM
To: sv-ac@server.eda.org
Cc: sv-champions@server.eda.org
Subject: [sv-ac] Mantis 1900 comments - Part 5

 

- The proposal has the following:

 

// Illegal:

//       The clock is not inferred from the context,

//       it shall be explicitly specified in the checker

//       (It is assumed that there is no default clocking declaration

//       in the checker declaration scope.)

checker check_illegal (logic test_sig);

   property p(logic sig);

         ...

   endproperty

   // Illegal: no clock in the property

   a1: assert property (p(test_sig));

   // Illegal: no clock in the property

   c1: cover property (!test_sig ##1 test_sig);

endchecker : check_illegal

 

"it shall be explicitly specified in the checker" - "shall" is not
appropriate in an example, "must" is better.

 

[Korchemny, Dmitry] I deleted the whole comment, see below.

 

"It is assumed that there is no default clocking declaration in the
checker declaration scope." - "It is assumed" refers only to this
example and not to the general case? It is confusing.

 

Most important, it seems to me that the assertions are illegal because
no clock is specified explicitly in the assertion, nor is any inferred
from the context. But this is true of any such property, not just in a
checker, so what is special about this? I guess you want to show that
the clock is not automatically inferred from the instantiation context,
but this is a confusing way to do it.

 

[Korchemny, Dmitry] I deleted the comment preceding this checker.
Comments to assertions should be sufficient. Also modified these
comments:

 

"Illegal: no clock in the property" --> "Illegal: no clock in the
assertion"

 

- 16.18.2 says that a checker body may contain let declarations, so the
statement in Mantis 1728 that "A let can be declared in any of the
following" needs to be modified to include checkers.

 

[Korchemny, Dmitry] Done.

 

- 16.18.5 says, "An initial_check procedure may contain concurrent
assertions and event controls only...An always_check procedure may be
specified in the checker body only and may contain concurrent
assertions, nonblocking checker variable assignments (see 16.18.6.1) and
event control statements... The always_check and initial_check
procedures impose the restriction that they contain one and only one
event control and no blocking timing controls." At first it says that
they may contain event controls (plural) and later it says that only one
is allowed. This is confusing.

 

[Korchemny, Dmitry] Changed it to "and an event control statement"

 

- "In the initial_check and the always_check procedures all events from
the explicit sensitivity list of their event control are inferred (if
any specified)," 

The "(if any specified)" is not clear. An event control is required. So
the only alternative to an explicit sensitivity list is an implicit one,
@*. Is that allowed?

 

[Korchemny, Dmitry] I deleted "(if any specified)", since it is
logically redundant. The always_check must have a an event control, but
the initial_check does not have to.

 

Thanks,

Shalom

---------------------------------------------------------------------
Intel Israel (74) Limited
 
This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Thu Feb 7 09:16:53 2008

This archive was generated by hypermail 2.1.8 : Thu Feb 07 2008 - 09:17:02 PST