OK, I will update the proposal. Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Kulshrestha, Manisha Sent: Monday, December 17, 2007 1:21 PM To: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi, I think that should be fine. Thanks. Manisha -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Monday, December 17, 2007 4:32 PM To: Kulshrestha, Manisha; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi Manisha, Will it be sufficient to make appropriate modifications to 38.4.1 and to 38.4.2? Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Kulshrestha, Manisha Sent: Monday, December 17, 2007 12:17 PM To: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi Dimitry, I understand the logic behind this decision but at the same time I am not completely comfortable with the current wording in the proposal. I think there is a difference in past functions and future functions (atleast in the simulator). We have had $past type of functions earlier also (in fact we read sampled values in all the cases) but that does not require assertion evaluation to start. But to get future value, we need to keep the assertion alive. Anyway, it will be good to define how callbacks will work in case future value functions are present. Thanks. Manisha -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Monday, December 17, 2007 2:37 PM To: Kulshrestha, Manisha; john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi Manisha, The rationale to define the attempts this way is to make the definition consistent with the one for the past values. Consider the following examples: a1: assert property (@(posedge clk) disable iff (rst) a |=> b); a2: assert property (@(posedge clk) disable iff (rst) $past_gclk(a) |=> b); a3: assert property (@(posedge clk) disable iff (rst) a |=> $future_gclk(b)); Assume that the clock rises at times 10, 30, 50, ... and the sampled value of a is high at time 30, and the global clock ticks at 2, 4, 6, ... In case of the assertions a1 and a2 the evaluation attempt starts at time 30 and finishes at time 50, and if rst is high at time 29, it does not kill this evaluation attempt, even though $past_gclk(a) relates to the value of a at time 28. The same principle should be applied to the assertion a3. The evaluation attempt starts at time 30, and finishes at time 50, and if rst is issued at time 51, it won't kill the evaluation attempt, and if b is low at time 52, the assertion a3 will fail. Therefore I believe that the described behavior is correct. You raised an important question about callbacks, and I agree that the text should be more explicit about the callbacks. In your example it looks to me that the callback should actually occur at time 12, cb_time should be equal to 11, while attemptStartTime should be equal to 10. What do you think? Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Kulshrestha, Manisha Sent: Monday, December 17, 2007 9:03 AM To: john.havlicek@freescale.com; sv-ac@server.eda.org Subject: RE: [sv-ac] call to vote on 1682 Hi, I vote no as I have doubts about the following statements: I have some questions about the changes related to the part where $assertkill part is defined. The paragraphs say: Even though global clocking future sampled value functions depend on future values of their arguments, the interval of simulation timesteps for an evaluation attempt of an assertion containing global clocking future sampled value functions is defined as though the future sampled values were known in advance. The end of the evaluation attempt is defined to be the last tick of the assertion clock and is not delayed any additional timesteps up to the next global clocking tick. The behavior of disable iff and other asynchronous assertion related controls such as $assertkill (see 19.10) is with respect to the interval of the evaluation attempt defined above. If, for example, $assertkill is executed in a timestep strictly after the last tick of the assertion clock for the evaluation attempt, then it shall not affect that attempt, even if $assertkill is executed no later than the next global clocking tick. Now here is an example: @(posedge clk) $rising_gclk(a) |=> b; Suppose clk happens at time 10, 30, 50 etc and the global clock happens at 12. The $assertkill is issued at time 11. So, for the attempt which starts at time 10, we can not do anything about $assertkill till we reach time 12, at that point it will be decided if $rising_gclk(a) is true or false. If it is false that means the assertion attempt ended at time 10 itself and $assertkill will not have effect. But if $rising_gclk(a) is true, the assertion will get evaluated further so $assertkill will have an effect. So, we'll execute $assertkill at time 12 ??? What about the callbacks etc. associated with $assertkill ?? Based on our discussion in the meeting, I was under the impression that since we decided to execute action block at the following global tick, we'll keep the similar behavior for disable iff and other asynchronous effects. May be I missed part of the discussion. Thanks. Manisha -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of John Havlicek Sent: Thursday, December 13, 2007 8:35 PM To: sv-ac@server.eda.org Subject: [sv-ac] call to vote on 1682 Hi Folks: This is the call to vote on the revised proposal for 1682. This ballot closes on 2007-12-17 as we discussed in our meeting on 2007-12-11. There are two documents on Mantis: GlobalCLockPastNextValueFunctions1682_071213_dk.pdf FormalFuture_071022_dk.pdf Please vote if you are eligible. See the details below. J.H. ------------------------------------------------------------------------ ---------- Ballot on Mantis 1682 - Called on 2007-12-13, final ballots due by 2007-12-17 T 23:59-08:00. v[xxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[-------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[xxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[x--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xx-xxxxxxxxx-xxx-x--xx--xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor Graphics) n[---------------------------xxxxx-------x-xx-x-] Jiang Long (Mentor Graphics) n[------x------------x--xxx.....................] Joseph Lu (Altera) v[xxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper) n[------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[xx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) v[xxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[----x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[xxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |--------------------------------------------- attendance on 2007-12-11 |----------------------------------------------- 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 a 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. -- 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. -- 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. -- This message has been scanned for viruses and dangerous content by MailScanner, and is believed to be clean.Received on Mon Dec 17 03:39:24 2007
This archive was generated by hypermail 2.1.8 : Mon Dec 17 2007 - 03:39:36 PST