Re: [sv-ac] [Fwd: Clock flow in SV assertion]

From: John Havlicek <john.havlicek_at_.....>
Date: Wed Mar 08 2006 - 06:05:11 PST
Surya:

The treatment of "@" as an operator is a device for parsing.
Therefore, you cannot deduce from the precedence assigned
to "@" for the purpose of parsing or the groupings that result
that the SVA example is wrong.  You have to use a combination
of parsing and semantic analysis, and you have to understand
what are the artificial effects of your parsing devices.

I know a number of tool teams have solved this problem already.
Perhaps someone else watching the reflector can help you.

Best regards,

John H.

> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> Date: Wed, 08 Mar 2006 19:19:29 +0530
> From: Surya Pratik Saha <spsaha@cal.interrasystems.com>
> X-Accept-Language: en
> Cc: sv-ac@eda.org
> X-Virus-Status: Clean
> Sender: owner-sv-ac@eda.org
> X-OriginalArrivalTime: 08 Mar 2006 13:50:14.0164 (UTC) FILETIME=[39BAF540:01C642B7]
> 
> <!doctype html public "-//w3c//dtd html 4.0 transitional//en">
> <html>
> Hi John,
> <br>Then I need to know the precedence of "@". That will automatically
> distiguish the real parentheses and fake parentheses.
> <p>Ed also mentioned in one of the mail that @ has the weakest precedence.
> <p>I&nbsp;am not sure, the mail you got or not.
> <p>But then considering @ as weakest the e.g. given will be parsed as I
> mentioned by using parentheses. That is:
> <br>@(posedge clk) a ##1 (@(posedge clk1) s1 |=> @(posedge clk2)s2);
> <p>So the e.g. is wrong as I explained earlier.
> <p>If otherwise, then can you tell me what it wants to mean by putting
> explicit parenthesis there?
> <p>John Havlicek wrote:
> <blockquote TYPE=CITE>Hi Surya:
> <p>I am not a parsing expert, but I think that you can treat "@" as
> <br>an operator and make up a precedence for it for the purpose
> <br>of reading it in.&nbsp; Not all choices may be equally good.&nbsp;
> :)
> <p>You have to distinguish "real" parentheses that were written
> <br>in the property from "fake" ones that get introduced in parsing.
> <p>Then you could go back over your parsed structure and figure
> <br>out, according to the clock flow rules, what the scope of each
> <br>clocking event is.
> <p>Best regards,
> <p>John H.
> <p>> Sender: spsaha@cal.interrasystems.com
> <br>> Date: Wed, 08 Mar 2006 18:42:25 +0530
> <br>> From: Surya Pratik Saha &lt;spsaha@cal.interrasystems.com>
> <br>> X-Accept-Language: en
> <br>> CC: sv-ac@eda.org
> <br>> X-OriginalArrivalTime: 08 Mar 2006 13:11:27.0485 (UTC) FILETIME=[CEEBEAD0:01C642B1]
> <br>>
> <br>> &lt;!doctype html public "-//w3c//dtd html 4.0 transitional//en">
> <br>> &lt;html>
> <br>> Hi John,
> <br>> &lt;br>Even if I dont consider @ as operator, I have to know the
> precedence
> <br>> to implement sequence/property expression in an yacc file. And also
> the
> <br>> LRM has the following rule:
> <br>> &lt;p>property_expr ::=
> <br>> &lt;br>sequence_expr
> <br>> &lt;br>...
> <br>> &lt;br>| clocking_event property_expr
> <br>> &lt;p>So in which context an item will be reduced with "clocking_event
> property_expr"
> <br>> has to be well defined.
> <br>> &lt;p>LRM is not clear on that.
> <br>> &lt;p>John Havlicek wrote:
> <br>> &lt;blockquote TYPE=CITE>Surya:
> <br>> &lt;p>> Some days ago I asked the precedence of @ operator in assertion
> rule.
> <br>> &lt;br>> I did not get well defined answer, however by reading the
> clock flow
> <br>> section,
> <br>> &lt;br>> it is understood that @ has the weakest precedence.
> <br>> &lt;p>Ed answered you that "@" is not an assertion expression operator,
> <br>> &lt;br>so your line of reasoning to deduce that the LRM example
> <br>> &lt;p>> @(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge clk2)
> s2;
> <br>> &lt;p>is wrong is flawed.
> <br>> &lt;p>I will repeat Ed's answer:&amp;nbsp; in SVA, "@" is not an
> expression
> <br>> &lt;br>operator.
> <br>> &lt;p>Best regards,
> <br>> &lt;p>John H.
> <br>> &lt;p>> X-Authentication-Warning: server.eda.org: majordom set sender
> to owner-sv-ac@eda.org
> <br>> using -f
> <br>> &lt;br>> Date: Wed, 08 Mar 2006 15:22:41 +0530
> <br>> &lt;br>> From: Surya Pratik Saha &amp;lt;spsaha@cal.interrasystems.com>
> <br>> &lt;br>> X-Accept-Language: en
> <br>> &lt;br>> X-Virus-Status: Clean
> <br>> &lt;br>> Sender: owner-sv-ac@eda.org
> <br>> &lt;br>> X-OriginalArrivalTime: 08 Mar 2006 09:55:09.0683 (UTC) FILETIME=[62CDF430:01C64296]
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;!doctype html public "-//w3c//dtd html 4.0 transitional//en">
> <br>> &lt;br>> &amp;lt;html>
> <br>> &lt;br>> &amp;amp;nbsp;
> <br>> &lt;br>> &amp;lt;p>-------- Original Message --------
> <br>> &lt;br>> &amp;lt;table BORDER=0 CELLSPACING=0 CELLPADDING=0 >
> <br>> &lt;br>> &amp;lt;tr>
> <br>> &lt;br>> &amp;lt;th ALIGN=RIGHT VALIGN=BASELINE NOWRAP>Subject:&amp;amp;nbsp;&amp;lt;/th>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;td>Clock flow in SV assertion&amp;lt;/td>
> <br>> &lt;br>> &amp;lt;/tr>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;tr>
> <br>> &lt;br>> &amp;lt;th ALIGN=RIGHT VALIGN=BASELINE NOWRAP>Date:&amp;amp;nbsp;&amp;lt;/th>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;td>Wed, 08 Mar 2006 10:28:44 +0530&amp;lt;/td>
> <br>> &lt;br>> &amp;lt;/tr>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;tr>
> <br>> &lt;br>> &amp;lt;th ALIGN=RIGHT VALIGN=BASELINE NOWRAP>From:&amp;amp;nbsp;&amp;lt;/th>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;td>Surya Pratik Saha &amp;amp;lt;spsaha@cal.interrasystems.com>&amp;lt;/td>
> <br>> &lt;br>> &amp;lt;/tr>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;tr>
> <br>> &lt;br>> &amp;lt;th ALIGN=RIGHT VALIGN=BASELINE NOWRAP>To:&amp;amp;nbsp;&amp;lt;/th>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;td>"sv-bc@eda.org" &amp;amp;lt;sv-bc@eda.org>, sv-ac@eda.org&amp;lt;/td>
> <br>> &lt;br>> &amp;lt;/tr>
> <br>> &lt;br>> &amp;lt;/table>
> <br>> &lt;br>>
> <br>> &lt;br>> &amp;lt;p>Hi,
> <br>> &lt;br>> &amp;lt;br>Some days ago I asked the precedence of @ operator
> in assertion
> <br>> rule.
> <br>> &lt;br>> I did not get well defined answer, however by reading the
> clock flow
> <br>> section,
> <br>> &lt;br>> it is understood that @ has the weakest precedence.
> <br>> &lt;br>> &amp;lt;p>Considering the fact the given e.g. in LRM (page
> no. 282, e.g.
> <br>> d)
> <br>> &lt;br>> &amp;lt;p>@(posedge clk) a ##1 @(posedge clk1) s1 |=> @(posedge
> clk2)
> <br>> s2;
> <br>> &lt;br>> &amp;lt;p>will be parsed as:
> <br>> &lt;br>> &amp;lt;p>@(posedge clk) a ##1 (@(posedge clk1) s1 |=> @(posedge
> clk2)
> <br>> s2);
> <br>> &lt;br>> &amp;lt;p>So (@(posedge clk1) s1 |=> @(posedge clk2) s2)
> will become
> <br>> a property
> <br>> &lt;br>> expression.
> <br>> &lt;br>> &amp;lt;p>But as per assertion BNF, ## operator can not
> have property
> <br>> expression
> <br>> &lt;br>> in RHS. So the e.g. given in LRM is wrong.
> <br>> &lt;br>> &amp;lt;p>Please confirm.
> <br>> &lt;br>> &amp;lt;pre>--&amp;amp;nbsp;
> <br>> &lt;br>> Regards
> <br>> &lt;br>> Surya.&amp;lt;/pre>
> <br>> &lt;br>> &amp;amp;nbsp;&amp;lt;/html>
> <br>> &lt;br>>&lt;/blockquote>
> <br>>
> <br>> &lt;pre>--&amp;nbsp;
> <br>> Regards
> <br>> Surya.&lt;/pre>
> <br>> &amp;nbsp;&lt;/html>
> <br>></blockquote>
> 
> <pre>--&nbsp;
> Regards
> Surya.</pre>
> &nbsp;</html>
> 
Received on Wed Mar 8 06:05:26 2006

This archive was generated by hypermail 2.1.8 : Wed Mar 08 2006 - 06:06:01 PST