Arbiter verification

anilo · Newbie Joined: May 20, 2004 Posts: 1

What are the different ways of verifying a reasonably complex arbiter that is embedded deep in the design. The arbiter has no direct access to the ports of the design. And another intresting situation is the arbiter arbitrates among the requests only when some of the internal design state conditions are satisfied. In such a scenario, what is the better approach to validate the arbiter?

Thanks

odellconnie · Junior Joined: May 10, 2004 Posts: 8

Formal verification (static property/model checking) is the canonical way to verify arbiters. There are three basic reasons:
1) arbiters have to deal with many corner cases correctly, as you have noted, and it is painful to generate and to ascertain that you have covered all cases of interest,
2) numerous design teams have applied formal to arbiters and any needed constraints/assumptions are straightforward to define (this is the major stumbling block for pure formal for most other design types)
3) Formal can and does exhaustively verify the arbiter, while with simulation you cannot hope to cover all the real variations for a complex arbiter.

Every time I go to "verify" an arbiter and I don't have formal in my toolkit, I will do what can be done with constrained random simulation of the arbiter as a unit, but I know that bugs are possibly being missed, when I could otherwise be doing it what I like to call "the right way".

Cheers,
Connie L. O'Dell
Sr. Verification Specialist
c.odell@co-consulting.net
303-641-5191
_____________________________________________
CO Consulting - Boulder, CO - http://co-consulting.net

bdeadman · Posted: Thu May 20, 2004 2:07 pm **Post subject:**

I think Connie is suggesting you verify the arbiter as a unit, ideally using formal modeling checking, whereas the original question seemed to suggest the arbiter ought to be tested when embedded in the system, and I'm not clear on the reason(s) for that?

If it must indeed be tested as part of the system, and probably by simulation, I would guess it's going to take a lot of cycles to get the system into each of the required corner cases, therefore I would suggest you look at some form of, ideally functional, coverage of the arbiter, since it will almost certainly be very difficult to be certain you've hit the required corner cases. You can then use this functional coverage to either manually, or semi-automatically drive the generation of additional test cases.

Finally, if the controllability of the arbiter is poor, it's probably fair to assume the observability is equally bad, therefore you might consider adding the kind of properties Connie mentioned as assertions on the arbiters behavior, to avoid faults not propagating to the design boundaries within the duration of the simulation.

Regards

Bernard

jeffli · Senior Joined: Jan 09, 2004 Posts: 32