[sv-ac] 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, and is
believed to be clean.