Subject: Re: [sv-ec] Fwd: [sv-ac] SVAC 0.79 template example
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Feb 03 2003 - 09:48:08 PST
Hi Surrendra;
Okay, I read your template and have a few comments.
1. Now we need this clocking domain in a template.
How does this compare to a set of assertions written in a module?
Why would one not allow an always block (like modules) to contain
this satelite FSM state code?
int req_cnt = 0; // initialized to 0 prior to any clock tick
int ack_cnt = 0; // initialized to 0 prior to any clock tick
always @(posedge clk)
begin
if (req) req_cnt <= req_cnt + 1'b1;
if (ack ) ack_cnt <= ack_cnt + 1'b1;
end
2. This is not a good restriction that you have written as a comment.
"// you cannot use assert or cover inside a clocking domain"
While good methodology may include the statement,
"Define named properties and assert or cover these names.
This allows for reuse of the properties independent of the
existing assertion or coverage directives."
I think the syntax should still allow the shorter form as I originally
wrote:
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.
[The clock specification is an independent thing.]
I think this is also an acceptable way of specifying assertions as you don't
have to search back up for what the property is, or search down to see how a
property is used (assert/cover, etc.) or if it is.
3. The property to ensure ack's match req's is interesting:
property match_req_p = (req_cnt - ack_cnt >= 0); // you never have an extra ack
This only works due to the assumption that the counters will never exceed their
maximum value. If these counters were defined to be smaller than 32 bits, then
this assumption may be violated.
Would this be an issue (32 bit state variables)
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Mon Feb 03 2003 - 09:50:50 PST