Subject: RE: [sv-ac] Question about reference to data defined in sequence.
From: Erich Marschner (erichm@cadence.com)
Date: Wed Feb 05 2003 - 18:28:45 PST
Bassam,
Sorry, I didn't mean to distress you. My point was simply that "substitution" is not sufficiently precise - you have to state *what* is being substituted for *what*. The substitution you are after seems to be text substitution, i.e., macro-processing semantics. (Parameter "passing" is simply a term that refers to other kinds of substitutions - of value for value, or reference for value, etc.)
I would use the term "text substitution" to describe the kind of substitution going on here. This involves "replacing" the text of each formal parameter name with the text of the corresponding actual parameter (which might be a value, a name, an expression, or a sequence). I would avoid using the term "verbatim" here, because it usually implies word for word quotation, or copying, without any notion of substitution.
The PSL 1.0 LRM uses "replacing" to describe this operation - e.g. in section 6.2.4.2, Property Instantiation, on page 74, lines 12-14:
"An instance of a named property holds at a given evaluation cycle if and only if the named property, modified by replacing each formal parameter in the property declaration with the corresponding actual parameter in the property instantiation, holds in that evaluation cycle."
Regards,
Erich
-------------------------------------------
Erich Marschner, Cadence Design Systems
Senior Architect, Advanced Verification
Phone: +1 410 750 6995 Email: erichm@cadence.com
Vmail: +1 410 872 4369 Email: erichm@comcast.net
| -----Original Message-----
| From: Bassam Tabbara [mailto:bassam@novas.com]
| Sent: Wednesday, February 05, 2003 8:17 PM
| To: Erich Marschner; 'Adam Krolnik'; john.havlicek@motorola.com
| Cc: Surrendra.Dudani@synopsys.com; sv-ac@eda.org
| Subject: RE: [sv-ac] Question about reference to data defined in
| sequence.
|
|
| Yes, that's what I said. And I further emphasize that explaining the
| semantics, must not use "overloaded" words ... I chose -substitution-
| (Jay supplied a supporting precedent too), because it seemed least
| problematic and a rather neutral word, that means "verbatim". I would
| not even want the reader to think about passing
| mechanisms/connections,
| that's the whole point.
|
| Your email wording however distresses me Eric, you use the word
| "substitution" rather freely as a generic concept for
| passing:-)! When
| proposing it, I had intended for it to be a distinction from
| "passing".
| Passing is one thing, -replacing- is another. Ok I am switching to
| replacing/substituting-verbatim now :-)!
|
| -Bassam.
|
| --
| Dr. Bassam Tabbara
| Technical Manager, R&D
| Novas Software, Inc.
|
| http://www.novas.com
| (408) 467-7893
|
| > -----Original Message-----
| > From: Erich Marschner [mailto:erichm@cadence.com]
| > Sent: Wednesday, February 05, 2003 4:44 PM
| > To: bassam@novas.com; Adam Krolnik; john.havlicek@motorola.com
| > Cc: Surrendra.Dudani@synopsys.com; sv-ac@eda.org
| > Subject: RE: [sv-ac] Question about reference to data defined
| > in sequence.
| >
| >
| > Bassam,
| >
| > What terms are used to describe the operation is not the
| > point. The SVA LRM needs to explain the semantics of such
| > parameters.
| >
| > All "parameter passing" is a kind of substitution, but there
| > are different ways to do substitution - hence the
| > proliferation of terms such as pass-by-reference (a pointer
| > to the actual variable location is substituted for the value
| > of the formal parameter, and implicit dereferencing occurs),
| > pass-by-value (the value of the actual variable is
| > substituted for the value of the formal parameter),
| > pass-by-name, pass-by-value-result, and other forms of
| substitution.
| >
| > I gather that you want the definition to be something like this:
| >
| > - The text of the actual parameter is substituted for each
| > occurrence of the corresponding formal parameter.
| >
| > This is essentially the kind of substitution done by
| > macro-preprocessors, which manipulate text. This is fairly
| > straightforward and gives intuitive results, provided that
| > none of the identifiers in the actual parameter expression
| > are redeclared in the template. If this is the definition
| > you want, then the SVA LRM should state that clearly, and it
| > should comment on the issue of a redeclaration in the
| > template potentially changing the meaning of a name that is
| > part of the actual parameter.
| >
| > Regards,
| >
| > Erich
| >
| >
| >
| > -------------------------------------------
| > Erich Marschner, Cadence Design Systems
| > Senior Architect, Advanced Verification
| > Phone: +1 410 750 6995 Email: erichm@cadence.com
| > Vmail: +1 410 872 4369 Email: erichm@comcast.net
| >
| > | -----Original Message-----
| > | From: Bassam Tabbara [mailto:bassam@novas.com]
| > | Sent: Wednesday, February 05, 2003 6:25 PM
| > | To: 'Adam Krolnik'; john.havlicek@motorola.com
| > | Cc: Surrendra.Dudani@synopsys.com; sv-ac@eda.org
| > | Subject: RE: [sv-ac] Question about reference to data
| defined in
| > | sequence.
| > |
| > |
| > | Hi All,
| > |
| > | For templates I would recommend we not use any of the
| following
| > | terminology to describe the formal/actual association: argument
| > | passing, design object binding, port connection,
| > parameters (although
| > | this gets
| > | the idea across, still has its baggage) ....
| > |
| > | * I suggest we call this -substitution- more formally
| > formal/actual
| > | substitution. That's what's happening no "passing"
| > (value/reference
| > | and so on...), and not really parameter (that's better reserved
| > | for Adam's
| > | generate type constructs...).
| > |
| > | BTW, to respond to this thread, I see no apparent
| > restriction on this
| > | substitution, you can do whatever, the restriction is that
| > once the
| > | code is preprocessed there should not be any (semantic)
| errors e.g.
| > | re-definition of sequences, putting a sequence where a
| > | boolean would go
| > | and so on ...
| > |
| > | -Bassam.
| > |
| > | --
| > | Dr. Bassam Tabbara
| > | Technical Manager, R&D
| > | Novas Software, Inc.
| > |
| > | http://www.novas.com
| > | (408) 467-7893
| > |
| > | > -----Original Message-----
| > | > From: owner-sv-ac@server.eda.org
| > | > [mailto:owner-sv-ac@server.eda.org] On Behalf Of Adam Krolnik
| > | > Sent: Wednesday, February 05, 2003 3:08 PM
| > | > To: john.havlicek@motorola.com
| > | > Cc: Surrendra.Dudani@synopsys.com; sv-ac@server.eda.org;
| > | Adam Krolnik
| > | > Subject: Re: [sv-ac] Question about reference to data defined
| > | > in sequence.
| > | >
| > | >
| > | >
| > | >
| > | > Hi John;
| > | >
| > | >
| > | > Or how about this version which would allow the encapsulation
| > | > I desire.
| > | >
| > | > The template has as an argument a sequence (check_seq) that
| > | > will be called from within the template. When it is called,
| > | > it passes in the dynamic data reference.
| > | >
| > | >
| > | > // A user defined sequence...
| > | > sequence check_data(data) = (data == fifo_out_data);
| > | >
| > | > // A standard template for use whereever.
| > | > template tem(check_seq);
| > | > ast: assert (fifo_push => ((int itsdata =
| > | > fifo_in_data) [1:100] fifo_pop;
| > | > [0] check_seq(itsdata)))
| > | > else $error();
| > | > endtemplate
| > | >
| > | > // Instantiate the template with the specific data
| > | checking sequence.
| > | > tem my_tem(check_data);
| > | >
| > | >
| > | > Or with more arguments:
| > | >
| > | > template tem(clk,
| > | > fifo_push,
| > | > fifo_in_data,
| > | > fifo_pop,
| > | > check_seq);
| > | >
| > | > ast: assert @(posedge clk)
| > | > (fifo_push => ((int itsdata = fifo_in_data)
| > | > [1:100] fifo_pop;
| > | > [0] check_seq(itsdata)))
| > | > else $error();
| > | > endtemplate
| > | >
| > | >
| > | > tem my_tem(clk, fifo_push, fifo_in_data, fifo_pop,
| check_seq);
| > | >
| > | > So what else could be parameterized?
| > | > The maximum value in the range above? [1:100] - could it
| > | > be [1:latency] ?
| > | > The width of declared dynamic data? int itsdata - could
| > | > it be [W-1:0] itsdata?
| > | >
| > | >
| > | > Adam Krolnik
| > | > Verification Mgr.
| > | > LSI Logic Corp.
| > | > Plano TX. 75074
| > | >
| > | >
| > | >
| > |
| > |
| >
|
|
This archive was generated by hypermail 2b28 : Wed Feb 05 2003 - 18:29:38 PST