Subject: Re: questions about CBV
From: John Havlicek (havlicek@adttx.sps.mot.com)
Date: Mon Apr 15 2002 - 13:11:59 PDT
Hi Adam:
> Hi John;
>
> Thanks for the explanation of weak vs. strong clocking.
> I guess I've used weak clocking without knowing it...
>
> You write:
> >Yes. In the statement layer of CBV, the local variables capture
> >sampled values that are local to the thread and its descendents. The
>
> That's good, but...
>
> >I think it is accurate to say that the CBV analogue of your assertion
> >would result in both processes terminating with the first "done". In
>
> That's bad IMHO.
From the perspective of CBV, the user has created two threads, both
of which are looking for the same thing. Since protocol correspondences
rapidly become too complicated to predict with pre-defined constructs
when there are varying priorities, retries, bypasses, etc., CBV leaves
it to the user to code the correspondences. The basic constructs of
CBV are simple and do not have the correspondence tracking built in.
You seem to be asking for more powerful constructs to relieve the user
of some of the coding and that may make the user's code more
localized. These sorts of goals can be achieved in CBV in a reusable
way using cbvmodules, but they are not pre-defined.
>
> >CBV, the user needs to provide the code that will ensure the correct
> >correspondences in cases like these. Often, one needs some auxiliary
> >FSM. For example, ...
>
> This is a simple protocol example, that a temporal regular expression
> should be capable of handling.
It will be helpful if you can say more about things like the bound on
the number of outstanding "req"s without corresponding "done" signals.
If there is no such bound, it is not obvious to me how to handle the
protocol with a regular expression. If there is such a bound, it
would be nice to know if the user can specify it, and, if so, how you
envision fitting it into the syntax.
> When threads sync to the same
> set of events, then what good is having threaded assertions? It
> would seem that they are self fulfilling - the first one passes,
> the second one follows it...
The threaded assertions are not required all to sync to the same
set of events. However, if the user codes them to do so, then they
will. Code can be added to cause the threads to sync to different
sets of events, but that code is not implicit.
>
> >Much more complicated protocol correspondences are routinely coded
> >in CBV.
>
> I expect that they are. And for complex protocols, one expects to
> provide more coding. For basic pipelines, one should not have to
> create FSM's, delays, etc. for checking them. Erich talked about
> this relating to first match vs. all match. I don't understand
> what exactly what this implies. But I do understand what a user
> would have a hard time coding to check the above example if threads
> match on the same event (which I would guess is all-match.)
I can comment on "all-match" vs. "first-match" in CBV.
In CBV, the treatment of a regular expression as "all-match" or
otherwise depends on its context.
For example, consider assertion at time i of
r ;
where r is a regular expression. This assertion passes provided
there exists j>=i such that r is matched from i to j. This assertion
can thus be discharged at the earliest such j>=i, and therefore can
be considered a kind of "first-match".
The assertion "r;" is equivalent to
observe (r) 1;
which is a special case of the statement form
observe (r) S
where S is a statement. Assertion of "observe (r) S" at time i passes
iff there exists j>=i such that r is matched from i to j and also
assertion of S at time j passes. Since assertion of S might fail at
the first j>=i at which r is matched, but might pass for some later j
at which r is matched, this statement form is not a "first-match".
Rather, it is a kind of "exists-match".
The dual is
if (r) S
Assertion of "if (r) S" at time i passes iff for each j >= i such that
r is matched from time i to j, assertion of S at time j passes. In
other words, "if (r) T" is "all-match" on r, although r is in the
position of a precondition.
CBV provides the "first_match" operator on regular expressions.
"first_match r" is matched from i to j iff r is matched from i to j
and r is not matched from i to k for any k that is <j and >=i.
Best regards,
John Havlicek
>
>
> Thanks John, for the helpful comments about CBV.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Apr 15 2002 - 13:14:44 PDT