[sv-ac] RE: 2069

From: Korchemny, Dmitry <dmitry.korchemny_at_.....>
Date: Sun Feb 03 2008 - 06:00:19 PST
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

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.




Received on Sun Feb 3 06:02:59 2008

This archive was generated by hypermail 2.1.8 : Sun Feb 03 2008 - 06:03:09 PST