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  <http://www.mailscanner.info/> MailScanner, 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  <http://www.mailscanner.info/> MailScanner, and is 
believed to be clean. 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.