Re: [sv-ac] technical reports // variable as ranges

 
 
John,
After some more thoughts, I believe that the LRM nees to change this one one
in:
2. LRM Section 17.6 Declaring Sequences
...A sequence can be declared with optional formal arguments...
..
-upper range as $
TO:
-upper range as $ or a static natural number.
That would fix things.
BTW, we discussed this in the Verification Guild,
 
ref:
_http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=490&postdays=0&postorder=asc&start=0_
(http://verificationguild.com/modules.php?name=Forums&file=viewtopic&t=490&postdays=0&postorder=asc&start=0)
and the question " Question2: Can the delay range be dynamic using a
variable, like ##[5:w]
My thoughts: NO. The range must be known at compile time, like ##[0:5], or
##[0:$] "
with the answer, based on 17.6 " This actually seems to be saying that you
the answer is YES, since I could have written a $ for the upper range in my
example. "
 
As you can see, thos is an aread that created confusion, and the LRM needs
to clarify this point.
Thanks,
Ben
 
In a message dated 6/29/2004 12:18:23 AM Pacific Standard Time, VhdlCohen
writes:

 
John,
Thanks for your quick reply. Minor comments.
 

1. From the perspective of the formal semantics, local variables
cannot influence the endpoints of temporal ranges
   ** That makes sense since the sequence_instance.ended cannot be
dynamically changed, as with the case of a variable used in the range (a variable
can be changed within the sequence).
 

2. LRM Section 17.6 Declaring Sequences
...A sequence can be declared with optional formal arguments...

An actual argument can replace an:
-Identifier
-Expression
-Event control expression
-upper range as $
 
Thus, the following should be legal (not addressed in the report (I
believe))
  sequence qReqAckDone(upper);
     req ##[1:upper] ack ##1 xfr[*0:upper] ##1 done;
endsequence : qReqAckDone
 
However, you stated "In other words, the endpoints of the temporal range
operators must be compile-time constants."
If I instante the above sequence witht the following, the endppoint will not
be known at compile time!
module t ...;
   int upper_sig;
   always @ (posedge clk) upper_sig <= input_data; // upper_sig is dynamic
 
property MaybeLegal_butEndpointIsNotKnownAtCompileTime;
   @ (posedge clk) ready |=> qReqAckDone(upper_sig); // sequence define
above
 endproperty
assert property ( MaybeLegal_butEndpointIsNotKnownAtCompileTime);
 
property WithEndPoint_mayNotBeLegal;
   @ (posedge clk) ready |=>
       ##[0:100] qReqAckDone(upper_sig).ended;
endproperty
assert property ( WithEndPoint_mayNotBeLegal);
// qReqAckDone(upper_sig).ended is not be known at compile time because
uuper_sig is dynamic! Violation of your premise of compile time constants?
 
3. Thanks for your solution .. complex, but it works
 
<sequence qReqAckDone(upper, lower, rep);

int vupper, vlower, vrep, x;

(req, vupper=upper, vlower=lower, vrep=rep, x = 0)
##1 (x < vupper, x = x+1)[*0:$]
##0 ((x >= vlower) && ack, x = 0)
##1 (xfr && (x < vrep), x = x+1)[*0:$]
##1 done;

endsequence : qReqAckDone
>
Thanks again,
Ben

 
In a message dated 6/28/2004 10:54:03 PM Pacific Standard Time,
john.havlicek@freescale.com writes:

From the perspective of the formal semantics, local variables
cannot influence the endpoints of temporal ranges. This is
because all temporal range operators are defined as derived
from explicit constant range operators. In other words, the
endpoints of the temporal range operators must be compile-time
constants. I do not know if the BNF allows your example, but
there is no formal semantics defined for your use of local
variables in the endpoints of ##[m:n] and [*m:n]. Thus, I
would have to say that your example is illegal.

-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
_http://www.vhdlcohen.com/_ (http://www.vhdlcohen.com/) vhdlcohen@aol.com
Author of following textbooks:
* Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004 isbn
 0-9705394-6-0
* Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
0-9705394-2-8
* Component Design by Example ", 2001 isbn 0-9705394-0-1
* VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
* VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
------------------------------------------------------------------------------
Received on Tue, 29 Jun 2004 09:01:46 EDT