Higher Order Logic and Hardware Verification