[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, and is
believed to be clean.