[sv-ac] RE: Mantis 3202: $ function in classes & constraints, seeking comments on outline

From: Eduard Cerny <Eduard.Cerny@synopsys.com>
Date: Mon May 23 2011 - 13:24:56 PDT

Hi Erik,

if the class instance does not exists yet, I think that reference to the a past value of its non-static member should error out due to null pointer, like any other kind of reference to it, no?

Thanks,
ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik
Sent: Monday, May 23, 2011 4:20 PM
To: sv-ac@eda-stds.org
Subject: [sv-ac] RE: Mantis 3202: $ function in classes & constraints, seeking comments on outline

Hi guys-Here's an outline of my current thoughts on adding the assertion system functions to classes and constraints. Please take a look & send comments if you are interested in this area. Ben, Anupam-I believe you mentioned at the last meeting that you could help with this.

Classes
  - Bit vector functions are already allowed: add example
  - For sampled value functions (past or future), need to define notion of sampled value of class variable
    = Static class variables: Treat like other static variables, take value from Preponed region
    = Automatic class variables
        = Option 1: Assume that class variables will come & go often in typical usage, so treat like other automatic vars. Sampled value == current value in current timestep, but when past or future referred to, uses postponed value from that time step. If the variable does not exist at the designated time, use the initial value.
        = Option 2: Assume that more common usage case is that class exists for a long time, and we want to treat its variables like static design variables when relevant. So define sampling as value from Preponed region for any timestep (including current one) where the variable exists, otherwise use the initial value.

- Constraints
   - Bit vector functions: LRM says "Constraints can be any SystemVerilog expression with variables and constants of integral type (e.g., bit, reg, logic, integer, enum, packed struct).". Since each of the $ bit vector functions could theoretically be rewritten as a boolean or integer expression, would there be any downside to simply adding in section 18.3 that they are permitted?
        = Could argue that 18.5.11 (functions in constraints) implicity allows them anyway, but can't hurt to clarify.
        = Complication: Constraints support only 2-state values. But I think this is OK: state that X or Z value is illegal & will result in error. Compilers can implicitly generate 2-state versions of the $ function expressions.
   - Sampled value functions: Adding these to constraints would be a major change, since current restrictions prevent the need to save state & solve constraints across time. So my instinct is to NOT enhance constraints to allow these.
        = Another option would be to relax the rules not allowing state in constraints, and add language like 17.7.2 (solving assume sets for checker random variables).

From: Rich, Dave [mailto:Dave_Rich@mentor.com]
Sent: Friday, May 13, 2011 11:42 PM
To: Seligman, Erik; sv-ac@eda-stds.org
Subject: RE: Mantis 3202: $ function in classes & constraints, future $ value functions in 'let'

Erik, See comments below.

Dave

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Seligman, Erik
Sent: Friday, May 13, 2011 1:13 PM
To: sv-ac@eda-stds.org
Subject: [sv-ac] Mantis 3202: $ function in classes & constraints, future $ value functions in 'let'

Hi guys-
I'm looking again at proposal 3202, where we had discussed extending the use of the various system functions to classes and constraints, and allowing future value functions in 'let'. I'm not sure I fully understand some of the issues here; can some of you clarify for me?

1. In the case of the bit vector functions ($countones, etc)-I didn't see any specific language (in the LRM or our 2476 proposal) that keeps them out of classes and constraints. Is there a reason people think they are currently prohibited there, or do we just need to clarify, perhaps with some additional examples, that they are not?
[DR] The problem with these functions is not whether they are allowed or not (they are), it's that functions are treated like black boxes when it comes to constraints. There's no synthesis/formal-like semantics that recognizes functions as Boolean expressions. The constraint section in the LRM says that functions divide the constraint space into an ordered set - solve for the random inputs to the function, then use the output as a non-random value. In the current LRM, we have to make specific exceptions for certain functions to be treated as Boolean expressions instead.

2. For the sampled value functions-was there a reason why we didn't want them in classes and constraints? Could we put language like, "These functions are allowed in any context in which their return type is valid"?
[DR] There are construction and lifetime issues with classes. How would you sample before the class is constructed?

3. Similarly, if we want to allow future functions in 'let', could we add language like, "These are allowed in a let expression, provided that when it is instantiaed, the substituted expression is legal"?
[DR] I don't think this is needed. The LRM already says "Semantic checks are performed to verify that the expanded let body with the actual arguments is legal."

Thanks!

--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
--
This message has been scanned for viruses and
dangerous content by MailScanner<http://www.mailscanner.info/>, and is
believed to be clean.
-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon May 23 13:25:35 2011

This archive was generated by hypermail 2.1.8 : Mon May 23 2011 - 13:25:39 PDT