Subject: questions about CBV
From: John Havlicek (havlicek@adttx.sps.mot.com)
Date: Fri Apr 12 2002 - 11:23:12 PDT
Hi Adam:
Thanks for your mail. My responses are interspersed below.
Best regards,
John Havlicek
========================================
> Hi John;
>
>
> Thanks for spending the morning doing this...
>
> You wrote:
>
> [Previous mail]
>
> : "a_posedge(clk)"
> : "(a_posedge(clk) & ~idle)"
>
> I didn't understand these example - the a_posedge() component.
CBV provides both "before" and "after" forms of the edge-detection
functions. "a_posedge" is "after posedge", while "b_posedge" is
"before posedge". There are also before and after forms of "negedge"
and "anyedge". The unmodified forms "posedge", "negedge", and
"anyedge" can be used, but their meaning (as "after" or "before") must
be declared by the user or otherwise understood by the tools
implementing the language.
CBV does not allow expressions that look more than one tick
ahead, so compositions like
b_posedge(b_posedge(clk))
are illegal.
>
> :> 3. Immediate implication (antecedent and consequent
> :>overlap by one cycle):
> :>
> :> {a; b; c} |-> {d; e; f} -- Sugar
>
> :In CBV, this weak suffix implication can be rendered as
> :
> : if (a; b; c)
> : not fail [d; e; f] ;
> : until "expect" is understood to mean "not fail".
>
> Uh, oh, 'not fail' Now I'm stuck - I couldn't understand this
> when verisity explained it, now I have to try again.
> Ok - double negatives.
The CBV shown is equivalent to the Sugar shown when interpreted
linearly (i.e., over traces) and using the weak clocking semantics
of Sugar--if you understand the one then you actually understand
the other. :-)
You should refer to the Sugar documents for the precise Sugar
semantics.
In CBV, "fail" is not the same as Verisity's "fail". [The CBV
"first_fail" corresponds more closely, if not identically, to
Verisity's "fail".] Suppose r is a CBV regular expression.
A word y = y_iy_{i+1}...y_j is in the language of "fail r" iff
1. no prefix of y is in the language of r, and
2. no word in the language of r is a prefix of y.
[In terms of finite automata, "fail r" can be thought of as follows.
Take a finite automaton recognizing the language of r. Determinize it
and make it complete. Introduce a new state "fail" that is trapping.
Reduce this automaton by collapsing any state that has no path to an
accepting state into the "fail" state. Reduce the automaton further
by identifying all the accepting states into a single "succeed" state
that is trapping and by deleting all other transitions out of the
"succeed" state. Now you have an automaton for "fail r", where the
"fail" state is the unique accepting state.]
>
> For myself (maybe others too) what is weak implication? vs. strong?
> I.e. why both
>
> if (a; b; c) not fail [d; e; f] ; // weak
> if (a; b; c) [d; e; f] ; // strong
One difference is that a weak implication will not be false just
because time ran out in a finite trace. A weak implication may be
true at the end of a finite trace, even though the consequent has not
been observed by that point. A strong implication will be false at
the end of a finite trace if the required consequent has not been
observed by that point.
The subtleties involve the question of how one knows to give up
looking for the consequent. Put another way, if the consequent
of a weak implication is not observed, under what conditions
is the weak implication true and under what conditions is the
weak implication false? If one does not understand this, then
I don't think one really understands the meaning of the weak
implication.
I am not very knowledgeable about the history of these particular
forms. I first saw them in the Sugar weak SERE implications. My
purpose has been to illustrate how to represent the Sugar weak
implications in CBV, not to advocate the use of any particular form.
CBV affords great flexibility to users to code precisely the forms
they need.
>
> :The juxtaposition of "not" and "fail" in the CBV renderings
> :of the weak implications has been criticized as "convoluted".
>
> This reasoning has my vote as seen above...
I respect this opinion. One should not ignore the fact that
in the simplest case of weak clocking according to the finest
granularity, the definition of weak suffix implications in
Sugar involve three quantifiers in alternation. My opinion is that
there is some subtlety in the weak implications, and Sugar does
a better job of hiding it than CBV.
>
> You write about overlapping antecedent/consequent vs. next cycle
> overlaps. I don't quite understand why both are required and would
> prefer to explain that overlapping is available and subsequent
> can be done by delaying the consequent by 1 cycle. E.g.
>
> if (a; b; c) not fail [d; e; f] ; // c & d coincident.
> if (a; b; c) not fail [1; d; e; f]; // c & 1 coincident.
CBV allows you to code either of these according to your needs
and preferences. Assertion of
[1; d; e; f];
is generally equivalent to assertion of
#(1) : [d; e; f];
where "#(1)" is the strong nexttime in CBV.
By the way, mea culpa: I said that
{a; b; c} |=> {d; e; f}!
in Sugar can be rendered in CBV as
if (a; b; c)
+(1) : [d; e; f];
when in fact the "+(1)" here (weak nexttime) should be "#(1)" (strong
nexttime):
if (a; b; c)
#(1) : [d; e; f];
>
> As to implication vs if() in syntax, I don't know if there's
> a real difference, but I like to explain to people that the
> assertions are simple, single statements. Having if() makes me
> think about where the else is. The syntax is a little heavier
> than just delaying the sequence by N cycles.
O.k. But there should be some syntax for relating antecedents
with consequents. CBV uses "if". Not all forms of "if" in
CBV admit "else". Generally, forms for which there is confusion or
ambiguity about when the "else" should be taken do not allow it.
These include the "if (<regexp>) <statement>" form.
>
> :CBV does provide mechanisms for accessing past values of a
> :signal.
> :
> :The first is the "past" operator:
>
> : past(c, n, e)
>
> Ah, thank you - One of the most useful elements, if not the most
> useful element IMHO. I have written 3 commonly used elements with
> this primitive for use with my assertions, posedge(e), negedge(e)
> and stable(e) all using past(1, e) in them.
>
> : The second is local variables. Local variables in CBV hold
> :sampled values of expressions. The value loaded into a CBV local
> :variable cannot be subsequently changed, so CBV local variables can
> :effectively provide access to the value of a signal an arbitrary
> :number of cycles in the past. The user must manage the conditions
> :under which sampling occurs.
>
> I am curious about your statement 'variable cannot be subsequently
> changed.' I have assertions that overlap execution, e.g. pipelined
> protocols, pipelined structures, etc. Do you mean that variables
> can only be set once for a given 'thread' of execution?
Yes. In the statement layer of CBV, the local variables capture
sampled values that are local to the thread and its descendents. The
local variable value cannot be changed except through overwriting in
case a subsequent local variable of the same name is sampled. [There
is no assignment statement in the statement layer of CBV.] Multiple
threads may execute the same local variable definition at different
times and therefore capture different sampled values.
> Or a variable
> can only be written once until the assertion completes execution?
I don't think I understand the distinction here. Each thread
that executes a local variable definition gets a sampled
value for the local variable. A single assertion could spawn
multiple threads that execute various local variable definitions
at various times.
>
> This is useful - basically a register that one can use to hold
> state for later comparison... But unless pipelining is satisfied
> they restrict usage, particularly for these most interesting cases.
>
> Lastly, what's your thought about assertions that are running
> concurrently, should each instance find the same event in the same
> time?
> -------------------------------------
> Consider the case of this assertion:
>
> if (req) assert ([1:10]; done);
>
> This allows 'done' to be asserted 1 to 10 clocks after 'req'.
> Now consider two 'req's in consecutive cycles. Is this assertion
> the proper form to ensure that the second 'req' will receive a 'done'
> within the specified time period?
>
> According to the emphasized sentence above, the answer is no.
> Both processes for the assertion will terminate with the first done
> (assuming it does not occur on the very next clock.)
>
> clk __ __ __ __ __ __ __ __
> ____| |__| |__| |__| |__| |__| |__| |__|
> _____ _____
> req ____| |_____| |__________________________________
> ___________
> done ______________________| |______________________
> _____
> done2 ______________________| |____________________________
>
> Would the assertion pass if the wavefrom 'done2' was used for
> the 'done' signal. As currently defined both processes would
> pass, though waveform done2 is missing another 'done' pulse
> and should be considered an error.
>
> Is this consistent with VFV semantics for overlapping sequences?
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
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, here I might use the CBV modeling constructs to
make an FSM to count the number of outstanding "req"s with no "done".
Then I could sample the value of this counter into a local variable of
each thread that is spawned at a "req". The value of this local
variable tells the thread how many "done" signals to skip over before
looking for its own. This strategy requires a bound on the number of
outstanding "req"s with no "done". A solution along these lines could
be coded using regular expressions or recursive tasks.
Much more complicated protocol correspondences are routinely coded
in CBV.
I hope this helps!
> ---------------------------------------------------
> Thanks again John!
>
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Apr 12 2002 - 11:29:53 PDT