RE: 1647 constraints and generation task force

[Ken Sailor <Ken_Sailor@pmc-sierra.com>]

Vitaly,

I've added the task force to the address since this is the most interseting email relating to the taskforce so far...  

As to your questions...

My background with regards to Versity: almost none.  I'm a technical advisor who has managed verification primarily before my company adopted Specman.  I understand the ideas but have little practical experience.

My phd, however, was in computer language design and semantics so I'm comfortable with the task if not the subject matter.

I was asked by my management to take on this task to help out Verisity.

Lately my work has almost nothing to do with verification, although I remain interested.

Big disclaimer!  If I write something totally stupid, don't be shy about telling me so.  I have no doubt that I will, and the cause can either be my lack of experience with Specman or just general incompetance.

---

Yes, side effects and the when sub-typing screw any kind of simple semantics.  Hopefully, however, there are weasel words to cover the complexity and put people into a heavy-lidded trance.  You really can't say much more about those issues than they exist or am I being too glib?  Having read mathematically rigorous semantics, I see no point in attempting such a beast.

Isn't the directionality of x=y[i:j] really a limitation of the current algorithm?  Let's just imagine that somebody came up with a magical algorithm that lifted this restriction - would you be upset?  What about leaving directionality to the implementation and user manual and simply saying that directionality is a tool for implementation that will be effectively exploited by the expert user but will not be guaranteed across implementations.

Ken





-----Original Message-----
From: Vitaly Lagoon [mailto:lagoon@cs.mu.oz.au]
Sent: Wednesday, November 03, 2004 6:42 AM
To: Ken Sailor
Subject: RE: 1647 constraints and generation task force



Hi Ken,

I don't have any clear ideas of how to write the standard. Moreover, I
guess I need more background information on what we are trying to
achieve. Are we trying to push in as much of constraint language of 'e'
as possible, maybe with some restriction lifted? Or maybe, we want to
fix a "core subset" of 'e' constraint language; or maybe, an abstract
superset? What's your point of view?


 > My humble insight into the spec'ing of constraints is this:
 > 
 > What about writing up the current syntax and translating into set
 > theory.  In this fashion, a loose but definitive semantics would be
 > given.

I like the direction in general. However, I doubt that we can capture
the whole of 'e' constraints in set semantics. Some features, such as
when-subtyping and structure constraints can introduce enormous
complexity in the set semantics. Some other things cannot be captured at
all, to the best of my understanding. For example, methods with side
effects.

 > 
 > That's about as far as I have gotten.  My impression, however, is
 > that a great deal of details are more particularly related to an
 > implementation or specific algorithm and those could be left out of
 > the standard.

That's right. However, we must draw the line carefully. For instance, in
a bit constraint x==y[j:i] I'm happy to have the directionality "i,j
before x,y" as part of the standard.

 > 
 > The down side is that you couldn't move from tool to tool and get the
 > same execution pattern - since different algorithms could satisfy the
 > standard.  

I don't think we should aim for that kind of full portability. It's
impossible to guarantee the same constraints are solved the same way
even in different versions of Specman, let alone future implementations.

 > On the other hand, the constraint algorithm will be the
 > proprietary heart of any tool so what else would you expect.

I think we accept it. We must state the right level of requirements to
the semantics of any such algorithm.

 > Have you actually done some thinking about how to write the standard?

I've just started :-)


BTW, could you write a few words about your background and relation to
Verisity?


Regards

Vit