[sv-champions] Re: [sv-sc] some comments on 1900, part 2

Hi Mike:

I agree with the changes you made. 

Regarding the following,

> > Part 2, p. 13.  It is stated that the assume set of F1 excludes
> >    F1.B1.u2 because the only formal argument of the child checker
> >    bar is bound to actual r that is an inactive free variable.
> > 
> >    Is it true that F1.B1.u2 is in the assume set of F1.B1?  I think
> >    that the rules say that it is.
> 
> Yes, it is. I didn't add anything to the doc about that - would you prefer that that be pointed out?

I think that adding a statement to this effect will help the reader to
understand what is going on.  F1.B1.u2 involves a free checker
variable ("n", I seem to recall) that does need to be randomized, so
just saying that F1.B1.u2 is not in the assume set of F1 leaves room
for doubt about whether this variable is ever randomized.

J.H.

> Date: Thu, 07 Aug 2008 16:30:54 -0700
> From: Michael Burns <michael.burns@freescale.com>
> CC: sv-champions@eda.org, sv-sc@eda.org
> X-OriginalArrivalTime: 07 Aug 2008 23:31:07.0146 (UTC) FILETIME=[AA7B36A0:01C8F8E5]
> 
> This is a multi-part message in MIME format.
> --------------030005070608030505010907
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
> Content-Transfer-Encoding: 7bit
> 
> 
> Hi John and all,
> 
> I've uploaded corrections for these to Mantis (changing the state to "feedback) and attached a PDF. My replies are below.
> 
> --Mike
> 
> John Havlicek wrote:
> > Part 2, p. 6.  In the example, is v1 static?  If so, then I think
> >    that the declaration assignment is performed only once, so the 
> >    behavior of check_loop is not described correctly.  This could
> >    be fixed by making v1 automatic or by changing
> > 
> >       logic [7:0] v1=0;
> > 
> >    to
> > 
> >       logic [7:0] v1;
> >       v1 = 0;
> 
> Yes - I've changed v1 to automatic.
> 
> > Part 2, p. 13.  It is stated that the assume set of F1 excludes
> >    F1.B1.u2 because the only formal argument of the child checker
> >    bar is bound to actual r that is an inactive free variable.
> > 
> >    Is it true that F1.B1.u2 is in the assume set of F1.B1?  I think
> >    that the rules say that it is.
> 
> Yes, it is. I didn't add anything to the doc about that - would you prefer that that be pointed out?
> 
> > Part 2, p. 14.  Miscounting.
> > 
> >       x |=> ##5 1'b0
> > 
> >    fails 6 cycles after x == 1.
> 
> Yes; fixed.
> 
> > Part 2, p. 14.  The exception to Preponed sampling for constants and
> >    automatics is too tight.  Local variables are excluded, as are the
> >    active free checker variables.
> 
> I just struck that whole sentence. It's just a restatement of stuff that's already defined elsewhere. Besides, it got awkward to try to fix it to be exactly right.
> 
> 
> --Mike
> 
> 

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