Subject: Re: [sv-ac] First match example and match of past.
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Feb 13 2003 - 01:21:57 PST
adam,
regarding your first question:
>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'.
it depends on what your specification is. if your specification is "for
every match of the antecedent", then no, you don't need first_match. if
your specification is "for the first match of the antecedent", then you do
need first_match.
that was the short answer. the long answer is that in many cases, if you
have multiple matches of the antecedent, it is a bug that you will catch
with another assertion. therefore, you are expecting only one match, and
it is simpler visually and conceptually to leave out the first_match. for
instance, suppose the specification is "if i have a request followed within
three cycles by an ack, then starting the cycle after the ack, (d;e;f). so
the spec is
assert @(posedge clk) (req; [1:3] ack) => (1;d;e;f); (2)
now, if you get two acks for the same req, it is a bug. so i would need
another assertion that checks this:
assert @(posedge clk) never (req; (ack*=[2:3] and 1*[3])); (3)
in this particular design (and in many like it), it doesn't matter whether
i use first_match or not in (2).
regarding your second question:
>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.
here is how i would do it. first, check that every request completes
within 100 cycles. then, check that a tag is never re-used before it is
legal to do so (i.e., there are never two uses of a tag for a request
without a completion for that tag between them). finally, check that for
each request, there is a single acknowledge per request (i.e., that there
are never two uses of a tag for completion without a request for that tag
between them). so we get:
assert @(posedge clk) ( req =>
((int rtag=req_tag) [1:100] (done && done_tag == rtag) else
$error("Request tag %0d didn't complete within 100 cycles.", rtag);
assert @(posedge clk) never ((int rtag=req_tag) req ;
!(done && done_tag == rtag)*[1:inf] ;[0] req && req_tag == rtag) else
$error("Request tag %0d re-used before done received.", rtag);
assert @(posedge clk) never ((int dtag=done_tag) done ;
!(req && req_tag == dtag)*[1:inf] ;[0] done && done_tag == dtag) else
$error("Two acknowledges received for request tag %0d.", dtag);
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
Adam Krolnik <krolnik@lsil.com>@eda.org on 10/02/2003 22:50:11
Sent by: owner-sv-ac@eda.org
To: sv-ac@eda.org
cc:
Subject: [sv-ac] First match example and match of past.
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 : Thu Feb 13 2003 - 01:19:12 PST