Subject: [sv-ac] First match example and match of past.
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Feb 10 2003 - 12:50:11 PST
Good afternoon all;
I have two questions about examples of assertions I have been trying to code...
1. I have an example assertion that brings up a question about first match and its
use.
assert @(posedge clk) (a; [1:3] b => {1; c; d}); (1)
Given that the antecedent could match 3 different ways, wouldn't I need first_match
to find sequences that starts uniquely with 'a' and progresses to 'c'.
Thus this would find a, then find a 'b', then check the rest. Without first_match,
if there was another 'b' wouldn't I possibly get a false failure of finding this 'b'
and no 'c' or 'd' ?
assert @(posedge clk) (a; first_match([1:3] b) => {1; c; d}); (2)
What would be an example where first_match is necessary if this is not one?
2. I'm trying to writeup an out of order (tagged) request/acknowledge protocol checker.
The requirements are:
1. Ensure that a transaction is never lost (that is, completes within 100
cycles).
2. Ensure that for each request, there exists only one corresponding acknowledge.
E.g. Two acknowledges with the same tag would be an error.
We use an additional tag array (indexed by the tag number) for requests and one for
acknowledges. We do this to pair request/acknowledge pulses uniquely.
-------
// assert request 1 completes within 100 cycles.
always @(posedge clk) begin
// Increment counter each time event is seen.
if (req) req_cnt[req_tag] <= req_cnt[req_tag] + 1;
if (done) done_cnt[done_tag] <= done_cnt[done_tag] + 1;
end
-----
The first assertion is simple. See request, remember tag, find done with
matching tag. Then check req_cnt/done_cnt array values to see if they match.
If done not found within 100 cycle window, error.
//#1
assert @(posedge clk) ( req =>
((int rtag=req_tag) [1:100] (done && done_tag == rtag &&
done_cnt[req_tag] == req_cnt[req_tag]) else
$error("Request tag %0d didn't complete within 100 cycles.", rtag);
The second requirement is harder. I use $past() to time shift my request signals (req,
req_tag) 100 cycles into the future so that I look at the values once I find the
acknowledge.
assert @(posedge clk) ( done =>
((int dtag = done_tag) [1:100]
$past(req, 100) && $past(req_tag, 100) == dtag) &&
done_cnt[done_tag]==$past(req_cnt[done_tag],100))) else
$error("Done for tag %0d does not match any past request.", dtag);
By moving the req and req_tag into the future I can write an assertion like #1 - find
done, remember tag, find request ...
I was trying to determine how small I could make these extra counter arrays (req_cnt,
done_cnt.) I thought a few bits would be enough - but then I realized that if the
requests were close enough together one could get the same count value within
that 100 cycles. E.g. with a count of 8 allowed, I could have one tag value get
requested 10 times within 100 cycles if the return acknowledge was fast.
So it would seem that the size of these counting arrays has to be tied to the
size of the timeout window.
Has anyone seen another way to do this? This is a lot of state to keep track of
a set of requests within a finite window time...
THanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Feb 10 2003 - 12:52:34 PST