| Login | | Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. | |
| Who's Online | There are currently, 53 guest(s) and 0 member(s) that are online.
You are Anonymous user. You can register for free by clicking here | |
 | |
|
Verification Guild: Forums |
|
| View previous topic :: View next topic |
| Author |
Message |
MikeP
Junior
Joined: Jun 15, 2004
Posts: 5
Location: Waltham, MA
|
 Posted: Wed Jun 23, 2004 11:40 am Post subject: Overflowing SVA Local Variables |
 |
|
Hey all,
I'm back with another SVA can of worms. Let's say you have a property like:
"If event A and event B initially occur K clock cycles apart, then thereafter they should always occur at most K clock cycles apart."
In the previous thread (Type Checking SVA Parameters) we determined that it seems to be legal to use local variables in ranges. Therefore the property could be expressed something like this:
| Code: |
sequence foo(A, B);
int [7:0] K;
(A, K = 0) ##1 ('true, K = K + 1) [*0:$] ##1 B ##1 (A ##[0:K] B)[*0:$];
endsequence
|
(Of course, this may also be entirely illegal SVA. It may just be that this property cannot be expressed in SVA or PSL.)
Now here's the problem. It's entirely possible to overflow K, especially since it was naively declared signed instead of unsigned. In this case, the simulator would now be checking against a negative range, which is explicitly forbidden by the semantics, and hence would obviously cause the universe to end in some horrible manner.
In my opinion there are several lessons to learn from this:
* It is the assertion writer's responsibility to ensure that SVA local variables are large enough to handle the task at hand. They should not naively be treated like Java variables.
* Unsigned variables should be used where appropriate, as they seem to play more nicely with a semantics based on moving forward. Basically, unsigned local variables should be the default, and signed only used for special cases.
* Sequences which are meant to be reused in unknown future contexts require explicit overflow checks. Don't fall into the "no one will ever run this for more than 32,000 CCs" trap. That's the kind of assumption assertion-based design is supposed to discourage.
Does anyone else have thoughts on checking local variables for overflow?
MikeP
BlueSpec |
|
| Back to top |
|
 |
|
|
You can post new topics in this forum
You can reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
|
| |
|
|
Forum FAQ
Search
Usergroups
Profile
Digest
Log in
