Hi Doug-- Here's my main concern. The user thought process is likely to be "I want to have an assertion to check the values of a and b in the combo logic, but all the logic of this fsm is not valid until the positive clock edge. So to be safe, I'll put this assert on the posedge of clock." For the moment we'll assume that there is a reason a concurrent assert can't be used in this case; perhaps a42 is really within a function, but for simplicity let's look at your example: module fsm(input clk, rst, a, b); ... always_comb begin : b1 a42: assert @(posedge clk) (a == b); ... end always_ff (@posedge clk) begin : b2 state <= nextstate; if (somecond) begin b <= !b; ... end ... end endmodule This seems to us like the most common case that a designer would generate, so it's important that our deferred asserts with event control behave as a designer would expect in this case, and report any violations of a42. Honestly, if we can't define the deferred event control option in such a way that the example above will report failures on a42, I think it may be better to leave it off the proposal altogether. But I would like to have this feature, which might be quite useful. Here is a summary of my original suggestion for the filtering method (as modified in a later email, not sure if you noticed): 1. When a42 is fails in procedural code, it is put on the deferred assertion report queue. 2. If block b1 is executed again, we have a flush point as previously described. 3. During the Observed/Postponed region, for each assertion in the deferred queue with an event control: 3a. If that event occurred during the current time step, we report the assertion. 3b. If that event did not occur during the current time step, the assertion remains on the queue. Thus it may get reported during a future time step when that event occurs, if the procedure (b1) has not been re-activated to create another flush point. (Intuitively, this represents the fact that since there was no change to block b1, the "bad" values are still in effect at the future time step.) I believe point 3b here resolves your concern about never reporting failures if signals change after a delay with respect to the clock edge. I also don't see how there could be a race condition issue with this method: we are checking the final execution of each of the asserts within any given time step, and if the correct clock did not transition, we delay until a future time step to give the new clock values a chance to take effect. If you think there is still a race danger, can you put together a small explicit example? We also have the other question about whether to use the Observed or Postponed region. Dmitry-- can you comment in more detail why we wanted Postponed rather than Observed? I'm not sure I fully recall our reasoning. Thanks! ________________________________ From: Warmke, Doug [mailto:doug_warmke@mentor.com] Sent: Wednesday, November 07, 2007 5:27 PM To: Seligman, Erik Subject: RE: RE: [sv-bc] New Proposal uploaded for Mantis 2005 Erik, Can you please elaborate on what you think one would intuitively expect in that final example? Did you understand my motivation of using an event control to filter finite-time glitches? The finite-time glitch problem is what I'm after. What you and Dmitry seemed to understand from the use of event control is something very different: You thought it meant to "sample and report in the time units corresponding to the specified edge", rather than immediately sample, but "report at the specified edge". I don't know if I could say one is more "intuitive" than the other. There are problems with your guys' interpretation. Here is what I have written in the Motivation section of rev 2 of 2005: One final point to mention in this Motivation section is about Dmitry/Erik's interpretation of my suggestion on the use of event controls in deferred assertion syntax. Dmitry and Erik had interpreted that to mean "Only evaluate the deferred assertion's expression during cycles in which the event control occurs". However, that was not the intention. While an interesting idea, there are problems there. Unlike concurrent assertions, deferred assertions don't have access to Preponed region values. This feature would then effectively be like #0 sampling of concurrent assertion values (i.e. the values at the end of the Active region), a feature which was discussed earlier and abandoned. For clocked assertion evaluation, we should just use concurrent assertions. Also, it is possible that an always_comb is sensitive to signals that change a finite-time delay after the clock edge (e.g., an RTL block fed by a gate-level block) In that case, the Dmitry/Erik system would never actually evaluate the deferred assertions, since the always_comb would never run in the same time step as the clock edge. Also, in the Dmitry/Erik interpretation, imagine users write their always_ff processes with plain blocking assigns rather than NBA's. You can then get into clock/data races as downstream processes execute at the clock edge. Upstream processes would have seen old data, downstream processes will see new data. Deferred assertions would have trouble them. To handle such races, whenever deferred assertions are encountered in procedural code, execute them assuming the clock will come. But if by Observed the clock doesn't come, schedule an implicit flush point and then abandon the pending violation reports. This is complex and will be bad for performance. Thanks Erik - looking forward to hearing more from you on this topic. (I hope I even have your interpretation right! J) Regards, Doug From: Seligman, Erik [mailto:erik.seligman@intel.com] Sent: Wednesday, November 07, 2007 1:38 PM To: Warmke, Doug Subject: RE: RE: [sv-bc] New Proposal uploaded for Mantis 2005 Thanks-- I agree, we're pretty close! The main sticking point now is the semantics of the event control. The final example in the current revision you posted is precisely what I see as the 'typical' usage case- so it it doesn't work as one would intuitively expect, that's a bit of a problem. Thus I wanted to see your response to my suggestion of going back to the filtering method that was in the previous draft, or if you had other ideas for proposing this in such a way that that example would work as the designer expects. ________________________________ From: Warmke, Doug [mailto:doug_warmke@mentor.com] Sent: Wednesday, November 07, 2007 1:24 PM To: Seligman, Erik Subject: RE: RE: [sv-bc] New Proposal uploaded for Mantis 2005 Erik, Sorry for my delay. I've been overhammered. I'll get this done by the end of the week. Actually I think the proposal is very close to an acceptable state as it is. What more items were you planning on adding to it? Regards, Doug From: Seligman, Erik [mailto:erik.seligman@intel.com] Sent: Wednesday, November 07, 2007 9:29 AM To: Warmke, Doug Subject: RE: [sv-bc] New Proposal uploaded for Mantis 2005 Hi Doug-- Haven't heard from you in a few days. Are you still working on this proposal & planning to reply to the email, or should I just take the _1 version and continue the editing...? ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Seligman, Erik Sent: Friday, November 02, 2007 8:26 AM To: Warmke, Doug; Adam Krolnik Cc: sv-ac@server.eda.org Subject: RE: [sv-ac] RE: [sv-bc] New Proposal uploaded for Mantis 2005 Hi Doug-- Thanks for posting that proposal. I think you're right, the 'disable' looks like a cleaner way to allow some manual flushing if desired. Am I correct that you are still revising this, since I don't see the _2 version posted in Mantis yet? In that case, rather than attempting to edit again right now, I'll send you my current questions & comments: 1. As the reasoning for using the Observed rather than the Postponed region, we state "While the Postponed region is also a candidate for the execution of deferred assertion reports, it is risky to allow execution of action block code in the Postponed region. Currently SystemVerilog has no such requirement. " But is it really 'risky', given the restrictions later described on the action block? I see one strong argument for the Postponed region: in that region, it is illegal to reschedule any previous regions, so we know it will only be executed once per time step. If we use the Observed region, it could get executed multiple times-- which might mean we will get glitches anyway, defeating the main purpose of this proposal. Am I interpreting the simulation rules incorrectly? Or is there a reason we shouldn't be worried about a glitch due to region iterations within a time step? 2. Isn't there a way we can redefine the behavior with event controls so your last example behaves more intuitively, and a42 does get executed? module fsm(input clk, rst, a, b); ... always_comb begin : b1 a42: assert @(posedge clk) (a == b); ... end always_ff (@posedge clk) begin : b2 state <= nextstate; if (somecond) begin b <= !b; ... end ... end endmodule When a42 is encountered, its report is scheduled for the next occurrence of (posedge clk). You point out that b1 may be running again in an active region before that, causing a flush point. Is there really no way a simulator can use the fact that (posedge clk) occurred during the current time step, in order to schedule a42 to be reported during the upcoming Observed/Postponed region? I guess this hints back at what was in the original proposal... I didn't fully understand why a filtering method can't work. What's bothering me is that this seems like a very typical usage, where a designer wants an immediate assertion in b1 but doesn't want to see glitches on an in-between clock, and this example seems to show that the deferred asserts with event controls can't be used for this pupose, making them a lot less useful. 3. Have you thought more about this suggested extension that Dmitry emailed? Or do you still prefer to defer it for now? I would extend it to allow the forms like "assert #0 (@clk expr);". The reason of doing that is to be able to use (degenerate) sequences to specify the assertion body. This will allow building assertion libraries for boolean assertions. E.g., sequence same(a, b, rst, clk) @clk rst || a == b; endsequence : same assert #0 (same(x, y, 0, posedge clk)); If only syntax "assert @clk (expr);" is permitted, it will be difficult to build libraries of these assertions. 4. I think we should probably add an example to the proposal in which one function is called from two processes, showing how a deferred assertion in the function is executed/flushed independently for each. -- This message has been scanned for viruses and dangerous content by MailScanner <http://www.mailscanner.info/> , 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 Fri Nov 9 10:38:24 2007
This archive was generated by hypermail 2.1.8 : Fri Nov 09 2007 - 10:38:54 PST