RE: [sv-ec] and [sv-ac] Checkers, and mantis items 2088,2089

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Thu Mar 13 2008 - 10:01:59 PDT
Hi Mehdi, Neil,

I hope I addressed most of your concerns at the meeting, I will
summarize my answers here (see below). We will also discuss your
comments at the SV-AC meeting.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Mehdi Mohtashemi
Sent: Thursday, March 06, 2008 10:12 AM
To: Korchemny, Dmitry
Cc: sv-ec@server.eda.org; sv-ac@server.eda.org; Levy, Yossef (DT);
john.havlicek@freescale.com
Subject: [sv-ec] and [sv-ac] Checkers, and mantis items 2088,2089

Hi Dimitry,  and SV-AC members,
As you have initiated a review meeting this coming Monday, we wanted
to provide a summary of the discussion that took place during our SV-EC
conference call on Monday March 3 2008.

Our SV-EC committee conducted an email ballot on mantis items 2088 and
2089
based on a request from SV-AC (John had sent the formal request). These 
mantis items did not pass during email vote as you are aware, there were
many discussions on the reflector on the subject. 
We then had placed 2088/2089 on SV-EC meeting agenda for Monday March 3
2008
and attempted to vote on them.
Below we summarize the feedback from SV-EC to SV-AC.  

--------------------------------------------------------------------
Mantis 2088, 2089 - from SV-AC committee

   At the meeting both Gordon and Arturo stated that they were now ok
with 
   the latest proposals for both of these Mantis items. The changes made
by Tom 
   addressed their concerns.

 Following concerns were raised:
   - There are concerns about checkers in general.
[Korchemny, Dmitry] The usability issue is addresses in the preamble to
1900.

   - With respect to Checker instantiations in procedural code
        naming conventions  (including cross-module references)
[Korchemny, Dmitry] The proposal does not forbid cross-module
references. Gord requested to add explicitly that the hierarchical names
inside checkers are resolved in the checker declaration context only.
Another restriction that should be added is that the hierarchical names
referencing checker objects should not be actual arguments of a checker.

        forces semantics
[Korchemny, Dmitry] According to the proposal the checker variable
cannot be forced inside a checker (it is not allowed by its grammar).
There is no limitation on forcing checker variables outside a checker,
therefore their forcing is not different from the forcing of regular
variables. The question is what a practical need in forcing checker
variables is. It might be a better idea to disallow checker variable
forcing (at all) and checker variable assignment outside the checker.

	  is binding allowed?
[Korchemny, Dmitry] Yes, it is. See subclause 22.10 in the proposal.

     General feeling was that the rules for all of these need
definition.
[Korchemny, Dmitry] See the above comments.

   - The assertions within checkers seem to be a new class of
assertions. 
     They are not concurrent nor immediate.

[Korchemny, Dmitry] They are regular concurrent assertions.

   - There appear to now be 4 types of assertions.
     Concurrent, immediate, deferred, those inside checkers.

[Korchemny, Dmitry] Only 3. See my previous comment.

   - It could be difficult to deal with all four.

[Korchemny, Dmitry] Same.

   - Checkers can now have untyped formals. This creates new situations
as to
     when certain information becomes available. 

[Korchemny, Dmitry] This comment needs to be clarified.

   - Coverage on a freevar seems to now be allowed. 
     This type of coverage appears to be unreliable. 
     Does the simulator just select one of the possible values? Freevars
in
     a simulation environment are very different from a freevar in a
formal
     tool.

[Korchemny, Dmitry] I assume that the question relates to "cover
property". The "cover property" with free variables will be as reliable
in simulation as "assert property": if the imposed assumptions are met,
both assert and cover statements with free variables are sound. If a
cover point is reachable for an expression containing a free variable
then it is reachable for any choice of the values for this free variable
in simulation, provided it is compliant with the assumptions.

Here is an illustration:

free checkvar bit a;
cover property (@clk a || !a);

This property is covered for any a. If you substitute a by any value at
any time, the cover point will still be reached.

   - Checkers are adding several new keywords that could clash with the
names

     of existing variables.

[Korchemny, Dmitry] As far as I can see the only problematic keyword is
"free". We will discuss the alternatives.

 Attempt to vote on approving the proposal for Mantis 2088 failed, here
is the
 details:

      Move: Arturo - approve the proposal for Mantis item 2088
    Second: Steven
   Abstain: Gordon  
		Ray       - not against the proposal for Mantis item
2088
		Steven    - wants the whole group of checker proposals
to be 
			    reviewed by the SV-EC as a group.
            Francoise - not sure how the coverage will be calculated
   Opposed: Cliff, Don, Heath, Dave Rich - same reason as Steven
		(Stu - would have also voted no if he had voting
rights.)
      In Favor: Arturo, Neil, Mark Hartoog, David Scott
	 12 attendees with voting rights were on-line.
	 Motion failed: 4-yes,4-no,4-abstains

More discussion continued after the above vote was concluded.

Some of the feedback from the SV-AC on questions raised on 2088 and 2089

was to look at the proposals from other SV-AC Mantis items. 
Some SV-EC meeting participants felt that a larger group of SV-AC 
mantis items should be reviewed as a group; that is a whole set of
Mantis 
items that pertain to checkers should be reviewed as a group instead of 
trying to review 2088 and 2089 in isolation. Their concern is with
checkers 
in general and not with 2088 and 2089 in particular. 

The following list was proposed (although there may be others):
   1900, 1549, 1681, 1648, 1728, 1682, 2088, 2089

Some of the statements and concerns by attendees:
There is a concern that checkers are crossing over into the rest of the
language. 
When the proposals from the SV-AC are contained within the area of
assertions, 
there is less of a concern. 
For some of the changes being made a cross-committee group would have
been 
more appropriate.

Procedural code seemed to have had created a particular concern.

[Korchemny, Dmitry] See my answer to Steven.

There appears to be disagreement within the SV-EC as to whether checkers

are part of the procedural code or not.

[Korchemny, Dmitry] The checkers may be instantiated in procedural code,
but they are not part of this procedural code where they are
instantiated. The checker instantiation in a procedural code is kind of
"syntactic sugaring" only.

 Although some members are
concerned 
that there are issues that need to be addressed but aren't sure yet.
They are 
looking for a way to be convinced that there are no additional issues
that need 
to be addressed.

The members who voted No and abstained felt that if these issues are not

addressed now they are likely to show up as a ballot issue and at that
point 
in time there will be less flexibility in how to address them. 

There appears to be a concern that more of a synthesis-centric viewpoint
is
leading these proposals in SV-AC. In general having others review the
proposals 
in detail would be useful. 


Mehdi and Neil
March 5 2008
------------------------------------------------------------------------
------





 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, 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 Mar 13 10:05:13 2008

This archive was generated by hypermail 2.1.8 : Thu Mar 13 2008 - 10:05:45 PDT