RE: [sv-ac] RE: New version of 2005

From: Seligman, Erik <erik.seligman_at_.....>
Date: Tue Jan 15 2008 - 11:16:48 PST
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.



Received on Tue Jan 15 11:20:45 2008

This archive was generated by hypermail 2.1.8 : Tue Jan 15 2008 - 11:21:22 PST