source: vis_dev/vis-2.1/examples/treearbiter/README @ 14

[4,8]-arbit.v  are instantiations of a tree based mutual 
exclusion circuit. They are reasonably well documented, 
and should be useful in illustrating how to code Verilog 
for VIS, how to use fairness and nondeterminism for 
to model the  environment  modules. There is no nondeterminisn
in the arbiter cells; they are synthesizable. I used
this example in my class (it was a HW problem, and this is 
the model solution).

FILES - 4-arbit.v = verilog source
                4-arbit.mv = compiled blif-mv
                4-arbit.fair = fairness constraints
                4-arbit.ctl = properties to be checked