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

The following example from Mantis 2008 was tested on three different
simulators and found to cause violations of the 'unique case assertion':

module bar();

bit clk, m, o, ff1, i_ff1 ;

always_comb begin
 unique case({m,ff1})
   2'b00: o = 1'b0;
   2'b11: o = 1'b1;
  endcase
  $display("%t m:%b ff1:%b",$time,m,ff1); 
end

always_comb m = ff1 && 1 ;

always_ff @(posedge clk) ff1 <= i_ff1;

initial forever 
  begin 
    #1; 
    clk = ~clk; 
  end

initial 
begin 
  @(clk) i_ff1 <=1; 
  #1000; 
  $finish; 
end

endmodule


Shalom


> -----Original Message-----
> From: owner-sv-ac@server.eda.org 
> [mailto:owner-sv-ac@server.eda.org] On Behalf Of Thomas Thatcher
> Sent: Tuesday, September 25, 2007 7:46 AM
> To: Seligman, Erik
> Cc: Korchemny, Dmitry; sv-ac@server.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.
> 
---------------------------------------------------------------------
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.