RE: [sv-ac] Feedback on Mantis 2005 Proposal

You're right about that example.  If you look in the preamble of the
proposal, you will see an example that actually has a potential glitch,
which is the problem we are trying to solve.  In the next draft I'll fix
the example to be one that actually needs the proposal to work!
 

-----Original Message-----
From: Thomas.Thatcher@Sun.COM [mailto:Thomas.Thatcher@Sun.COM] 
Sent: Monday, September 24, 2007 10:46 PM
To: Seligman, Erik
Cc: Korchemny, Dmitry; sv-ac@eda-stds.org
Subject: Re: [sv-ac] Feedback on Mantis 2005 Proposal

Hello Dmitry, Erik,

I'm thinking through the examples again, and I'm still bewildered.

Take the first example:

	reg [1:0] a = 2'b00;
	always @(posedge clk) begin
	    a = 2'b00;
	    a1: assert property(a == 2'b00);
	    a = 2'b11;
	    a2: assert property(a == 2'b11);
	end

This to me sounds like a perfect place to use immediate assertions.  I
believe immediate assertions would give exactly the desired behavior.
The always block should be executed only once (unless you have glitches
on clk, in which case, nobody really can help).  And immediate
assertions sample the variable at the expected time.  So the following
code should have no
problems:

	reg [1:0] a = 2'b00;
	always @(posedge clk) begin
	    a = 2'b00;
	    assert (a == 2'b00);
	    a = 2'b11;
	    assert (a == 2'b11);
	end

Where glitches might be important would be in an always_comb block. The
example you have is too simplistic, and would still work with immediate
assertions

	reg [1:0] a = 2'b00;
	always_comb begin
	    a = 2'b00;
	    assert (a == 2'b00);
	    a = 2'b11;
	    assert (a == 2'b11);
	end

But a more complicated example might be constructed.

Tom

Seligman, Erik wrote:

>Hi Dmitry-- thanks for replying.  (Sorry, I've been out sick most of 
>this week, and am just catching up on my SV-AC email today.)
>
>Tom--  A few more comments:
>    - I think Dmitry has reasonable answers below for some of your 
>specific points; pls clarify whether you think further explanation is 
>needed, or suggest changes to the language of the proposal.
>    - There is already a SV-BC proposal for the unique/priority stuff, 
>so I'll move that piece to that proposal (2008) and try to find an
owner
>from their end.    
>    - As Dmitry points out, I don't really think this solution really 
>causes more problems than it solves-- it solves the critical issue of 
>glitchy assertions, and only causes a problem in the rare corner case 
>where an assert is placed in between blocking assignments, or in the 
>unusual initial case Dmitry mentions.
>    - Also keep in mind, as mentioned in our note on the Mantis, we 
>have considered an alternative: rather than modify concurrent 
>assertions, define a new type of assertions ("final assertions") that 
>follow the semantics described in this proposal.  In our Intel 
>discussion we thought that would be adding more confusion to the 
>language and not really be necessary, since there are only a few cases 
>(basically the embedded-in-blocking-assigns cases) where we would need 
>the final assertions to be substantially different from concurrent
assertions.
>But if the change to existing semantics is too risky, this is an
option.
>
>Anyway, I'll try to incorporate comments received so far & work on 
>another draft by next week's mtg.  Tom (& others), pls think about this

>& tell us if you still have major objections, if you think we should 
>switch to the "assert final" model & leave concurrent asserts alone, or

>if you think it's just a case where clarification was needed.
>
>
>-----Original Message-----
>From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On

>Behalf Of Korchemny, Dmitry
>Sent: Wednesday, September 19, 2007 9:01 AM
>To: Thomas.Thatcher@sun.com; sv-ac@server.eda-stds.org
>Subject: RE: [sv-ac] Feedback on Mantis 2005 Proposal
>
>Hi Tom,
>
>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 Thomas Thatcher
>Sent: Tuesday, September 18, 2007 5:58 PM
>To: sv-ac@server.eda-stds.org
>Subject: [sv-ac] Feedback on Mantis 2005 Proposal
>
>Have not seen this show up on reflector yet, so I'm re-sending.
>
>Tom
>
>-------- Original Message --------
>Subject: Feedback on Mantis 2005 Proposal
>Date: Mon, 17 Sep 2007 10:43:04 -0700
>From: Thomas Thatcher <thomas.thatcher@sun.com>
>Reply-To: Thomas.Thatcher@Sun.COM
>To: sv-ac@eda-stds.org
>
>Hello Everyone,
>
>I have read through the proposal.  Here are my comments.
>
>First of all, the changes to unique and priority would have to be 
>approved by BC.
>
>[Korchemny, Dmitry] I agree. I would even create a separate proposal 
>for it.
>
>But even so, the proposed change will not be backward compatible, and 
>will create confusion. I read the proposal as "if the unique/priority 
>occurs in a place where concurrent assertions are illegal, then it 
>behaves like an immediate assertion. Otherwise, it behaves as a 
>concurrent assertion."
>This
>creates too much confusion for a small amount of benefit.
>
>[Korchemny, Dmitry] There was a thread in SV-BC addressing this issue.
>As I understood from Matt this feature is very important and requires 
>solution. Matt suggested a new keyword for the new semantics, something

>like "assert priority case ...". This issue belongs to the competence 
>of SV-BC, but the current enhancement can provide infrastructure for 
>its resolution.
>
>Next, I don't see the necessity of the first change in 16.14.5.  The 
>new
>text:
>
>"If the clock is explicity specified with a property, it can be 
>different from the inferred clock as shown below:"
>
>To me this seems like giving users rope to hang themselves with.
>
>[Korchemny, Dmitry] I would agree with you if we had talked about 
>manually written assertions. The situation is different when we are 
>talking about assertions belonging to a checker library. Consider the 
>following example:
>
>always @(posedge clk) begin
>	a <= ...;
>	assert property(a_is_stable_between_two_posedge_clk>);
>	...
>end
>
>Though it looks like that this assertion is controlled by posedge clk, 
>but it is actually controlled by some faster clock. When the user puts 
>this assertion inside the always procedure, she has no idea, why this 
>code does not compile, and the compilation error message will hardly be

>of any help for her.
>
>The proposed enhancement certainly does not harm for manually written 
>assertions since if somebody writes it this way, he does it on purpose.
>
>Next, On the case statement example
>
>	reg [1:0] a = 2'b00;
>	always @(posedge clk) begin
>	    a = 2'b00;
>	    a1: assert property(a == 2'b00);
>	    a = 2'b11;
>	    a2: assert property(a == 2'b11);
>	end
>
>I don't see how this is going to work.  Concurrent assertions always 
>use the sampled value of the signal.  Thus one or both of the two 
>assertions above should fail, regardless of the enabling conditions, 
>because they are going to get the previous value of a, before the 
>assignment takes place.  Even after the shadow variable explanation, 
>the code still doesn't work.
>
>	reg [1:0] a = 2'b00;
>	bit shadow_a1;
>	bit shadow_a2;
>	always @(posedge clk) begin
>	    a = 2'b00;
>	    shadow_a1 = ((a == 2'b00) != 'b0);
>	    a = 2'b11;
>	    shadow_a2 = ((a == 2'b11) != 'b0);
>	end
>	    a1: assert property(@(posedge clk) shadow_a1);
>	    a2: assert property(@(posedge clk) shadow_a2);
>
>The assert properties get the values of shadow_a1 and shadow_a2 from 
>the preponed region, before they are ever assigned.
>
>[Korchemny, Dmitry] There is a problem here at the initial step only, 
>when the second assertion fails. At all other iterations the behavior 
>will be correct. This is a common problem with concurrent assertions - 
>they sample the value before it is ready yet. For most practical cases 
>it does not really matter, because these assertions will normally use 
>disable iff.
>
>If you are proposing a change to the scheduling semantics for 
>concurrent assertions, then I am completely opposed.
>
>[Korchemny, Dmitry] This proposal does not change the scheduling 
>semantics of concurrent assertions. It changes their behavior when they

>are put between two blocking assignments to the same variable, but 
>people usually don't do that. The alternative would be to introduce one

>more type of assertions - final assertions, which would act as 
>described in the proposal. So, the dilemma is whether to change the 
>behavior of concurrent assertions in some cases, or to have three types

>of assertions instead of two. I don't know which solution is better.
>
>We want to avoid at all costs having things work one way in one context

>and a different way in a different context.
>
>[Korchemny, Dmitry] But this is exactly what immediate assertions do 
>now.
>
>I think that this mantis item should be indefinitely postponed, until 
>we can come up with a proposal that doesn't cause worse problems than 
>it solves.
>
>[Korchemny, Dmitry] This subject is extremely important, since 
>currently boolean assertions in SVA have only limited applicability: 
>immediate assertions exhibit a glitch behavior, while concurrent 
>assertions cannot be used to follow the sequential execution, since 
>they use sampled values only. Also, immediate assertions do not have a 
>well defined formal semantics.
>
>Therefore, currently the most basic assertions - the plain boolean 
>assertions are the most problematic in SVA. I don't think that there is

>a more urgent issue in SVA than this one for the whole industry. Of 
>course, I am not advocating adopting any hasty or unelaborated 
>solutions, but I strongly disagree with the statement that this item 
>should be indefinitely postponed.
>
>Any alternative solutions or suggestions are welcome.
>
>Tom
>--
>------------------
>Thomas J. Thatcher
>Sun Microsystems
>408-616-5589
>------------------
>
>
>  
>

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