Subject: Few more assertion examples/questions
From: Adam Krolnik (krolnik@lsil.com)
Date: Tue Mar 12 2002 - 08:00:19 PST
Hi Tom;
I will not be able to attend the meeting tomorrow (on the phone.)
My family and I are leaving early on a trip...
I've been thinking a little more about the assertion syntax.
Specifically
the retriggering each clock. We have found this to be an area of
pitfalls
when it comes to writing assertions. For example, (I will use Rajeev's
example
again, Thank you!)
always @(arbiterState or request)
if (arbiterState == GRANT)
assert reject(~request)
((arbiterState==GRANT)*[0:5]) @@(posedge clk);
Let's say that this assertion was inside some combinatorial logic
process:
always @(all_the_inputs_to_this_logic or the_states)
begin
<the block code>
...
assert reject (~request)
(arbiterState_next == GRANT triggers
((arbiterState==GRANT)*[0:5]) @@(posedge clk);
Should this still work?
The answer is most likely no. The reason is that this code will be
reexecuted
on the next cycle, causing us to recheck the arbiter state for another 5
cycles
of GRANT. This also happens if this assertion is alone in it's own
process:
always @(posedge clk)
assert reject (~request)
(arbiterState_next == GRANT triggers
((arbiterState==GRANT)*[0:5]);
We bypass this problem, by having engineers use the posedge() construct
to properly
fulfil the english statement, 'Once the fifo goes to READ state'. The
property then
reads:
always @(posedge clk)
assert reject (~request)
(posedge(arbiterState_next == GRANT) triggers
((arbiterState==GRANT)*[0:5]);
Here is the question for the group. Can I write an assertion to check
for these
waveforms (no missing / extra pulses.)
clk __ __ __ __ __ __ __ __
____| |__| |__| |__| |__| |__| |__| |__|
_____ _____
req ____| |_____| |__________________________________
___________
ack ______________________| |______________________
_____
ack2 ______________________| |____________________________
The protocol is that for every req(uest) there must be a matching
ack(nowledge)
within the next 1 to 10 cycles.
If I wrote:
always @(posedge clk)
assert_strobe (req triggers ([0:9];gnt);
Would this be sufficient to check that a grant is asserted for each
request?
Would this fail if ack2 was substituted above for ack?
How would I write the assertion to check that each grant was in response
to a single req?
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Tue Mar 12 2002 - 08:01:34 PST