Verifying an Arbiter Circuit