Subject: Re: more on Assertion discussion of FVTC languages
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Apr 12 2002 - 06:48:39 PDT
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.
:> 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.
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
: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...
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.
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 statments. Having if() makes me
think about where the else is. The syntax is a little heavier
than just delaying the sequence by N cycles.
: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? Or a variable
can only be written once until the assertion completes execution?
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?
---------------------------------------------------
Thanks again John!
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Apr 12 2002 - 06:50:34 PDT