近年来，卷积神经网络（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测试平台搭建
1. 配置寄存器黑盒化：降低设计复杂度，实现零周期配置
2. 在输入输出接口使用帧AIP：输入侧作为假设确保正确帧输入，输出侧作为断言检查帧属性
3. 最大化使用断言IP：根据设计需求使用其他通用或自定义AIP
确保最后数据送出
通过在DUT输出接口实例化帧AIP的第二组断言，确保像素推送机制无缺陷。例如，断言SOF |=> s_eventually EOF可检测像素是否卡在内部缓冲区。
死锁/活锁检测
利用帧AIP的第三组断言~Frame |=> s_eventually Frame，在输入接口作为假设驱动连续帧像素，在输出接口作为断言检测连续输出像素，从而发现可能导致系统挂起的死锁或活锁。
编写FPV友好的算法模型
采用双帧（F1和F2）切换机制，确保在DUT处理帧时，FV模型使用稳定帧，避免不必要的缓冲复杂度。
重叠本地检查器组合
摒弃难以实现的端到端检查器，将设计划分为多个逻辑分区，编写覆盖每个分区的本地检查器。通过重叠分区和检查器，确保每个部分正确性，最终保证整体设计无缺陷。
案例研究
在实际的CNN图像处理单元验证中，应用上述技术：
• DUT规格：22000种可能配置，支持12个输入帧和12个输出帧并行处理，帧大小为4k×2k像素
• 抽象：将帧大小缩减为16×16，配置寄存器黑盒化
• 验证结果：发现45个以上设计缺陷，验证时间缩短50%以上，覆盖率达到100%
结论
基于CNN的图像处理单元验证复杂度高，传统仿真方法难以应对。形式化验证方法，特别是本文介绍的这些技术，为高效验证提供了有效途径。通过减少验证时间和资源消耗，同时保证100%覆盖率和设计质量，这些方法在实际应用中取得了显著成效。未来计划将这些技术推广到更先进的CNN设计验证中，涵盖客户端和服务器端的SOC。
参考文章
A Novel Approach to Verify CNN Based
Image Processing Unit
数字芯片资料不定时更新，建议转存。
链接：https://pan.baidu.com/s/1QJXXQoU3Wly6KaGShT7jlg?pwd=3uMy提取码：3uMy复制这段内容打开「百度网盘APP即可获取」