| 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, 52 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 |
Pappu
Senior
Joined: Oct 08, 2004
Posts: 47
|
 Posted: Wed Dec 01, 2004 1:39 am Post subject: Verifying an Arbiter using a FV Tool (model checking) |
 |
|
I will appreciate any pointers on how to break up the design to derive the maximum benefit. Should we go top down or bottom up. Especially, when we want to verify the arbiter's priority resolution, should we code a higher level model in the property specification language to calculate the master which will get the priority or just write some "test cases" with different priorities.
Thanks |
|
| Back to top |
|
 |
odellconnie
Junior
Joined: May 10, 2004
Posts: 8
|
| Posted: Wed Dec 01, 2004 9:21 am Post subject: Verifying an Arbiter using a FV Tool (model checking) |
|
|
Pappu,
You have the right idea with the first approach. I would caution you against using properties that re-implement the design too closely, though.
This just allows the same bug to be re-written in your assertions.
I prefer to think of the spec the arbiter implements, and code that up, for instance, if the prioritization scheme guarantees that a request on a class of inputs will result in a grant within 4 clock cycles, then that is a assertion.
If a lower priority request is guaranteed only to be responded to eventually, I will write an assertion like that.
(This usually requires writing an assumption that eventually a period will occur where no higher priority requests are made for some period of time, which is the hardest part).
The benefit of the high-level specification is that it is easier to see that your design implements the english-language spec, and also it is often less work 
Also, the benefit of this over specific test cases is that it allows you to find bugs that you haven't anticipated, since the formal engine will probably try combinations and sequences of requests that you haven't anticipated, in the effort to find ways your design violates your spec.
Good luck!
Connie L. O'Dell
CO Consulting, Inc.
c.odell@co-consulting.net
Boulder, CO
http//co-consulting.net |
|
| Back to top |
|
|
Pappu
Senior
Joined: Oct 08, 2004
Posts: 47
|
| Posted: Wed Dec 01, 2004 11:39 pm Post subject: |
|
|
Thanks Connie. One of the problems we run into is constraining the other signals when verifying the correct priority resolution in the arbiter.
For example, the master with the highest priority bus request will get a bug grant, provided no other master is already parked on the bus or no other transaction is already in progress (the request may time out).
Thanks |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Thu Dec 02, 2004 5:31 am Post subject: |
|
|
pappu,
| Quote: | | For example, the master with the highest priority bus request will get a bug grant, provided no other master is already parked on the bus or no other transaction is already in progress (the request may time out). |
be careful. this sounds very close to what connie meant by
| Quote: | I would caution you against using properties that re-implement the design too closely, though.
This just allows the same bug to be re-written in your assertions. |
does your spec allow the case where a high priority bus request is never serviced because whenever it appears another transaction is already in progress? if not, then you need to take a step back and write some assertions at an even higher level: if a high priority request tries for a grant (and tries again whenever it is not granted), then eventually it will get a grant.
what about lower priority requests? are they guaranteed to eventually be granted, albeit at a lower priority? if so, then you need the same type of property for them as well.
if you do not write such properties, you run the risk of missing specification bugs (a livelock is allowed) as well as design bugs. that is, i would expand connie's caution to properties that re-implement the specification too closely as well. the spec usually says how something is done, and frequently leaves the what (e.g. lack of livelock) as an unspoken assumption.
have fun,
cindy. |
|
| Back to top |
|
|
hemanth
Senior
Joined: Aug 16, 2004
Posts: 93
Location: Bangalore
|
| Posted: Fri Dec 03, 2004 12:36 am Post subject: |
|
|
cindy,
In the case of arbiter isnt the spec just restricted to the fairness of an arbiter in a particular sense, then what pappu mentions may well be the spec. and if I am not mistaken dont specs speak of what to rather than how to?? |
|
| Back to top |
|
|
cindy
Industry Expert
Joined: Aug 17, 2004
Posts: 309
|
| Posted: Sun Dec 05, 2004 2:39 am Post subject: |
|
|
hemanth,
| Quote: | | if I am not mistaken dont specs speak of what to rather than how to?? |
of course, that is what a spec is supposed to do. but unfortunately, most of them don't. for instance, how many times have you seen it written in the spec that "the chipset should not deadlock"? probably never. lack of deadlock (or livelock) is usually taken for granted and so not stated explicitly in the spec.
furthermore, there are at least two levels of "what" and "how". at the level you are thinking of, the "what" is that the master with the highest priority bus request will get a bus grant. the "how" is the particular configuration of registers and gates that achieve this functionality. at this level, the spec indeed describes the "what".
but take another step back, and you see that the "what" is that high priority requests are given higher priority while still letting low priority requests have a chance, and in addition, no deadlock or livelock (a very generic description of an arbiter). part of the "how" is that the master with the highest priority bus request will get a bus grant. at this level, the spec describes "how", not "what".
in verification, it is important to take that step back, and make sure you are checking the bigger picture of "what". otherwise, you may end up with a chip that obeys the spec, but doesn't work.
cindy. |
|
| 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
