RE: [sv-ac] RE: 2069

And to be picky, "which" should be "that".
 
Shalom


________________________________

	From: owner-sv-ac@server.eda.org
[mailto:owner-sv-ac@server.eda.org] On Behalf Of Bustan, Doron
	Sent: Monday, February 04, 2008 10:12 AM
	To: Korchemny, Dmitry; sv-ac@server.eda.org
	Subject: [sv-ac] RE: 2069
	
	

	Hi Dmitry, 

	 

	I think it is ready. One question:

	 

	It could be my English but when you write:

	"assert property statement is satisfied on a set of traces if it
is satisfied on each trace of the set

	which satisfies all the assumptions associated with the model."
How can one tell whether "which 

	satisfies all the assumptions associated with the model"  refers
to the trace or the set ?

	 

	Same question for the last item.

	 

	Thanks

	 

	Doron

	 

	
________________________________


	From: Korchemny, Dmitry 
	Sent: Sunday, February 03, 2008 4:00 PM
	To: Bustan, Doron; 'sv-ac@eda.org'
	Subject: RE: 2069

	 

	Hi Doron,

	 

	I have also addressed your forth comment. I dropped all mentions
of formal verification and simulation from the proposal.

	 

	Thanks,

	Dmitry 

	 

	
________________________________


	From: Bustan, Doron 
	Sent: Sunday, February 03, 2008 9:03 AM
	To: 'sv-ac@eda.org'; Korchemny, Dmitry
	Subject: 2069

	 

	Hi Dmitry,

	 

	Here are my comments:

	 

	1.	I would use "trace" instead of "path". "path" is very
overload in the LRM, and it could be confusing. 

	At the start of F.3, I would say something like: "This subclause
describes the trace semantics of an assertion: The semantics of an
assertion statement in a single computation (trace) of the design.
Subclause F.4 describes the semantics of an assertion statement on
several traces of the design combined together (global semantics.)

	2.	page 2. "verification statement" -> "assertion
statement". 
	3.	No need to rewrite the property_spec in terms of
property_expr. Disable iff's "disabled" does the work. But then keep
describing the trace semantics using words not rewriting. I think that
using words is better anyway. 
	4.	 F.4 I would just say that "for assert/assume an
assertion  statement holds on a set of traces if and only if it holds in
all of them, and for coverage an assertion statement hold on a set of
traces if it holds in at least one. I would not try to define the
modeling technique. 
	5.	The only comment that I would use for "simulation"
"formal" is something like "in formal all traces of the design are being
considered, however for most designs, shall not expect to verify all
traces. 

	 

	 

	 

	Doron


	-- 
	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.