RE: [sv-ac] RE: call to vote on 1900

Hi Manisha,

Please, see my comments below. I uploaded the updated version
checkers_080110dk.pdf into Mantis.

Thanks,
Dmitry

-----Original Message-----
From: Kulshrestha, Manisha [mailto:Manisha_Kulshrestha@mentor.com] 
Sent: Wednesday, January 09, 2008 7:06 PM
To: Korchemny, Dmitry; john.havlicek@freescale.com; sv-ac@server.eda.org
Cc: Bustan, Doron; eduard.cerny@synopsys.com; yaniv.fais@freescale.com;
johan.martensson@jasper-da.com; piper@cadence.com; Seligman, Erik;
bassam.tabbara@synopsys.com; thomas.thatcher@sun.com
Subject: RE: [sv-ac] RE: call to vote on 1900

Hi Dimitry,

Please see my comments below:

Thanks.
Manisha

Hi Dimitry,

The sequence methods are allowed in continuous assignments to checker
variables. But this contradicts with the language in section 16.13.6,
where it says the following:


The ended status of the sequence is set in the Observe region and
persists
through the Observe region. This method shall only be used to detect the
end point of a sequence used
in another sequence.

The triggered status of the sequence is set in the Observe region and
persists through the remainder of the time step. This method shall only
be used in wait statements or boolean
expressions (see 9.4.4) outside of sequence context or in the disable
iff boolean expression for
properties.

[Korchemny, Dmitry] I don't see any contradiction with the subclause
16.13.6 here since the assignments to checker variables are performed in
the Observed region.

MK> Since 16.13.6 describes where all these methods can be used, that
section needs enhancement to mention that these methods can be used in
checkers assignments also. So far, I do not think these methods are
allowed in continuous assignments. So far only method 'triggered' was
allowed out of assertions and that too had certain restrictions as
stated in "This method shall only be used in wait statements or Boolean
expressions (see 9.4.4) outside of sequence context or in the disable
iff boolean expression for properties."

[Korchemny, Dmitry 2] There already is a corresponding note in the
proposal about ended usage in checker variable assignments (section
16.13.6). I also added the notes for triggered and matched methods.

Dimitry, I think we discussed this in one of the last meetings and
decided that the example and the language needs some fixing ? Since so
far 'matched' was not allowed out of sequences, some clarification is
needed how it will work in sequential and continuous assignments. How
the clock synchronization will happen ?

[Korchemny, Dmitry] There are some explanations in the text. The
fragment describing sequence methods (including 'matched') currently
reads (page 16):
***
The right-hand side of a checker variable assignment may contain
sequence methods ended and triggered (see 16.8.10), which can be used in
this case interchangeably, and the sequence method matched. The matched
method has its usual meaning in nonblocking assignments, and has the
same effect as ended and triggered in continuous assignments. For
example:

MK> I think the first sentence should clarify that ended and triggered
should be used in same clock case and matched should be used in multi
clock case. I am not comfortable with 'usual meaning' wording for
matched. So far the matched was not allowed anywhere other than
assertion so which 'usual meaning' we are referring to here ? Also,
saying that matched has same effect as ended and triggered is not right.
At least in assertions, in non-multiclock cases the usage of matched and
ended gives different results. 

[Korchemny, Dmitry 2] I rewrote the paragraph as:

"The right-hand side of a checker variable assignment may contain
sequence methods ended and triggered, which can be used in this case
interchangeably, and the sequence method matched (see 16.8.10 and
16.13.6). In nonblocking assignments the matched method provides
synchronization between the clock of the sequence and the clock
controlling the assignments; it has the same effect as ended and
triggered in continuous assignments. The ended (or triggered) method
should be used in nonblocking assignments when the sequence clock
coincides with the assignment clock, and in continuous assignments; the
matched method should be used in nonblocking assignments when the
sequence clock is different from the assignment clock."

I think that the sentence "it [the matched method] has the same effect
as ended and triggered in continuous assignments" is correct, since it
says that all three methods may be used interchangeably in the
continuous assignments and have that they have the same effect. It is
explicitly specified here that the matched method is considered in the
assignment context, and not in the context of a sequence/property.

When sequence matches, the ended becomes true at the same clock edge but
the matched can be read true only at the next clock edge. P1800 strictly
says that matched only becomes true at next tick of the writer clock and
remains true until the first clock edge of the reader clock. 


// a, b, c, d, clk1 and clk2 are bit variables defined elsewhere
sequence s1;
	@clk1 c ##[0:$] d;
endsequence : s1
sequence s2;
	@clk2 c ##[0:$] d;
endsequence : s1

checkvar bit x, y = 1'b0, z = 1'b0, u = 1'b0;
assign x = a && b;
always_check @clk1 begin
	y <= x && s1.ended;
	// y <= x && s.triggered; has the same meaning

	z <= s2.matched;
	u <= s2.ended;
end
Suppose that the sequence s2 has a match at time 80 and the nearest tick
of clk1 happens at time 90. Then at time 90 z will be assigned the value
1'b1 since match stores the result of s2 match until the arrival of the
first clk1 tick after the match (see 16.13.5). On the contrary, the
value of u at time 90 will be 0 since there is no match of s2 at time
90.
***

Could you send your suggestion how to clarify the text?

Thanks.
Manisha

-----Original Message-----
From: John Havlicek [mailto:john.havlicek@freescale.com] 
Sent: Monday, December 31, 2007 10:28 PM
To: sv-ac@eda.org
Cc: doron.bustan@intel.com; eduard.cerny@synopsys.com;
yaniv.fais@freescale.com; john.havlicek@freescale.com;
dmitry.korchemny@intel.com; Kulshrestha, Manisha;
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
---------------------------------------------------------------------
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.