RE: Proposal for generation changes...

["Dan Romaine" <dan.romaine@paradigm-works.com>]

I read through Vitaly Lagoon's first post, and I like his ideas.  The notion
of using variables in ranges sounds like an excellent addition, but as he
mentioned, it would require some complication that would need to be thought
through.  There must be some reason the language does not support this at
the moment.  I also agree about the need to document the generator, but the
problem there might be that Verisity will not be willing to divulge some of
there implementation secrets.

About the specific comments on my post, I agree that we should not dumb-down
the language and take away powerful features such as dynamic re-ordering.  I
see the power of such features but feel we need to add additional syntax to
make things more clear.  With the concept of unidirectional constraints,
many, many users hurt themselves with this.  I am an instructor for
Verisity's basic and advanced E courses, as well as a verification
consultant/contractor, and almost everyone has a problem with this issue...
I mostly refer to the imply operator.  The example of the keep a>b; is a
valid example and I agree that it is important to allow a test to constrain
either a or b, but have the a>b rule maintained.  That flexibility is great.
I feel the imply (=>) looks as if it's unidirectional when in fact it is
not.  Many intelligent users read the imply as, "if x is true, then impose
y", when that is not how it actually works.  I think we need both a
unidirectional as well as a bidirectional imply.  Most times an imply is
written it needs to be accompanied by the keep gen () before () statement to
produce what a user is trying to accomplish.

So my primary point is the concept of new syntax around the imply so that a
user who intends order can use an imply that also imposes generation order.

Regarding the second comment about separate generation cycles, this is an
acknowledged issue by Verisity.  In very large E environments, order can go
haywire!  There are so many things that can re-order constraints and create
new generation groups (by default there is one generation group, but order
requests create multiple generation groups), that when we are talking about
thousands and thousands of fields, the a, b order (from Vitaly's email) can
get reversed unintentionally.  I'm not sure if this is listed in the
known-bugs list, but the original declaration of fields is not enough to
guarantee order.  This may simply be an implementation issue with Specman
Elite, but it is a real problem that I feel we need to discuss and address.

I agree that we need to improve re-ordering syntax for clarity and ease of
use as well as improved understanding about what a user is coding, while
allowing flexibility and powerful features.  I have been using E exclusively
for years and feel that there is a lot of room for improvement in this area!

 - Dan Romaine




-----Original Message-----
From: Vitaly Lagoon [mailto:lagoon@cs.mu.oz.au] 
Sent: Tuesday, February 17, 2004 6:55 AM
To: Dan Romaine
Cc: 1647-gentf@ieee1647.org
Subject: RE: Proposal for generation changes...


Hi Dan,

 > Currently when one field has dependency on another field, to be safe,
 > we must specify generation order explicitly.  There is a default
 > generation order (order of declaration), as well as other sytax which
 > effects order (like when inheritance), but the most robust solutions
 > for eVC and the like of code written and tested in one environment
 > but then integrated in another is to use the value() method OR keep
 > gen () before () syntax.  Most people who code up large E code
 > environments run into issues with generation order.  I propose two
 > changes:
 > 

Let me comment on this view of the problem. I think that fixing an order
in a component is not a universal method of solving ordering
issues. Sometimes we must rely on the dynamic reordering. Here is my
example.

We have the following fragment in our specification:

  a : int;
  b : int;
  keep a>b;

and there are no other constraints affecting the relative order of 'a'
and 'b'. So, 'a' would be normally generated before 'b'. Now assume that
you or someone using your code wants to bind the specification to some
context e.g, a test. This context is associated with a new dependency

  keep a==2*b;

As we know, this one imposes the order "b before a". In the current
Specman this constraint will cause reordering. 'b' would be generated
first and 'a' would be then computed as 2*b. The constraint "a>b" would
be checked (and satisfied, unless there was an integer overflow) thus,
guaranteeing the integrity of the environment. Note that the generation
would fail if we had "a before b" constraint in the
specification. Similarly, "b before a" is not good because we could have
"keep b=a/2" in our context.

My point is that dynamic reordering can be very useful and provide great
flexibility. Of course, it should be used with care and understanding of
its principles.  

 > 1) We create a syntactical notion of new passes through generation.
 > This would provide a way for one piece of code (an eVC perhaps) to
 > run its own static analysis, reductions, and set scalars flow
 > completely independent of other sections of code.  This feature would
 > create predictability and reliability that does not exist today.
 > When e-code is run in a different environment than you wrote it in,
 > your generation order might be re-arranged.  Verisity admits this
 > freely, and I think we need to find a solution.

My understanding is that the internal order in a component is not
affected unless there are external constraints imposing order (as in my
example). What am I missing here?

 > 
 > 2) We either add a new semantic for unidirectional implication or
 > change the existing bi-directional imply.  Most users would like to
 > see the imply operator (=>) effect generation order.  I think we need
 > both a unidirectional and a bidirectional imply.  Both could boil
 > down to the appropriate OR statements, but the unidirectional could
 > also add an order constraint.  I think the goal should be easily
 > coded user intent and readability.  I'm not sure what the best
 > solution is, but there are times when the order of generation is
 > thought to be one way, but it becomes convoluted and the imply holds
 > true, but the unintended field is in control of distribution.  Here
 > is a quick example:
 > 
 > x: uint;
 > y: byte;
 > 
 > keep x < 10 => y < 200;
 > 
 > In this case, a small range of x [0..9] has a large range for y [0..199],
 > but a large range of x [10..MAX_INT] has a small range of y [200..255];
 > 
 > If x is generated first, the distribution of values is even over
 > [0..MAX_INT] by default, therefore there is a strong chance that y
 > will be in the [200..255] range.  If Y is generated first, the
 > distribution of generated values changes completely.  Both examples
 > are OK, but the intent needs to be more clear than the simply order
 > of declaration.
 > 


I would use "keep gen (x) before (y)" in addition to the "=>"
constraint. That is assuming that my intention is for 'x' to control the
distribution of 'y'. So, the directed imply you are proposing is just an
alternative syntax for that. Am I right?

 > So in short, there is a difference between dependency and order.
 > Order is our mechanism to guarantee dependency.  If order is not
 > explicitly coded, there is room for unintended results.  I think we
 > need to reduce the ambiguity and add more precision, specifically to
 > the imply operator.
 > 

I think that this view is a bit radical implying that dynamic reordering
is only there to confuse us, and that the order should be always
hardwired in e-code. I disagree with that. However, there is definitely
room for discussion on how to improve the reordering mechanism and make
the it easier to control and understand.

Regards

Vitaly Lagoon