Subject: [sv-ec] Fwd: [sv-ac] SVAC 0.79 template example
From: dudani@us04.synopsys.com
Date: Fri Jan 31 2003 - 13:37:00 PST
Hi Adam,
Please see the solution. There may be some errors as I don't know the exact
problem. Please also note that you use the clocking domain inside a
template, which allows you to declare variables with clock semantics. The
LRM will be updated with the clocking domain as an item for template body.
template pipeline_reqack(
clk, // The clock signal (posedge version)
req, // The request (single pulse) signal.
ack, // The acknowledge of completion, corresponding to a req.
latency, // The maximum time for an ack to be returned for req.
pipedepth) // The maximum number of requests waiting for acknowedges.
clocking my_clk @posedge clk; // this clock is used for all clocked
evaluations within this clocking domain
int req_cnt = 0; // initialized to 0 prior to any clock tick
int ack_cnt = 0; // initialized to 0 prior to any clock tick
// non blocking assignments are executed after all property related
evaluations are performed, so the
// new values are available at the next clock tick
req_cnt <= req ? req_cnt + 1'b1 : req_cnt;
ack_cnt <= ack ? ack_cnt + 1'b1 : ack_cnt;
property expect_req_then_ack_p = // clock is not needed as it is
under a clocking domain already
(req => ( (int cnt = req_cnt) // Note req_cnt to match
with ack_cnt.
(true ;[1: latency] ack && ack_cnt ==
cnt))); // matches with req.
property match_req_p = (req_cnt - ack_cnt >= 0); // you never have an
extra ack
property pipedepth_exceeded_p = (req_cnt - ack_cnt < pipedepth);
endclocking
// you cannot use assert or cover inside a clocking domain
expect_req_then_ack: assert (expect_req_then_ack_p);
else $error("Ack not received within
%0d cycles.", latency);
> match_req: assert (match_req_p);
else $error("Extra ack received w/ no corresponding
req.");
pipedepth_exceeded: assert (property pipedepth_exceeded_p) ;
else $error ("exceeded pipdepth (%0d)
of protocol for requests.", pipedepth);
endtemplate
Surrendra
>Date: Wed, 29 Jan 2003 16:14:15 -0600
>From: Adam Krolnik <krolnik@lsil.com>
>User-Agent: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.0.1)
>Gecko/20020920 Netscape/7.0
>X-Accept-Language: en-us, en
>To: sv-ac@eda.org
>Subject: [sv-ac] SVAC 0.79 template example
>Sender: owner-sv-ac@eda.org
>
>
>
>Hello all;
>
>
>Using the draft 0.79, I've tried to write an example template.
>
>I am trying to write a template to show that:
>
> For every request (pulse) there exists a corresponding ack (pulse).
> [expect_req_then_ack]
> For every ack (pulse) there exists a, previously sent, corresponding
> req (pulse).
> [match_req]
> Up to 4 request (pulses) (the pipedepth) may be sent before an ack (pulse)
> is returned. [pipedepth_exceeded]
>
>So I am trying to write this template.
>
>
>template pipeline_reqack(
> clk, // The clock signal (posedge version)
> req, // The request (single pulse) signal.
> ack, // The acknowledge of completion, corresponding to a req.
> latency, // The maximum time for an ack to be returned for req.
> pipedepth) // The maximum number of requests waiting for acknowedges.
>
> // Declare two counter to number requests and acknowledges.
> int req_cnt; // what is the initial value?
> int ack_cnt; // same Q.
>
> // Update the counters - but how? I can only write a nonblocking
> assignment.
> // When does these assignments execute?
> req_cnt <= req ? req_cnt + 1'b1 : req_cnt;
> ack_cnt <= ack ? ack_cnt + 1'b1 : ack_cnt;
>
> // Assertions
> expect_req_then_ack: assert @(posedge clk)
> (req => first_match ( (int cnt = req_cnt) // Note req_cnt to match
> with ack_cnt.
> ([1: latency] ack && ack_cnt == cnt))) //
> matches with req.
>
> else $error("Ack not received within %0d cycles.", latency);
>
> match_req: assert @(posedge clk)
> (ack => first_match ((int cnt = ack_cnt) // Note ack_cnt to match
> with past re
>
> //First, timeshift the req/req_cnt waveforms into the
> future, by latency.
> // Then look for the resulting future version of req
> matching the ack_cnt.
> ([1: latency -1] $past(req, latency) && $past(req_cnt,
> latency) == cnt))))
> else $error("Extra ack received w/ no corresponding req.");
>
> pipedepth_exceeded: assert @(posedge clk) (req_cnt - ack_cnt < pipedepth)
> else $error ("exceeded pipdepth (%0d) of protocol for requests.",
> pipedepth);
>
> endtemplate
>
>
>Questions:
>
> 1. What is the initial value of variables declared in the template?
> Is there some way to get back to an initial state (presumably if a reset
> term was asserted) ?
> 2. How do the variables get updated? - I presume the nonblocking
> statements update
> them.
> 3. With what clock do the nonblocking assignments get executed on?
> 4. Are there other problems with this template example?
>
>
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752
Tel: 508-263-8072
Fax: 508-263-8123
email: dudani@synopsys.com
**********************************************
This archive was generated by hypermail 2b28 : Fri Jan 31 2003 - 13:38:26 PST