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.