随着机器学习技术深入人们的生活，从消费电子到移动监控系统再到更高安全相关领域中，其软硬件质量变得与我们的生命安全财产安全息息相关。形式化验证技术以其严谨些与高度数学化的特点，已经成为了保证系统正确性的关键技术。对应机器学习系统的需求，AI加速芯片因其对系统性能的巨大提升近期被广大关注着，为了追赶日新月异的神经网络算法，大批研究从硬件架构上支持密集计算程序的执行效能，但如何确保这些快速开发下的执行正确性。对于这类AI加速软硬件系统，本项目选取其加速的两大模式：混合精度浮点数的配置和并行数据向量运算配置。由于浮点数参与的计算产生的误差影响有着非线性的特点，一般通用自动化验证工具不可对其直接验证求解。要构造自动化的求解过程需要对这些验证混合精度浮点数问题以及并行数据处理问题进行模型优化及转换。为此形成自动化的形式化验证方法及工具链是本研究主要研究目标。

While machine learning technologies become ubiquitous in our daily life, the quality of these systems has been closely related to the security of our lives and properties. Thanks to its rigorous and mathematical characteristics, formal methods become one of the key techniques to verify the correctness of systems. As the rapidly developed neural network algorithms lead the needs of faster chip foundations, more and more researches focus on the idea of AI accelerator chips. How to provide correctness and availability under fast development is the main question. For these customized accelerator chips, the research aimed at the configurable mix-precision of floating points and the parallel computation of vectorized floating points. For verifying the rounding error will not lead to system exceptions or wrong results. The existing automatic theorem provers have a problem with the non-linear of floating points. Therefore, additional research on how to formally define and verify the two acceleration helpers will be the main goals.