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

Formal Verification Based on Detection Technology of Multicycle Path

作　　者：朱秋岩 ZHU Qiuyan(Beijing Institute of Computer Technology and Application,Beijing 100854,China)

机构地区：[1]北京航天自动控制研究所,北京100854

出　　处：《计算机测量与控制》2022年第4期35-39,97,共6页Computer Measurement &Control

摘　　要：多周期路径是将复杂电路运算拆分在多个时钟周期完成,从而提高电路总体运行频率的一种方法;在设计和验证中,多周期路径约束错误会导致设计迭代反复和验证误报;文章对多周期路径的产生机理和设计验证中常见的问题进行分类分析,提出一种用静态时序分析和形式验证结合来查找设计中的多周期路径的方法,首先通过静态时序分析,查找出时序违例的路径,针对这些路径,插入设计的检测电路,检测电路主要通过检测目的触发器采样控制信号有效时间,来判断该路径是否为多周期路径;采用基于断言的形式验证,用自动化的手段检测多周期路径;实践结果表明,该方法针对两种时钟下的多周期路径,能够100%准确地检测出违例的多周期路径,避免多周期路径错误约束,省略人工分析和动态仿真确认多周期路径环节。A multicycle path is a way to split complex circuit operations into multiple clock cycles to improve the circuit clock frequency.The error constraint of multicycle path may cause design iterations and false positives in design and verification.In this paper,the generation mechanism for multicycle path and the common problems in design and verification are classified and analyzed.A method of finding multicycle paths 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 in these paths.By detecting the valid time for register sampling control signal,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 effectively detect all error multicycle paths within two clocks,and it avoids the error constraint of multicycle path,and omits the manual analysis to confirm the multicycle paths.

关 键 词：SOC验证 时序分析 形式验证 多周期路径 断言 

分 类 号：TN402[电子电信—微电子学与固体电子学]