电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2008年
5期
886-892
,共7页
冯毅%易江芳%刘丹%佟冬%程旭
馮毅%易江芳%劉丹%佟鼕%程旭
풍의%역강방%류단%동동%정욱
形式化验证%模型检验%跨时钟域设计%线性时序逻辑
形式化驗證%模型檢驗%跨時鐘域設計%線性時序邏輯
형식화험증%모형검험%과시종역설계%선성시서라집
传统方法无法在RTL验证阶段全面验证SoC系统芯片中的跨时钟域设计.为解决此问题,本文首先提出描述亚稳态现象的等价电路实现,用以在RTL验证中准确体现亚稳态现象的实际影响;然后使用线性时序逻辑对跨时钟域设计进行设计规范的描述;为缓解模型检验的空间爆炸问题,进一步针对跨时钟域设计的特点提出基于输入信号的迁移关系分组策略和基于数学归纳的优化策略.实验结果表明本文提出的方法不仅呵以在RTL验证阶段有效地发现跨时钟域设计的功能错误,而且可以使验证时间随实验用例中寄存器数量的递增趋势从近似指数级增长减小到近似多项式级增长.
傳統方法無法在RTL驗證階段全麵驗證SoC繫統芯片中的跨時鐘域設計.為解決此問題,本文首先提齣描述亞穩態現象的等價電路實現,用以在RTL驗證中準確體現亞穩態現象的實際影響;然後使用線性時序邏輯對跨時鐘域設計進行設計規範的描述;為緩解模型檢驗的空間爆炸問題,進一步針對跨時鐘域設計的特點提齣基于輸入信號的遷移關繫分組策略和基于數學歸納的優化策略.實驗結果錶明本文提齣的方法不僅呵以在RTL驗證階段有效地髮現跨時鐘域設計的功能錯誤,而且可以使驗證時間隨實驗用例中寄存器數量的遞增趨勢從近似指數級增長減小到近似多項式級增長.
전통방법무법재RTL험증계단전면험증SoC계통심편중적과시종역설계.위해결차문제,본문수선제출묘술아은태현상적등개전로실현,용이재RTL험증중준학체현아은태현상적실제영향;연후사용선성시서라집대과시종역설계진행설계규범적묘술;위완해모형검험적공간폭작문제,진일보침대과시종역설계적특점제출기우수입신호적천이관계분조책략화기우수학귀납적우화책략.실험결과표명본문제출적방법불부가이재RTL험증계단유효지발현과시종역설계적공능착오,이차가이사험증시간수실험용례중기존기수량적체증추세종근사지수급증장감소도근사다항식급증장.
