利用Formal引擎提升复杂设计跨时钟域的检查和验证效率.pdf

设 计 【l】国集 成 电路 China Integrated C ircuit L 利用 Formal引擎提升复杂设计 跨时钟域的检查和验证效率 游余新 (明导 (上海)电子科技有限公司) 摘要：为了减少复杂设计中可能的亚稳态风险，不少公司都采用工具或人工来检查设计中存在跨时钟域 的问题。传统的检查方法只能检查设计 中是否做 了跨时钟域的处理，却无法检查处理得是否合理，而静 态Formal验证技术采用数学穷举的方法，利用断言对设计中的同步器进行快速验证，确保数据的可靠 传输，有效避免了一些设计缺陷。Mentor公司的QuestaCDC和Forma1工具可以对设计进行跨时钟域 的检查，并可用Forma1引擎证明设计中跨时钟域同步器与其断言的一致性，可极大地提高复杂设计的 验证效率和鲁棒性。 关键词：亚稳态；跨时钟域检查；静态验证技术 Formal；断言 Abstract：Inordertoreducetheriskofmetastabilityeffects，differenttoolsormanualchecking forclock domain crossing issuesareadoptedbymany companies． The traditionalchecking methodscancheckwhetherCDC issuesarehandledornot， butcan’tprovewhethertheyare handlescorrectly． Staticverificationtechnologywith assertionscan avoid theCDC bugsmore effectivelywith mathematicsexhaustivemethod， and make sure the data can be transferred inorereliably． MentorGraphic’SQuestaCDC andFormaltoolprovidestheclockdomain crossingcheckingeffectively，andverifiestheconsistencybetween CDC synchr0nizersandtheir assertionpropertiesviaFormalengine，whichcan improvetheverificationefficiencyanddesign robustnessgreatly． K ey words：Metastability；CDC Staticverificationtechnoloyg Formal；Assertion 1 概述 大主要原因之一 1【_。设计中的CDC (ClockDomain Crossing)问题主要分为三类 ，究其根本原因都是由 随着芯片复杂程度的增加，其拥有的时钟域也 于亚稳态造成。(1)亚稳态的传播 ；R／计者需要采用 越来越多，跨时钟域的问题已经成为重新流片的两 同步器方式去降低亚稳态传播的几率。(2)不同时 7nr苣笛，1d堋、嘲 圜 ■—【■【●C巾hina国In集tegr成ated电Cir路cuit 设…计 钟域之IiJ『号传播时 ¨{现数据破坏 ；有时设计者虽 CDC生成的断膏来枪 (：I)C 议的话，其断 的 然 c ：价 添JJI【r同步器，但仍兀法保证数据 激活仍取决于激励的完备性，没汁中仍彳丁¨丁能存在 接收点能I确接收来r1发送端的数据。这时需要 缺陷；而采川琏于属性的形式验证力法，可以通过数 没汁 利JHCI)C 议来保证数据 的完整性与正确 学方法穷举所