[sv-ac] RE: 2069

Hi Doron,

 

Please, see my comments below. I deposited the updated version into
Mantis, and also attaching it here.

 

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.

[Korchemny, Dmitry] Fixed.

 

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

[Korchemny, Dmitry] At the beginning of F.3 I added the following:

 

"This subclause describes 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). Since simulation tools deal
with a

single valuation trace, their behavior is described by the trace
semantics.

Formal verification tools deal with sets of all feasible traces,
therefore the

global semantics is needed to describe their behavior."

 

At the beginning of F.4 I put:

 

This subclause describes the semantics of an assertion statement on
several

traces of the design combined together (global semantics). The global
semantics

is used to describe behavior of formal verification tools as they deal
with

sets of all feasible valuation traces.

 

2.	page 2. "verification statement" -> "assertion statement".

[Korchemny, Dmitry] Fixed.

 

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.

[Korchemny, Dmitry] Done.

 

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.

[Korchemny, Dmitry] But you need somehow to define the semantics of
assumptions and to explain how they limit the set of feasible traces.

 

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. 

 

[Korchemny, Dmitry] If a formal tool cannot verify the whole set of all
feasible traces then it does not do formal verification, but some kind
of underapproximation. I would rather not discuss it in Annex F.

 

 

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.