采用虚拟时钟的多时钟域电路模型检测

Formal Model Checking to Multi-Clock Design by Using Virtual Clock

随着系统规模的扩大和复杂性的增加,设计验证已成为集成电路设计中最大的挑战。符号模型检测(Formal model check)的验证方法由于可以解决验证的完备性问题,正受到越来越多的重视。在多时钟域设计已成为大规模集成电路设计热门领域的今天,原来的符号模型检测方法无法直接进行多时钟域的验证。通过建立一个虚拟时钟来代替原来的多个时钟,并对原电路以及CTL(Computation Tree Logic)进行适当改写,使之能直接用符号模型检测的方法进行验证,并对改写的电路进行了复杂度分析。

As the scale and complexity of systems increase, design verification has become a significant challenge for ASIC design. Formal model check has received more and more attention due to its completeness of verification. However, the conventional formal model check is not applicable for multi-clock design. In this paper, a virtual clock was used to replace the original multi-clock, and the original design and computation tree logic （CTL） were modified, so that the formal model check can be used directly for verification. Finally, the complexity of modified design was analyzed.