Subject: Final Assertion Spec -- problem noted.
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Apr 05 2002 - 07:50:25 PST
Good morning;
I also found that the keyword 'triggers' is stillthere in the BNF,
but is not explained in the text and should be removed.
The top paragraph on page 9 brings up a question that we did not
address - that of (to use Verisity's term) consuming an event.
The paragraph states:
If the assert statement is executed again before the sequence spawned
by the original execution has expired, then a new process shall be
spawned that looks for the sequence starting at the current timestep.
It is therefore possible to have multiple processes in-flight, each
monitoring the same sequence but offset in time. It is possible for
these multiple processes to be satisfied by the same sequential
behavior, even though the processes are offset in time.
** In such a case, both processes will terminate at the same
timestep, in which both sequences are satisfied."
One problem is this paragraph terminates in 'Consider:' with an
example that does not relate at all to this paragraph.
Second - the last sentence that I emphasized (**) will prevent
assertions with variable occurrences from being useful.
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 that waveform is missing another 'done' pulse.
Is this consistent with VFV semantics for overlapping sequences?
This is a serious problem as currently defined. One will be in
danger of providing false positives!
IMHO I propose:
"In such a case, the first process requiring that event will
have priority to consume it. Subsequent processes will need to
wait for the next time the event occurrs."
We have not seen any cases where the current behavior is desirable
over this proposed behavior. Anyone else on the committe have
alternate experiences? I know there are people with existing
assertion tools/languages.
--------------------
BTW, what was the concensus on the assume/guarantee question from VFV?
I presume that it will be a tool issue to allow specification of
which properties to assume or prove.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Apr 05 2002 - 07:51:57 PST