基于形式验证的多周期路径检测技术

Formal Verification Based Detection Technology of Multicycle Path

摘要:

多周期路径是将复杂电路运算拆分在多个时钟周期完成，从而提高电路总体运行频率的一种方法。在设计和验证中，多周期路径约束错误会导致设计迭代反复和验证误报。本文对多周期路径的产生机理和设计验证中常见的问题进行分类分析，提出一种用静态时序分析和形式验证结合来查找设计中的多周期路径的方法，首先通过静态时序分析，查找出时序违例的路径，针对这些路径，插入设计的检测电路，检测电路主要通过检测目的触发器采样控制信号有效时间，来判断该路径是否为多周期路径。采用基于断言的形式验证，用自动化的手段检测多周期路径。实践结果表明，该方法针对两种时钟下的多周期路径，能够100%准确的检测出违例的多周期路径，避免多周期路径错误约束，省略人工分析和动态仿真确认多周期路径环节。

Abstract:

A multicycle path is a way to split complex circuit operations over multiple clock cycles to improve the clock frequency of the circuit. The error constraint of multicycle path may cause design iterations and false positives in design and verification. In this paper, the generation mechanism of multicycle path and the common problems in design and verification are classified and analyzed. A method of finding multicycle paths in design is presented by combining formal verification with static timing analysis.Firstly, through static time sequence analysis, the paths of time sequence violation are found out. Then, the designed detection circuit is inserted for these paths. By detecting the destination register sampling control signal valid time, whether the path is a multicycle path can be determined. The detection circuit is validated in the form of assertions, and multicycle paths are detected by automated means.The results show that the proposed method can detect all error multicycle paths under two clocks effectively, and avoid the error constraint of multicycle path, and omit the manual analysis to confirm the multicycle path.