Thanks, This addresses my concerns - I'm sorry I didn't explain this properly (I found it hard to do without a real waveform example). Yaniv -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, January 08, 2008 14:16 To: Fais Yaniv; sv-ac@eda.org Subject: RE: [sv-ac] RE: call to vote on 1900 Hi Yaniv, Now I understand your concern: it is not intuitive to call the assignments equivalent in the simulation (though, strictly speaking, this is a matter of definition). Therefore I rewrote the text without using the notion of equivalence, and deposited it into Mantis: The simulation of the nonblocking assignments containing future value function invocations in their right-hand side is defined using rewriting of the assignment to a continuous assignment by shifting the whole assignment towards the past by one tick of the global clock. The following example illustrates the rewriting algorithm. Given the nonblocking assignment: // clk, expr, b and c defined elsewhere checkvar bit a = expr; always_check @clk a <= b && $future_gclk(c); The new form after rewriting is: assign a = $changed_gclk(clk) ? $past_gclk(b) && c : $past_gclk(a); This form is used only starting from the second tick of the global clock. Before it the initial value of a is kept. Note that in this case the variables a and b are sampled by the global clock, and their behavior between two consecutive ticks of the global clock is ignored. Thanks, Dmitry -----Original Message----- From: Fais Yaniv [mailto:yaniv.fais@freescale.com] Sent: Tuesday, January 08, 2008 1:24 PM To: Korchemny, Dmitry; sv-ac@eda.org Subject: RE: [sv-ac] RE: call to vote on 1900 Hi, I think the equivalence you define is correct for a model where all the signals may change only when the global clock changes, I was only saying that this equivalence is relying on some assumption which isn't entirely correct for simulation when signals (some of them coming from test bench) don't always change in the same time step as the fastest clock. This behavior (signals changing in time steps where the global clock doesn't change) can come from an improper (but not illegal) definition by the user of the global clock or simply by signals driven by the testbench at various time points, at this situation the user will see in the waveform a signal which behaves differently than a clock governed non blocking assignment since the signal may change not at the clock edge (like an assign). This scenario, as noted above , can occur not only because of a glitch, the proper solution would be to allow updating the variable using the future value just *before* the clock tick and only then, since this is too awkward I'm personally fine with the assign solution as a long as it would be noted that this isn't equivalent in simulation and in some cases it may behave differently (if the assumption made for formal verification doesn't hold). Yaniv -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, January 08, 2008 11:23 To: Fais Yaniv; sv-ac@eda.org Subject: RE: [sv-ac] RE: call to vote on 1900 Hi Yaniv, This definition is consistent with 1682. The situation you describe is a glitch, and in many cases it is even desirable to ignore it - this is a common situation with the concurrent assertions. And what would you suggest for the following assignment: always_check @clk a <= b && $future_gclk(c) && $future_gclk(d); if c and d change at different time steps? Thanks, Dmitry -----Original Message----- From: Fais Yaniv [mailto:yaniv.fais@freescale.com] Sent: Tuesday, January 08, 2008 11:00 AM To: Korchemny, Dmitry; sv-ac@eda.org Subject: RE: [sv-ac] RE: call to vote on 1900 Hi Dmitry, what if you define a global clock to be a clock which is slower than the "clk" ? (I know this isn't the intention but we never said this isn't allowed). in this case the always_check would be updated in a faster rate than the assign looking at "$past_gclk(b) && c", this can cause inconsistency if "b" would be changing not a the global clock rate. The source of the problem isn't with the "clk" however but with all signals which can change in between ticks of the global clock - this shouldn't happen in formal verification if indeed the global clock is the fastest system clock but in simulation you can have time step delays, now since the "assign" is always evaluated it can get to look at "c" not at a global clock tick time point, if at this time point the value of "c" is different than the future value at the next global clock tick than an inconsistency can occur. Regards, Yaniv always_check @clk a <= b && $future_gclk(c); assign a = $changed_gclk(clk) ? $past_gclk(b) && c : $past_gclk(a); -----Original Message----- From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] Sent: Tuesday, January 08, 2008 09:25 To: Fais Yaniv; Havlicek John; sv-ac@eda.org Subject: RE: [sv-ac] RE: call to vote on 1900 Hi Yaniv, Please, see my comments below. Thanks, Dmitry -----Original Message----- From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Fais Yaniv Sent: Monday, January 07, 2008 8:02 PM To: Havlicek John; sv-ac@server.eda.org Subject: [sv-ac] RE: call to vote on 1900 I vote yes with the following minor amendment: page 7: checker_instantiation ::= checker_identifier name_of_instance ([list_of_port_connections]) ; should be same as page 32: checker_identifier name_of_instance ([list_of_checker_port_connections]) ; [Korchemny, Dmitry] Fixed. also, on page 23 it is written: always_check @clk a <= b && $future_gclk(c); The equivalent form after rewriting is: assign a = $changed_gclk(clk) ? $past_gclk(b) && c : $past_gclk(a); I think it should be added that there is an assumption that all those signals do not change between edges of the global clock , otherwise in simulation a bad definition of global clock (that is a definition of an event which isn't necessarily the fastest one) means the above isn't equivalent (since if you look at the value of "a" thus by the assign the values of "clk" or "c" between edges of the global clock you can see different values than those in the actual edge of the global clock). [Korchemny, Dmitry] I think this definition is consistent with the definition of $future_gclk in simulation for assertions. $future_gclk(c) means the value of c at the next tick of gclk, even if c changed before that. Yaniv -----Original Message----- From: John Havlicek [mailto:john.havlicek@freescale.com] Sent: Monday, December 31, 2007 18:58 To: sv-ac@eda.org Cc: doron.bustan@intel.com; eduard.cerny@synopsys.com; Fais Yaniv; Havlicek John; dmitry.korchemny@intel.com; Manisha_Kulshrestha@mentor.com; johan.martensson@jasper-da.com; piper@cadence.com; erik.seligman@intel.com; bassam.tabbara@synopsys.com; thomas.thatcher@sun.com Subject: call to vote on 1900 Hi Folks: Since my last call to vote on 1900 did not reach the reflector, I am calling for a new, 1-week vote. This is that call. I have copied the eligible voters individually because the reflector seems unreliable. Please send your ballot both to the reflector and to me individually. Please vote if you are eligible. See the details below. J.H. ------------------------------------------------------------------------ ---------- Ballot on Mantis 1900 - Called on 2007-12-31, final ballots due by 2008-01-07 T 23:59-08:00. v[xxxxxxxxxxxxxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Intel) v[xxx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys) n[--------------------x-xxx---------x-x-xxx-x---x] Surrendra Dudani (Synopsys) v[xxxxxx-xxxxxx-xxxxxxxxx-xx-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale) t[xx--xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale - Chair) v[xxxxxxxxxxxxxxxxxxxxxxxxxxxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel - Co-Chair) v[xxx-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[xxxxxxxxxxxxxxxxx..............................] Johan Martensson (Jasper) n[-------------------------x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale) v[xxx-xxxx-xxxxxxxxxxxxxxxxxxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence) v[xxxx-x-x-xx-xxxxxxx-x-xxxxx-x..................] Erik Seligman (Intel) n[-----x-x----x--------xxxx-----xxxx-xx----------] Tej Singh (Mentor Graphics) v[xxxx-x-xxxxxx--xxxxxxxx-xxxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys) v[xxxxxxx-xxxxxxxxxxxxx-xxxxxxxxxx...............] Tom Thatcher (Sun Microsystems) |----------------------------------------------- attendance on 2007-12-18 |------------------------------------------------- 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. --------------------------------------------------------------------- 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. --------------------------------------------------------------------- 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 Tue Jan 8 05:25:48 2008
This archive was generated by hypermail 2.1.8 : Tue Jan 08 2008 - 05:26:00 PST