Subject: RE: [vhdl-200x] Implicit conversion, Overloading, & Strong Typin g
From: Bailey, Stephen (SBailey@model.com)
Date: Fri Dec 19 2003 - 07:38:11 PST
Gabe,
The application of a boolean conversion on an entire property has distinctly different semantics from a boolean conversion on each combinatorial expression within a sequence. The latter is no different from a boolean expression in VHDL (or whatever HDL you are using with PSL). The former converts the pass/fail (hold, not held) of the entire sequence into a boolean value. PSL already supports doing this with named endpoints. A couple of the possible uses of endpoints are:
1. Transfer the result of a sequence in one clock domain to another.
2. Potential use for triggering HDL processes (providing signalling semantics that cross from the PSL to HDL realms). This would be useful for reactive testbenches and custom error handling applications.
There are probably other uses as well, but the point is that what you wrote is not semantically equivalent to what Jay wrote.
-Steve Bailey
> Jay,
> what about writing:
> assert always to_boolean(
> {master_state = WRITE} |->
> {{slave_accept = '1'} | {master_state = WRITE [*];
> master_state = WRITE and slave_accept = '1'}});
> It would mean that the to_boolean function would have to
> understand PSL, but
> that is doable and still keeps the flexibility of the assert
> statement to
> handle non boolean conditions.
> Gabe
> ----- Original Message -----
> From: "Jay Lawrence" <lawrence@cadence.com>
> To: "VHDL-200x" <vhdl-200x@eda.org>
> Sent: Friday, December 19, 2003 8:21 AM
> Subject: RE: [vhdl-200x] Implicit conversion, Overloading, &
> Strong Typing
>
>
> >
> >
> > I've been silently watching this debate for the last few
> days and was
> > unconvinced by either side until this post by Steve (I have read the
> > rest of the thread after this).
> >
> > The conditional context provides a clear delineation that a boolean
> > value is required and if a type conversion operator from a
> given type to
> > boolean is provided it is reasonable to apply it.
> >
> > I think that in VHDL in general this does not save
> significant typing
> > and does not add much value, however when you consider PSL
> assertions
> > the readability of an assertion will be greatly reduced without this
> > functionality. The current assertions only take a single conditional
> > expression so it is no big deal to just write
> >
> > assert to_boolean( ... );
> >
> > However, PSL temporal properties will have lots of conditions with
> > intervening operators.
> >
> > An example would be an assertion that says that once a bus
> master has
> > issued a write, the write state must continue until the slave has
> > accepted the write;
> >
> > always {master_state = WRITE} |->
> > {{slave_accept = '1'} | {master_state = WRITE [*];
> > master_state = WRITE and slave_accept = '1'}};
> >
> > Each of the {} above surrounds a sequential regular
> expression that is
> > composed of a series of boolean terms. To rewrite this requiring
> > booleans at each location would look like:
> >
> > always {to_boolean(master_state = WRITE)} |->
> > {{to_boolean(slave_accept = '1')} |
> > {to_boolean(master_state = WRITE [*]);
> > to_boolean(master_state = OCP_WRITE and slave_accept =
> > '1')}};
> >
> > (NOTE: the | operator above is a PSL "or" operator on
> sequences, not a
> > VHDL operator so it does not need to be wrapped in to_boolean()).
> >
> > I find the second one much harder to understand. This
> property only has
> > 4 boolean conditions. Properties with booleans above 10 will not be
> > uncommon.
> >
> > For what its worth, I think that in a boolean context, when an
> > appropriate overloaded function is available, the implicit
> application
> > of the function will greatly enhance writing and reading of
> properties.
> >
> > Jay
> >
> > ===================================
> > Jay Lawrence
> > Senior Architect
> > Functional Verification
> > Cadence Design Systems, Inc.
> > (978) 262-6294
> > lawrence@cadence.com
> > ===================================
> >
> > > -----Original Message-----
> > > From: Bailey, Stephen [mailto:SBailey@model.com]
> > > Sent: Friday, December 19, 2003 1:36 AM
> > > To: VHDL-200x
> > > Subject: RE: [vhdl-200x] Implicit conversion, Overloading, &
> > > Strong Typing
> > >
> > >
> > > Hamish,
> > >
> > > > Jim Lewis wrote:
> > > > > Actually, I believe you are comfortable with this
> > > > > behavior, you are just stuck on "implicit".
> > > > > Let me give an example:
> > > > >
> > > > > signal A, Y : unsigned (8 downto 0) ;
> > > > >
> > > > > Y <= A + "000001111" ;
> > > > > vs.
> > > > > Y <= A + 15 ;
> > > > >
> > > > > This is overloading. The compiler picks the right
> "+" operator
> > > > > to call based on the equation and we are happy. It only knows
> > > > > which one to call based on type of the operands.
> > > > >
> > > > >
> > > > > Likewise:
> > > > > if Cs = '1' and Cs2 = '1' then -- if1
> > > > > vs.
> > > > > if Cs1 and Cs2 then -- if2
> > > > >
> > > > > Here the compiler also picks the right "COND" operator for the
> > > > > expression. For the first one (if1), it sees the top
> > > > > expression is boolean so it realizes it does not need to
> > > > call "COND".
> > > >
> > > > In the first example, you specifically called "+" and
> expected the
> > > > compiler to find the right one. In the second example you
> > > > called AND it
> > > > find the right one too. That's fine and quite logical.
> > > >
> > > > But you didn't explicitly called "COND" at all. That's
> > > > foreign to VHDL.
> > >
> > > The point Jim was trying to make is that you are calling COND
> > > because the condition context requires a boolean value and a
> > > COND that matches is visible. Remember that VHDL's syntax
> > > defines the following contexts (and only these contexts) that
> > > *condition* can occur (this is documented in the proposal):
> > >
> > > - assert *condition* ...
> > > - if *condition* (if statement and if-generate)
> > > - elsif *condition*
> > > - wait [...] until *condition* [...]
> > > - when *condition* ... (conditional signal assignment,
> exit, next)
> > > - while *condition*
> > > - to be defined PSL expressions
> > >
> > > We actually discussed an alternative way to arrive at the
> > > same functionality. Since people seem to be hung up on this
> > > implicit call and cannot make the connection to how it is
> > > just a tiny extension to operator overloading capabilities
> > > already in the language:
> > >
> > > - What if assert, if, elsif, until, when and while were
> > > defined in the language as operators.
> > >
> > > - Users could then overload the operators to take a parameter
> > > of any type and return boolean.
> > >
> > > - Tools would apply subprogram overload resolution just as
> > > they do today to select which visible if, etc. operator to apply.
> > >
> > > This would work exactly like today's subprogram overloading
> > > capabilities. We thought the COND proposal would be easier
> > > to digest and accept. We may have been wrong in that regard
> > > as the if, etc. as operators proposal should not lead to
> > > people misinterpreting the proposal as Hamish (and others)
> > > have done by trying to apply it to contexts in which it isn't
> > > allowed (see next comment).
> > >
> > > (Note: The idea of if, etc. being overloaded operators would
> > > not impact how branching, etc. work. Only how the expression
> > > is interpreted as TRUE/FALSE.)
> > >
> > > > By the way, does the implicit "COND" call only apply to if?
> > > > What about
> > > > assignments to boolean, as in
> > > >
> > > > signal z: boolean;
> > > > signal x, y: bit;
> > > >
> > > > begin
> > > > z <= x and y;
> > > > end if;
> > > >
> > > > Logically this should work too, if it works with if.
> > >
> > > No, it does not logically work because this is NOT a
> > > condition context. There is no explicit context (nothing in
> > > the syntax that indicates that the LHS is boolean) which
> > > makes it obvious that the result of the RHS should be
> > > converted to boolean.
> > >
> > > We did not want the proposal to apply to this situation and
> > > it does not.
> > >
> > > -Steve Bailey
> > >
> >
>
>
This archive was generated by hypermail 2b28 : Fri Dec 19 2003 - 07:41:51 PST