数据处理是我们这个时代最大的特点，人工智能、深度学习、5G等新兴技术的出现，对于处理器计算能力提出了更高的要求。在超标量处理器设计中，支持SIMD的向量浮点单元将会得到更多的应用。　　支持向量指令的浮点单元最大数据位宽为128位，因其庞大的输入状态空间，基于仿真的模拟验证需要花费大量的时间，且无法遍历整个状态空间。形式验证使用数学推理的方式，遍历整个状态空间，适用于浮点这类的计算单元，可以快速且完备地完成验证工作，缩短产品上市周期。　　本文的估值模块采用基于查找表的分段线性近似法进行快速估算，速度快，运算周期短，支持向量运算，大大提高了处理器运算性能。估值单元输出是近似值，其输出结果只需满足相对误差要求。对其验证时，需要将输出的二进制浮点数转换成十进制，进而判断结果是否满足精度要求，而相对误差的计算又会引入复杂的运算，对基于BDD和SAT算法的形式化验证引擎，复杂的运算操作会极速增加状态空间，导致内存爆炸，验证无法收敛。　　针对内存爆炸的问题，本文根据估值模块具体的设计结构，采用多种策略，解决了状态空间爆炸的问题，成功对估值模块进行证明。目前，业界主流形式化验证工具仅支持基于RTL和网表的参考模型，实现RTL-RTL/RTL-GATE的等价性形式验证。本文选用ATEC公司的等价性验证工具，使用C语言构建参考模型，成功实现了RTL-C的等价性验证。