近年来，卷积神经网络（CNN）在图像处理和计算机视觉领域取得了巨大成功，如人脸识别、姿态估计等。然而，基于CNN的图像处理单元设计复杂，验证工作面临巨大挑战。传统的仿真验证方法难以覆盖其庞大的配置空间，且耗时费力。本文将介绍一种创新的形式化验证（Formal Verification, FV）方法，用于高效验证CNN图像处理单元。
验证挑战
CNN图像处理单元的配置空间极为庞大（约2Nx1000，N>0），数据处理算法复杂。传统的仿真验证方法，无论是定向测试还是约束随机测试，都难以有效覆盖如此庞大的配置空间。此外，市场对产品上市时间的要求限制了验证时间，使得通过仿真验证完全覆盖所有配置变得不切实际。
形式化验证方法
开发帧断言IP（Frame Assertion IP, AIP）
图像处理过程中，图像被分割成多个帧，每个帧又分为多个像素。帧具有以下属性：
•  SOF（Start of Frame）：帧起始
•  EOF（End of Frame）：帧结束
•  SOL（Start of Line）：行起始
•  EOL（End of Line）：行结束
帧AIP通过断言确保每个像素的属性正确，包括：
1.  像素位置与属性匹配的断言（如行首像素应有SOL属性）
2.  帧完整性断言（如帧起始后必须有帧结束）
3.  帧存在性断言（如无帧时最终会出现帧）
加速FV测试平