Challenges of Formal Verification on Deep Learning Hardware Accelerator