静态形式验证在跨时钟域和复位验证中的应用

摘要

With complex multi-clock-domain functional blocks integrated into Soc, errors in cross domain crossing (CDC) signals path design can lead to metastability, glitches or other functional failures. The issues caused by metastability and traditional verification methods are introduced. Compared to the traditional dynamic simulation method, which is time consuming and non-exhaustive, static formal verification leverages the power of mathematical method and checks the design exhaustively. It helps to improve Qo R of verification, and is quick, highly efficient and exhaustive. Various CDC and reset errors found by static formal method are given as examples to illustrate the challenges in multi-clock-domain designs. Verification results from design blocks of different scale are compared and analyzed.%Soc芯片的各个复杂功能模块中通常包含多个时钟域和复位域, 跨时钟域信号路径设计的错误可能引起亚稳态问题进而导致设计故障.本文介绍了亚稳态的危害、以及传统的验证方法.相对于传统动态仿真方法耗时、容易遗漏的缺点, 静态形式验证利用数学方法进行穷举, 可以高效、快速、完备的检查可能出现的所有场景, 提高验证的质量和效率.本文通过实例, 利用静态形式验证技术对不同规模的设计中存在的跨时钟域和复位问题进行检视, 并对验证结果进行了对比和分析.