Re: [sv-ac] RE: 2069

Hi Folks:

To answer Doron's question, the relative clause usually
binds to the immediately preceding nominative rather than
an earlier.

I agree with Shalom on using "that" instead of "which".
"That" introduces an essential (i.e., restrictive) clause,
while "which" usually introduces a non-essential clause.

People argue about this, but for the LRM I recommend using
"that" for essential clauses.

J.H.

> X-Authentication-Warning: server.eda.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.25,301,1199692800"; 
>    d="scan'208,217";a="256487150"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 4 Feb 2008 11:57:41 +0200
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] RE: 2069
> thread-index: AchmMsCjPEg5/uLJSNWxFzlUDLRSfgAOdhNQACYhITAAA8scUA==
> From: "Bresticker, Shalom" <shalom.bresticker@intel.com>
> X-OriginalArrivalTime: 04 Feb 2008 09:58:21.0416 (UTC) FILETIME=[796B9680:01C86714]
> X-eda.org-MailScanner: Found to be clean, Found to be clean
> X-eda.org-MailScanner-SpamScore: s
> X-Spam-Status: No, No
> Sender: owner-sv-ac@eda.org
> X-eda.org-MailScanner-Information: Please contact the ISP for more information
> X-eda.org-MailScanner-From: owner-sv-ac@server.eda.org
> 
> This is a multi-part message in MIME format.
> 
> ------_=_NextPart_001_01C86714.792AECCA
> Content-Type: text/plain;
> 	charset="us-ascii"
> Content-Transfer-Encoding: quoted-printable
> 
> And to be picky, "which" should be "that".
> =20
> 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
> =09
> =09
> 
> 	Hi Dmitry,=20
> 
> =09=20
> 
> 	I think it is ready. One question:
> 
> =09=20
> 
> 	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=20
> 
> 	satisfies all the assumptions associated with the model"  refers
> to the trace or the set ?
> 
> =09=20
> 
> 	Same question for the last item.
> 
> =09=20
> 
> 	Thanks
> 
> =09=20
> 
> 	Doron
> 
> =09=20
> 
> =09
> ________________________________
> 
> 
> 	From: Korchemny, Dmitry=20
> 	Sent: Sunday, February 03, 2008 4:00 PM
> 	To: Bustan, Doron; 'sv-ac@eda.org'
> 	Subject: RE: 2069
> 
> =09=20
> 
> 	Hi Doron,
> 
> =09=20
> 
> 	I have also addressed your forth comment. I dropped all mentions
> of formal verification and simulation from the proposal.
> 
> =09=20
> 
> 	Thanks,
> 
> 	Dmitry=20
> 
> =09=20
> 
> =09
> ________________________________
> 
> 
> 	From: Bustan, Doron=20
> 	Sent: Sunday, February 03, 2008 9:03 AM
> 	To: 'sv-ac@eda.org'; Korchemny, Dmitry
> 	Subject: 2069
> 
> =09=20
> 
> 	Hi Dmitry,
> 
> =09=20
> 
> 	Here are my comments:
> 
> =09=20
> 
> 	1.	I would use "trace" instead of "path". "path" is very
> overload in the LRM, and it could be confusing.=20
> 
> 	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".=20
> 	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.=20
> 	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.=20
> 	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.=20
> 
> =09=20
> 
> =09=20
> 
> =09=20
> 
> 	Doron
> 
> 
> 	--=20
> 	This message has been scanned for viruses and=20
> 	dangerous content by MailScanner <http://www.mailscanner.info/>
> , and is=20
> 	believed to be clean.=20
> 
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.
> 
> 

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