Re: [sv-ac] Q: verification statements

Hi John,


On Fri, Oct 19, 2007 at 11:27:03AM -0500, John Havlicek wrote:
> Hi Johan:
> 
> Yes, I agree that the beginning of 16.14 is defective.
> 
> I don't think the severity of the defect is that high, though, when I
> look at Clause 16 as a whole.
> 
> I am hesitant about a small patch to get rid of "concurrent assertion"
> in 16.14.  The phrase "concurrent assertion" appears 62 times in the
> D4 LRM, including the various syntax non-terminals that use it with
> underscores.
> 
> I would like to see some alternative suggestions.

However the phrase "verification statement" appears to occur only 6
times (I think mainly in 16.14, like in 1614.6). Maybe we should replace
those occurrence by "concurrent assertion statement"? for consistency.

/Johan

> 
> J.H.
> 
> > Date: Fri, 19 Oct 2007 16:04:05 +0200
> > From: Johan =?iso-8859-1?Q?M=E5rtensson?= <johan.martensson@jasper-da.com>
> > Cc: erik.seligman@intel.com, sv-ac@eda.org
> > Content-Disposition: inline
> > X-OriginalArrivalTime: 19 Oct 2007 14:04:09.0896 (UTC) FILETIME=[EB960A80:01C81258]
> > 
> > Hi John,
> > 
> > In any case, don't you think that the beginning of the clause 16.14
> > suffers from some terminological confusion as I noted below?
> > 
> > Best Regards,
> > 
> > Johan
> > 
> > | 
> > | Hi,
> > | 
> > | That part (16.14) seems inconsistent w.r.t. to terminology: The heading
> > | reads "Concurrent assertions". The first paragraph talks about
> > | "verification statement", whereas the second paragraph again talks about
> > | "concurrent assertion statement". Are these two terms meant to refer to
> > | the same thing? In that case why not settle for one of them? I
> > | personally prefer "verification statement" since it seems strange to
> > | group assumes and covers under "concurrent assertions".
> > | 
> > | Regards,
> > | 
> > | Johan M
> > | 
> >   
> > On Fri, Oct 19, 2007 at 06:13:35AM -0500, John Havlicek wrote:
> > > Hi Erik:
> > > 
> > > We should be careful about eliminating the use of the phrase
> > > "concurrent assertion".  We have had that phrase for a long time, and
> > > there has been a basic dichotomy between "immediate assertions" and
> > > "concurrent assertions".
> > > 
> > > A problem with the phrase "concurrent assertion" is that when you
> > > compare it with the syntax of the concurrent assertion statements, it
> > > suggests that we only mean "assert property" because of the close
> > > relation of "assertion" to "assert".
> > > 
> > > However, I worry that replacing "concurrent assertion statement" with
> > > "concurrent verification statement" is also not ideal because
> > > "verification statement" read literally is too vague.  A reader may
> > > wonder if this phrase applies to non-assertion statements as well.
> > > 
> > > A better solution may be to find a place in Clause 16 to define terms 
> > > and then use them consistently.
> > > 
> > > J.H.
> > > 
> > > 
> > > >  
> > > > I've reviewed 1995 (concurrent assertions in loops) vs 1737 (fixing some
> > > > language in 16.14.5).  They don't touch the same part of the text, but I
> > > > had a question about some phrasing that I may need to sync up 1995 with.
> > > > 
> > > > 1737 uses the term "verification statements".  I forget, did we agree
> > > > that this is the best general term describing assert, assume, and cover
> > > > statements?  In that case, rather than phrasing 1995 as "concurrent
> > > > assertions" in loops, I should probably modify the phrasing to
> > > > "concurrent verification statements".
> > > > 
> > > > But do we also need to change the title of section 16.14.5?  Right now
> > > > it's "Embedding concurrent assertions in procedural code".
> > > > 
> > > > -- 
> > > > 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.
> > 
> > -- 
> > ------------------------------------------------------------
> > Johan Mårtensson                 Office: +46 31 7451913
> > Jasper Design Automation         Mobile: +46 703749681 
> > Arvid Hedvalls backe 4           Fax: +46 31 7451939
> > 411 33 Gothenburg, Sweden        Skype ID: johanmartensson
> > ------------------------------------------------------------

-- 
------------------------------------------------------------
Johan Mårtensson                 Office: +46 31 7451913
Jasper Design Automation         Mobile: +46 703749681 
Arvid Hedvalls backe 4           Fax: +46 31 7451939
411 33 Gothenburg, Sweden        Skype ID: johanmartensson
------------------------------------------------------------

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