There really is no need to pass the clock inference if you define the semantics correctly. There seems to be an irregularity in the way synthesis semantics are defined or the intent to be defined in different parts of the language. Generally, synthesis semantics require that tasks and functions be in-lined, i.e. expanded in place. SV has done this for the always_comb construct by expanding the sensitivity list to include effects from function calls. Concurrent assertions in procedural code (and now including for-loops) introduce what I would consider synthesis semantics in order to support that feature in simulation. Concurrent assertions in functions have been disallowed inside functions for no other reason than the lack of time and resources to fully specify the synthesis semantics in the LRM. Synthesis tools have already defined the semantics they need to implement such a feature. So I suggest that we investigate the possibility of making functions a "first class" feature supporting what's needed for assertions instead coming up with new construct that circumvent these artificial restrictions. Dave ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Mirek Forczek Sent: Wednesday, April 09, 2008 9:35 AM To: 'Korchemny, Dmitry'; 'Bresticker, Shalom'; sv-ac@server.eda.org Subject: RE: [sv-ac] 1728 mantis: "let" construct vs function following the example: a) indeed I would have to pass the clock to the function and there is a way in SV to do this properly: function bit a (ref clk, input b, input c); return $past(b,,, posedge clk) + c; endfunction always @(posedge clk) begin ... assert property (d < a(clk,b,c) ); // posedge clk is inferred here for $past(b) end (use of $past is legal in procedural code, but I'm afraid LRM do not state clearly if $past is a timing-construct ...) b) another possibility would be to introduce 'inline' for functions: function inline bit a (input b, input c); return $past(b) + c; endfunction could mean the function body will be (semantically) expanded at the call place - thus the expression will be exposed for clock infference, but this would be a brand new construct in a language. I agree generic functions would have a heavy parametrization syntax. "let" is much more concise. Unfortunatelly this advantage also cause a problem for a language integrity. "let" is a strange constuct: it has untyped parameters. It does not belong to other strictly-typed constructs in a language. Although it exists at the syntax and semantics level of the language, it is very like the preprocessor macro ... (That's why I evaluate other possibilities ...) "1) let cannot have sequences and properties as its arguments" why not ? expecially once the "let" formal arguments are untyped ... but the same claim apply for today sequence / properties as well ... both: "let" and sequence/property would greatly benefit from sequence/property-type parameters ... Regards, Mirek ________________________________ From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: 9 kwietnia 2008 16:18 To: Mirek Forczek; Bresticker, Shalom; sv-ac@server.eda.org Subject: RE: [sv-ac] 1728 mantis: "let" construct vs function Hi Mirek, 1) let cannot have sequences and properties as its arguments. 2) Parameterized functions, if eventually introduced will probably have clumsy syntax, while let definition should be concise. In formal verification it is common to write abstract generic models and syntax simplicity is very important. Unfortunately, the syntax of generic functions cannot be as you suggest: if an argument type is omitted logic is implied, so you will have to use heavy parameterization syntax to achieve the same effect. Another point is the temporal context inference which is impossible even in parameterized functions. Consider the following example: let a = $past(b) + c; ... always @(posedge clk) begin ... assert property (d < a ); // posedge clk is inferred here for $past(b) end Should you use functions you would have to explicitly pass the clock argument to the function (let alone I am not sure that using $past in functions is legal). Thanks, Dmitry ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Mirek Forczek Sent: Monday, April 07, 2008 6:31 PM To: Bresticker, Shalom; sv-ac@server.eda.org Subject: RE: [sv-ac] 1728 mantis: "let" construct vs function 1) I agree about benefit from seqeuence / property arguments. But there would be still alternative - allow sequence / property to be specified as actual parameter for the type parameter, and than we can go back to the parametrized function / tasks idea again. (other variant: introduce explicit 'sequence' and 'property' parameters as opossed to 'type' parameters (if you prefer to avoid conflicts / ambiguity with 'sequence' and 'property' apperance in contexts where the built-in types and class types are allowed as 'type' parameters), btw, the sequence and property definitions semantics would benefit greatly from the 'sequence' and 'property' parameters too, this issue was also rised some time ago .. ) 2) The context sensitivness - shall be the same for function call and let statement as long as you keep the function code following basic structural programming rule: - no global references from inside the function, Than all the sensitive data must be provided as arguments to the function, so they have to be placed explicitly at the function call construct, and thus they will be exposed exactly at the assertion sensitivity context. The "let" construct is a nice idea. But if the parametrized functions will be introduced eventually, than it may appear that the "let" will just duplicate the same capabilities that the parametrized functions will provide, and will not provide any unique capabilities any more. Mirek ________________________________ From: Bresticker, Shalom [mailto:shalom.bresticker@intel.com] Sent: 7 kwietnia 2008 16:56 To: Mirek Forczek; sv-ac@server.eda.org Subject: RE: [sv-ac] 1728 mantis: "let" construct vs function There are several advantages to let over parameterized tasks and functions (which have not been done yet because it is not trivial to do so). Others can explain them better than I. One example, though, is that let arguments can be sequences and properties. Another is their context sensitiveness. Shalom ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Mirek Forczek Sent: Monday, April 07, 2008 5:34 PM To: sv-ac@server.eda.org Subject: [sv-ac] 1728 mantis: "let" construct vs function Hi, The 1728 mantis introduces 'let' construct: the motivation is given as: "Including let expressions into packages (See Clause 25) is a natural way to implement a well-structured customization for assertions." there is an example also: // in a package let at_least_two(sig, rst = 1'b0) = rst || ($countones(sig) >= 2); // in a design reg [15:0] sig1; reg [3:0] sig2; always_comb begin q1: assert (at_least_two(sig1)); q2: assert (at_least_two(~sig2)); end I'm wondering if the same could be achieved just with functions (?): // in a package function automatic bit at_least_two(sig, rst = 1'b0); return rst || ($countones(sig) >= 2); endfunction // in a design (no change at all vs 'let' version) reg [15:0] sig1; reg [3:0] sig2; always_comb begin q1: assert (at_least_two(sig1)); q2: assert (at_least_two(~sig2)); end Are there any other benefits in having 'let' construct over already existing 'function' ? If it is about unbounded argument types in 'let' construct, a parametrized function and tasks shall be considered as an alternative. They shall provide same flexibility as the "let" construct but they would be an extension of an existing concept (function, task) instead of a brand new one (let). The parametrized function and tasks extension (functions and tasks with #parameters - in particular: with type parameters) would be consistent with already intorduced concpet of the parametrized classes - and their methods in particular. Regards, Mirek -- This message has been scanned for viruses and dangerous content by MailScanner <http://www.mailscanner.info/> , and is believed to be clean. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. --------------------------------------------------------------------- Intel Israel (74) Limited This e-mail and any attachments may contain confidential material for the sole use of the intended recipient(s). Any review or distribution by others is strictly prohibited. If you are not the intended recipient, please contact the sender and delete all copies. -- 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 Wed Apr 9 13:22:22 2008
This archive was generated by hypermail 2.1.8 : Wed Apr 09 2008 - 13:26:19 PDT