FW: [sv-ac] call to vote on Mantis 1674

From: Eduard Cerny <Eduard.Cerny_at_.....>
Date: Tue May 01 2007 - 10:12:30 PDT
To open up the discussion and hopefully converge on a solution. perhaps
some additional wording...
 
Best regards,
ed
--------------------------------------------------------

 
Hi Manisha,
 
The text says:
 
---
When an inferred expression system function is used as the default value
on a formal argument to a property or a sequence, it is replaced by the
inferred expression as determined at the point where the property or
sequence is instantiated. Therefore, if the instance is the top
expression in a verification statement, the event expression that is
used to replace the default argument $inferred_clock is that as
determined at the location of the verification statement. If the
instance is not the top-level property expression in the verification
statement then the event expression determined by clock-flow rules up to
the instance location in the property expression is used as the default
value of the argument. If $inferred_clock is used directly as a clocking
event in the property expression then its value is determined by clock
flow rules after the full expansion of property and sequence instances.
---
 
I think that if it is specified as the default value, then it should be
substituted there and the propagated. This is as with any other value
passed as default.
 
Regarding the case when it is not top-level property, the text indicates
what to do:
 
"If the instance is not the top-level property expression in the
verification statement then the event expression determined by
clock-flow rules up to the instance location in the property expression
is used as the default value of the argument."
 
This means that if you pass it as the actual, it is replaced by clock
flow rules at the position of the instance. 
 
What else should it say? Would more examples help?
 
Thanks,
 
ed
 
 
 
 
 
 
 
 


________________________________

	From: Kulshrestha, Manisha
[mailto:Manisha_Kulshrestha@mentor.com] 
	Sent: Friday, April 27, 2007 3:09 PM
	To: Eduard Cerny
	Subject: RE: [sv-ac] call to vote on Mantis 1674
	
	

	Hi Ed,

	 

	It is based on the proposal you sent.  What is not intuitive is
the fact that, if $inferred_clock was already  in the property
expression, it behaves differently than if passed as a argument.  

	 

	Also, now that I think about it more, what happens when
$inferred_clock is not a default argument but it is passed by the user ?

	 

	E.g. assert property (p_triggers(a, b, c, $inferred_clock)); 

	 

	What happens when p_triggers is not a top property ? The current
language does not clarify this.  Does this behave like default argument
or property expression ?

	 

	As far as need for such a thing is concerned, I understand that.
I do not have any alternative way to do this either at this point.

	 

	Thanks.

	Manisha

	 

	 

	From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com] 
	Sent: Friday, April 27, 2007 10:47 AM
	To: Kulshrestha, Manisha
	Cc: Eduard Cerny
	Subject: FW: [sv-ac] call to vote on Mantis 1674

	 

	Hi Manisha,

	 

	one more question - did you base your vote on this modified
proposal that I sent on 4/23 for your comments or is it on the proposal
on Mantis?

	 

	Thanks,

	ed

	 

________________________________

	From: Eduard Cerny [mailto:edcerny@synopsys.COM] 
	Sent: Monday, April 23, 2007 5:09 PM
	To: Kulshrestha, Manisha; Korchemny, Dmitry; Seligman, Erik
	Cc: Eduard Cerny
	Subject: RE: [sv-ac] call to vote on Mantis 1674

	Hi  Manisha, Dmitry, Erik,

	 

	I tried to "improve" the proposal. Please have a look and let me
know if it is closer to what you'd want.

	 

	Best regards,

	ed

	 

		 

________________________________

		From: Kulshrestha, Manisha
[mailto:Manisha_Kulshrestha@mentor.com] 
		Sent: Sunday, April 22, 2007 10:58 PM
		To: Eduard Cerny
		Subject: RE: [sv-ac] call to vote on Mantis 1674

		 

		Hi Ed,
		
		For 2) There is some statement in the proposal about
being 'lazy' in evaluation. If we go by that then clkx should be same as
clkw. I think there is scope for confusion here and it needs
clarification.
		
		Thanks.
		Manisha
		
		-----Original Message-----
		From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
		Sent: Fri 4/20/2007 5:15 PM
		To: Kulshrestha, Manisha; john.havlicek@freescale.com;
sv-ac@eda-stds.org
		Subject: RE: [sv-ac] call to vote on Mantis 1674
		
		Hi Manisha,
		
		Regarding 1), I added a sentence saying that in that
case it returns
		false.
		
		For 2), I tink that if false is retirned, it should
disable the
		property. Let's see what others say.
		For clkx in a4, the $inferred_clock is the default value
of the formal
		argument clkx, hence as described, it binds to the clock
inferred from
		the context where the property is instantiated (clkx by
the default
		argument value $inferred_clk which at the property
instance position is
		the default clocking clock (negedge clk1)). Only of
$inferred_clock is
		inlined in the property expression, it follows what you
say.
		
		Should it be more explicit? What do you suggest?
		
		Thanks
		ed
		
		
		
		
		> -----Original Message-----
		> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org]
On
		> Behalf Of Kulshrestha, Manisha
		> Sent: Friday, April 20, 2007 4:47 PM
		> To: john.havlicek@freescale.com; sv-ac@eda-stds.org
		> Subject: RE: [sv-ac] call to vote on Mantis 1674
		>
		> Hi,
		>
		> I see two issues with this proposal:
		>
		> 1. There is no mention about what is the inferred
disable condition in
		> case there is no default disable. The proposal says:
The inferred
		> disable expression is the reset expression from the
default disable
		> expression (See 17.14 Note to
		> editor: This is after introducing proposal #1648).".
What happens when
		> there is no default disable ??
		>
		> 2. I see some inconsistency in example a4. It is using
$inferred_clock
		> in two places (clkx is inferred clock and there is
explicit $inferred
		> clock before 'z'). When it replaces inferred clock for
clkx, it says
		> that it is being replaced by default clocking, but for
the
		> $inferred_clock before 'z', it uses clock flow rules.
		>
		> In the proposal it says "The inferred clocking event
expression is the
		> current resolved event expression that can be used in
a clocking
		> event definition. It is obtained by applying clock
flow rules to the
		> point where $inferred_clock is called.
		> If there is no current resolved event expression, then
$inferred_clock
		> returns false (i.e., 1'b0).".
		>
		> Since clkx is being used after clkw, the inferred
clock should be same
		> as clkw ??
		>
		> If clkx was the first clock in the property expression
then it should
		> have been default clock ?
		>
		> Also, what does it mean that $inferred clock returns
false ? Does it
		> mean, it is an error ? Or you simply replace clock
expression by 1'b0
		> (which will make property useless). I think this case
should result in
		> error and proposal should say that clearly.
		>
		> 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, April 18, 2007 4:20 AM
		> To: sv-ac@server.eda-stds.org
		> Subject: [sv-ac] call to vote on Mantis 1674
		>
		> All:
		>
		> This is the call to vote on the proposal for Mantis
1674.
		>
		> As discussed in our meeting, this vote runs longer
than
		> the usual week because we have so many e-mail ballots
		> running concurrently.
		>
		> Please vote if you are eligible.  See the details
below.
		>
		> J.H.
		>
		> Ballot on Mantis 1674
		>
		> - Called on 2007-04-18, final ballots due by 23:59 PDT
on 2007-04-30.
		>
		>  v[xxxxxxxxxxxxxxxxxxx-xx] Doron Bustan (Freescale)
		>  v[xxxxxxxxxxxxxxxxxxxx-x] Eduard Cerny (Synopsys)   
		>  n[---------x-x-xxx-x---x] Surrendra Dudani (Synopsys)
		>  v[x-xxxxx-xxx-xxx-------] Yaniv Fais (Freescale)
		>  t[xxxxxxxxxxxxxxxxxxxxxx] John Havlicek (Freescale -
Chair)
		>  v[xxxxrxxxxxxxxxxxxx-xxx] Dmitry Korchemny (Intel -
Co-Chair)
		>  v[xxxxx----------xx-xxxx] Manisha Kulshrestha (Mentor
Graphics)
		>  n[---xxxxx-------x-xx-x-] Jiang Long (Mentor
Graphics)
		>  n[x.....................] Joseph Lu (Altera)
		>  n[x--x-xx--xx-xxxxxxx-x-] Hillel Miller (Freescale)
		>  v[xxx-xxxxxxxx-xxxxxxxxx] Lisa Piper (Cadence)
		>  v[xx-x..................] Erik Seligman (Intel)
		>  n[-----xxxx-xx----------] Tej Singh (Mentor Graphics)
		>  v[xxxxxxxxxxxxxxxxxxxxxx] Bassam Tabbara (Synopsys)
		>  v[xxxxxxx...............] Tom Thatcher (Sun
Microsystems)
		>    |---------------------- attendance on 2007-04-17
		>  |------------------------ 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)
		>               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.
		>
		>
		>


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Tue May 1 10:13:05 2007

This archive was generated by hypermail 2.1.8 : Tue May 01 2007 - 10:13:19 PDT