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.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.