Subject: Re: [sv-ac] local variables
From: John Havlicek (john.havlicek@motorola.com)
Date: Wed Mar 05 2003 - 15:43:44 PST
Hi Adam:
Thanks for your quick and careful reading!
My attempts to answer your questions are below.
Best regards,
John H.
> Hi John;
>
> Your proposal says:
>
> >7) The sequence must end at the point where the value is accessed. Otherwise, the
> > comparison of such a variable will result in false. For example, in s10, if
> > sequence s9 doesn't end where s9.x is used, then (s9.x == data2) will be false,
> > regardless of the value of data2.
>
> Isn't this a little implicit to require s9 to end at the time of use?
It is a _lot_ implicit! I am not really worrying about the specific syntax,
since we don't get to decide it in SV-AC. Semantically, the point is that
when getting local variables out of a sequence, you can only do it at a point
where the sequence ends.
In a previous incarnation, the proposal required "ended" to be used explicitly,
so that one would have written something like
sequence s9 = (a ; (int x = data, int y = data1) b; c);
sequence s10 = (d ; e; ended(s9) && (s9.x == data2));
>
> Can I do something like this? This is much more explicit...
>
> sequence s9(cmpdata) = (a; (int x = data, int y = data1) b; c; [0] cmpdata == x);
> sequence s10 = (d; e; ended s9(data2));
This looks o.k. to me. However, you might have had
sequence s10_alternate = (d ; e; (int z = s9.data) 1; f; (z == data2));
in which case you might not want to push the stuff following the "handoff"
into s9. [The point of this feature is to allow you to get local variables
out of named sequences. You can always "flatten" the definitions to avoid
using it, but that may be inconvenient.]
>
>
> On the example from #8, is this describing useful (desired) functionality,
> or is it describing what happens (whether or not that is useful.)
>
>
> > Then p12 becomes:
>
> > property p12_v1 = (d ; e; (v1 == data2));
> > property p12_v2 = (d ; e; (v2 == data2));
>
> > Both properties p12_v1 and p12_v2 must hold.
>
> If v1 != v2 then you get a failure! This concept of multiple matches at the same time
> step (due to nondeterminism) is not intuitive.
Yeah, I'm not sure I like the "forall" semantics. As I said in the "JH:" notes,
JH: This proposed semantics should be scrutinized. My intuition
JH: is that for the purpose of defining tight satisfaction,
JH: such multiple match situations should be existentially
JH: quantified.
In other words, my intuition is that "both properties p12_v1 and p12_v2 must hold"
should be "at least one of p12_v1 and p12_v2 must hold".
>
>
> Concerning templates and dynamic variables - what type is recommended for dynamic variables?
>
> With templates one can pass in signals of different sizes. If an 'int' is only 32 bits,
> then I guess a template won't work with data larger than 32 bits.
I don't see why the dynamic variables cannot be of any bitvector type.
I have been writing "int" because all the examples use "int" and I haven't
bothered to figure out what other type specifiers are legal!
>
> Thanks John.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
>
This archive was generated by hypermail 2b28 : Wed Mar 05 2003 - 15:45:00 PST