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 ------------------ -- ------------------ 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.Received on Wed Sep 19 09:01:17 2007
This archive was generated by hypermail 2.1.8 : Wed Sep 19 2007 - 09:01:42 PDT