RE: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal

Hi Gord,

I regret that the schedule of our BT does not match, so let's try to do
what is possible by phone. I sent the bridge information in my previous
email.

I hope that most of your concerns have already been addressed in the
proposal, and I believe that we will be able to provide satisfactory
solutions to other comments as well.

My slides are very informal and were designed to convey the basic idea
of the proposal, and sometimes the formulations are not always very
accurate, as you pointed out about syntactic sugaring. The proposal text
should be much more precise.

The slides about SAR and AAR may be useful since they explain the
simulation semantics. I will keep them, we always can skip them during
the presentation.

Could you clarify the following sentence: "Some of the special routines
(for example those related to enables) for checkers really need to be
explained in terms of how they relate to the outer language
constructs."?

I will update the slides according to your comments.

Thanks,
Dmitry

-----Original Message-----
From: owner-sv-ec@server.eda.org [mailto:owner-sv-ec@server.eda.org] On
Behalf Of Gordon Vreugdenhil
Sent: Thursday, March 06, 2008 7:35 AM
To: Korchemny, Dmitry
Cc: sv-bc@server.eda.org; sv-ec@server.eda.org; sv-ac@server.eda.org
Subject: Re: [sv-bc] RE: [sv-ac] RE: [sv-ec] Checkers & Formal



Dmitry,  I will not be able to attend as I am in India.  If
there is a webex/dialin, I will try to attend remotely, although
given the nature of my concerns, I very much doubt that a
remote discussion will be very effective.


Here are some high-level comments on this.  I don't think that BC/EC
likely needs (or wants) to know about all the assertions specific
areas that are in play.  For example, in the slides that were
posted, the issues related to SAR and AAR are likely not
really relevant to the concerns raised in BC/EC.

What is of concern (at least to me) are some of the comments on slides
37 and following.  I know that the way in which the "loop unrolling"
and similar constraints are now being expressed is different, but
the fundamental view is still there.  Some of the semantics
of "sampling", etc. as raised on the slides have not really become
much clearer to me either.

Some of the special routines (for example those related to
enables) for checkers really need to be explained in terms of
how they relate to the outer language constructs.  Rules regarding
force, hierarchical naming, etc. need to be covered.  Issues
related to freevars (vcd dumping, forcing, coverage, etc) need
to be explained, including comments as to what aspects of simulator
behavior are vendor defined.

One of the slide comments (on slide 10) was that assertions is
procedural code is just "syntactic sugaring".  There have been
various things since then that make me question that.  So, if
the "syntactic sugar" claim (esp. wrt checkers) is true, why
all the new features and complexity?  If it isn't true (which
I don't think it is), then the different rules need to
be carefully laid out.

I'd like to have a fairly concise description of the differences
in rules for immediate assertions, deferred assertions, concurrent
assertions, and assertions in checkers.  All in the context of
procedural code since that is the main area where things get
really messy.  If that cannot be summarized concisely and
completely, it would make me wonder about the complexity of
the resulting language and whether we aren't opening the door
to very difficult language compositionality issues in the future.


At a high level, I understand that when I've raised point issues
that those have eventually (for the most part) been resolved
to some extent.  My high level concern is that I think that the
resulting system is so complex that it is extremely difficult
to reason about the language feature interactions and how they
will compose in the future.

Gord

-- 
--------------------------------------------------------------------
Gordon Vreugdenhil                                503-685-0808
Model Technology (Mentor Graphics)                gordonv@model.com


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