Also are mine. Thanks, Dmitry -----Original Message----- From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com] Sent: Thursday, November 01, 2007 6:45 PM To: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi, My comments are included: Manisha -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, October 30, 2007 7:45 PM To: Kulshrestha, Manisha; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi Manisha, Please, see my comments below. I've uploaded a version with fixes and also am attaching it here. Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Kulshrestha, Manisha Sent: Tuesday, October 30, 2007 8:54 AM To: john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi, I vote 'no' with the following comments. 1. The proposal says: "$steady_gclk(expression) returns true if the sampled value of the expressions does not change at the next global clock tick. Otherwise it returns false." I think it should have same type of wording as $falling_gclk has (i.e. if the sampled value of the LSB of the expression ....) [Korchemny, Dmitry] I don't think so. Its definition should be consistent with $stable, and the definition of $stable explicitly says: " $stable returns true if the value of the expression did not change. Otherwise, it returns false." MK> OK. I checked the definition of $stable and this is fine. 2. The proposal says: "The use of these functions is limited to assertion features only. It shall be an error to invoke these functions outside of property expressions, this also implies that they shall not be used in assertion action blocks." Is 'assertion features' defined any where ? I believe these functions can be used in sequences. Because the second sentence says that these can not be used outside of property expressions. May be the sentence should be something like " These functions shall be used only in the concurrent assertion boolean expressions". [Korchemny, Dmitry] I rewrote this paragraph as: "It shall be an error to invoke the global clocking sampled value functions outside of property expressions, this also implies that they shall not be used in assertion action blocks." MK> I am assuming that you mean that these global clocking sampled value functions can be used only in property_expr. Somehow the term property expressions is being used in the LRM to imply assertions also. E.g. 4.4.2.6 has "The code specified by blocking assignments in the program block and the pass/fail code from property expressions are scheduled in the Reactive region. The Reactive region is the reactive region set dual of the Active region (see 4.4.2.2)." Also, are these functions allowed in sequences expressions ? [Korchemny, Dmitry] I believe that the usage of "property expression" in 4.4.2.6 is wrong and should be fixed. In other cases property expression and property_expr are used interchangeably. I rewrote the above statement as: "The global clocking sampled value functions may be invoked only in property_expr or in sequence_expr; this implies that they shall not be used in assertion action blocks." 3. It says: "Additional restrictions are imposed on the usage of the global clocking future sampled value functions: they shall not be nested and they shall not be used in assertions containing sequence match items (see 16.9, 16.10)." So, these restrictions are only for future sampled value functions. Not for past ones. How would a nested $past() work ? Either way it needs more clarity. [Korchemny, Dmitry] I don't think we should provide more explanations for the past value functions here, since regular $past functions can be nested. If you think that the definition of the nesting of the regular $past functions is not clear enough, it should be a subject of a separate mantis. 4. It says "An evaluation attempt of an assertion containing global clocking future sampled value functions ends at the global clocking tick that follows the assertion clock tick at which the final boolean expression of the assertion is evaluated,". I think there should be a '.' instead of ',' at the end of this statement. [Korchemny, Dmitry] Fixed. Also it kind of implies that all the attempts of a assertion containing future sampled value function will end at the next global clock tick. This may not be the case if the last Boolean expression (which caused failure or pass) does not contain future sampled value function. [Korchemny, Dmitry] I think that this will be difficult to define and implement. It is also easier to the user when the definition is simple. In the same paragraph it is using ":", is that according to the standard ? I am not sure. [Korchemny, Dmitry] Why is it forbidden to use a colon in the LRM? Could you be more specific? MK> Here is the original sentence: Note however, that the behavior of the disable iff clause and other asynchronous assertion related controls (e.g. $assertkill, see 19.10) remains consistent with its behavior for assertions without global clocking future sampled value functions (see 16.12): the completion of the property evaluation does not include (or is not contingent on) the additional global clocking tick. MK> You just sent out email that you plan to remove the statements about evaluation attempt. I am just wondering if this proposal needs to clarify anything about disable iff or $assertkill. If the proposal does not say anything then it implies that the behavior of these things is not changing with the introduction of these new functions. What do you think ? [Korchemny, Dmitry] I removed the previous paragraph and added the following text. This behavior also follows from the description of the formal semantics. I will appreciate if you could suggest a better formulation. For assertions containing global clocking future sampled value functions the behavior of the disable iff clause and other asynchronous assertion related controls (e.g. $assertkill, see 19.10) remains consistent with its behavior for assertions without global clocking future sampled value functions (see 16.12). Example 3. Assume that the signal rst is high between times 82 and 84, and is low at all other time moments. Then the following assertion a3: assert property (@$global_clock disable iff (rst) $changing_gclk(sig) |-> $falling_gclk(clk)) else $error("sig is not stable"); fails at time 80 (see Figure 16-14 Note to the editor: please, adjust the reference), since rst was inactive between times 70 and 80. Thanks. Manisha -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek Sent: Wednesday, October 24, 2007 6:21 AM To: sv-ac@server.eda.org Subject: [sv-ac] call to vote on 1682 Hi Folks: As we agreed in today's meeting, I am calling for a vote on 1682. The documents are GlobalClockPastNextValueFunctions1682\ 071016_dk.doc GlobalClockPastNextValueFunctions1682\ 071016_dk.pdf on Mantis. These two should be identical from a technical perspective. Please vote if you are eligible. See the details below. J.H. ------------------------------------------------------------------------ ---------------- Ballot on Mantis 1682 - Called on 2007-10-23, final ballots due at 2007-10-30 T 23:59-07:00. v[xxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[xxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) n[--------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) n[------------x--xxx.....................] Joseph Lu (Altera) v[xxxxxxxxx..............................] Johan Martensson (Jasper) n[-----------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) v[-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[xxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |--------------------------------------- attendance on 2007-10-23 |----------------------------------------- voting eligibility for this ballot |------------------------------------------ email ballots received Legend: x = attended - = missed r = represented . = not yet a member v = valid voter (2 out of last 3 or 3/4 overall) n = not valid voter t = chair eligible to vote only to make or break a tie -- This message has been scanned for viruses and dangerous content by 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. --------------------------------------------------------------------- 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, and is believed to be clean.Received on Mon Nov 5 06:12:40 2007
This archive was generated by hypermail 2.1.8 : Mon Nov 05 2007 - 06:12:48 PST