Tej-- Tell me how this version looks to you. Thanks! ________________________________ From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On Behalf Of Singh, Tej Sent: Monday, January 14, 2008 11:58 AM To: Seligman, Erik; sv-ac@server.eda.org Cc: Warmke, Doug; Vreugdenhil, Gordon; Kulshrestha, Manisha Subject: [sv-ac] RE: New version of 2005 (deferred assertions) posted in Manits Hi Erik, There are still some issues in the 16.4.2 section where the causes of flush point of procedure is listed. An assertoff/assertkill is different from the flush point of procedure. $assertoff can be done on a single deferred assertion which only causes the flushing of that assertion and not of the procedure. So I would modify it as A procedure is defined to have reached a deferred assertion flush point if any of the following occur: ¾ The procedure, having been suspended earlier due to reaching an event control or wait statement, resumes execution. __The procedure was declared by an always_comb or always_latch statement, and its execution is resumed due to a transition on one of its dependent signals. __The outermost scope of the procedure is disabled by a disable statement (see 16.4.4) As for the effect of $assertoff/$assertkill/$asserton and VPI functions on deferred assertion, it should be mentioned in the respective sections that deal with these tasks and not in this section. These changes need to be added to the proposal. Further in 16.4.4 Disabling deferred assertions It is not clear what does "disable is applied to a procedure means". I think you mean disabling the outermost scope of the procedure. It is also not clear what will happen if a sub block scope inside the procedure is disabled. For e.g. always @(a or b or c) begin : b1 a5: assert #0 (a == b) begin : b2 a6 : assert #0 (b == c) end end When 'b1' is disabled it flushes all pending reports of the procedure becaue b1 is the outermost block. But what happens if b2 is disabled. Does it cause flushing of all deferred assertions in that subscope (a6 in this case)? My suggestion is to not allow disabling of subscope to cause flushing of assertions in that scope to keep it simple. This is also consistent with the rule that disabling of task does not cause flushing of assertions in that task. So the only two disables that cause flushing are disabling of outermost scope of the procedure and disabling of single named assertion statement. I will suggest the following text change to make it more clear The disable statement shall interact with deferred assertions as follows: ¾ A specific deferred assertion statement may be disabled. Any pending assertion report of the assertion is cancelled. __ When a disable is applied to the outermost scope of the procedure that has an active deferred assertion queue, in addition to normal disable activities (See 9.6.2), the deferred assertion report queue is flushed and all pending assertion reports on the queue are cleared. Disabling a sub block scope or a task does not cause flushing of any pending reports. Regards Tej ________________________________ From: Seligman, Erik [mailto:erik.seligman@intel.com] Sent: Monday, January 14, 2008 9:43 AM To: sv-ac@server.eda.org Cc: Warmke, Doug; Singh, Tej; Vreugdenhil, Gordon; Kulshrestha, Manisha Subject: New version of 2005 (deferred assertions) posted in Manits I have modified this proposal to remove the controversial event-control feature, and I believe it addresses all the other objections that have been rasied so far. If nobody comes up with any objections, I think the should be ready for us to call another vote after tomorrow's meeting. (Note that we have a separate proposal open, 2209, to potentially re-add the event feature if we have time to define it properly.) Erik Seligman Formal Verification Architect Corporate Design Solutions Design Technology and Solutions Intel Corporation M.S. JF4-402 2111 NE 25th Ave Hillsboro, OR 97124 Phone: (503) 712-3134 -- 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.
This archive was generated by hypermail 2.1.8 : Tue Jan 15 2008 - 11:21:22 PST