RE: [sv-ac] Recursive instantiation of let

Hello,

regarding the 2nd example, assign x = myxor(myxor(a,b), myxor(c,d));, unfortunately there seems to be no formal definition of the rewriting algorithm for let in the LRM.
However, there is a formal definition of rewriting for properties and sequences in Annex F.4.1.1 on page 1196. Since let also uses substitution, I think we could use the same algorithm. If I follow it correctly, it seems to me that the function flatten_property(p) will proceed by substituting the actual argument as is into the body of p', without evaluating it first. This means that
assign x = myxor(myxor(a,b), myxor(c,d)) would be expanded first as
assign x =(myxor(a,b) + myxor(c,d)), and finally
assign x = ((a+b) + (c+d))
as Dhiraj indicated.

It might be good to provide a rewrite algorithm for let in Annex F, or indicate how the one for property and sequence differs from let.

Best regards
ed

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Dhiraj Kumar Prasad
Sent: Wednesday, March 07, 2012 6:11 AM
To: Alok Kumar Sinha; sv-ac@eda.org
Cc: Dhiraj Kumar Prasad
Subject: RE: [sv-ac] Recursive instantiation of let

Hello Alok,

Recursive let instantiation is not permitted as it may result in infinite call but again this is w.r.t to let body not w.r.t usage of let.

For your second example i.e usage

assign x = myxor( myxor(a) , myxor(b) );
The number of argument for internal myxor is 1 in place of 2 and neither have default value. So it will raise error. Might you tried to write something like

assign x = myxor(myxor(a,b), myxor(c,d));

LRM clearly says that the let construct get expanded with actual argument replacing formal argument, which here stand for the replacement till any let construct
expansion is required.

So the above usage will be replaced with
       myxor(a,b) = ((a+b) + (c+d));
which is always legal.

Regards,
dhiRAj

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Alok Kumar Sinha
Sent: Wednesday, March 07, 2012 2:50 PM
To: sv-ac@eda.org
Subject: [sv-ac] Recursive instantiation of let

Hi,

According to LRM section 11.13,

"The let body gets expanded with the actual arguments by replacing the formal arguments with the actual
arguments. Semantic checks are performed to verify that the expanded let body with the actual arguments
is legal. The result of the substitution is enclosed in parentheses (...) so as to preserve the priority of evaluation
of the let body. Recursive let instantiations are not permitted."

So, it is clear that

(1) let myxor(a, b) = myxor(a) + myxor(b);

is illegal since it is having same let instantiation in its body.

Now if there is a case where a let is defined as,

(2) let myxor(a, b) = a + b;

, and for a let instantiation like

assign x = myxor( myxor(a) , myxor(b) );

Will it be expanded to :
let myxor(a, b) = myxor(a) + myxor(b);

I other words, does that mean - the instantiation becomes recursive.

According to my interpretation, when formal arguments get replaced with the actuals in the let body, it will result in
a let defined as in (1), and hence should become recursive.

Anyone, please confirm if my understanding is correct or if I am missing anything.

Thanks and Regards
Alok

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