RE: [sv-ac] 1728 mantis: "let" construct vs function

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Wed Apr 09 2008 - 07:18:27 PDT
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.

-- 
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.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Wed Apr 9 07:23:05 2008

This archive was generated by hypermail 2.1.8 : Wed Apr 09 2008 - 07:23:24 PDT