电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2009年
2期
258-265
,共8页
冯毅%许经纬%易江芳%佟冬%程旭
馮毅%許經緯%易江芳%佟鼕%程旭
풍의%허경위%역강방%동동%정욱
形式化验证%模型检验%跨时钟域设计%电路特性生成
形式化驗證%模型檢驗%跨時鐘域設計%電路特性生成
형식화험증%모형검험%과시종역설계%전로특성생성
对跨时钟域设计进行功能验证是SoC验证中的难点问题.传统的面向跨时钟域设计的模型检验方法并没有充分考虑电路特性描述的完整性问题,然而制订完整的电路特性是模型检验有效性的基础,不全面的电路特性描述将可能隐藏设计错误.为生成完整的描述跨时钟域设计的电路特性,本文首先提出基于有限状态自动机的电路特性生成方法;然后为缓解状态空间爆炸问题,提出基于亚稳态的数值化简策略.通过对两个典型的跨时钟域设计进行实验的结果表明,采用本文方法不仅能够达到100%的电路特性覆盖率,而且可以发现被传统方法隐藏的功能错误.同时模型检验的时间代价也能够得到大幅度降低.
對跨時鐘域設計進行功能驗證是SoC驗證中的難點問題.傳統的麵嚮跨時鐘域設計的模型檢驗方法併沒有充分攷慮電路特性描述的完整性問題,然而製訂完整的電路特性是模型檢驗有效性的基礎,不全麵的電路特性描述將可能隱藏設計錯誤.為生成完整的描述跨時鐘域設計的電路特性,本文首先提齣基于有限狀態自動機的電路特性生成方法;然後為緩解狀態空間爆炸問題,提齣基于亞穩態的數值化簡策略.通過對兩箇典型的跨時鐘域設計進行實驗的結果錶明,採用本文方法不僅能夠達到100%的電路特性覆蓋率,而且可以髮現被傳統方法隱藏的功能錯誤.同時模型檢驗的時間代價也能夠得到大幅度降低.
대과시종역설계진행공능험증시SoC험증중적난점문제.전통적면향과시종역설계적모형검험방법병몰유충분고필전로특성묘술적완정성문제,연이제정완정적전로특성시모형검험유효성적기출,불전면적전로특성묘술장가능은장설계착오.위생성완정적묘술과시종역설계적전로특성,본문수선제출기우유한상태자동궤적전로특성생성방법;연후위완해상태공간폭작문제,제출기우아은태적수치화간책략.통과대량개전형적과시종역설계진행실험적결과표명,채용본문방법불부능구체도100%적전로특성복개솔,이차가이발현피전통방법은장적공능착오.동시모형검험적시간대개야능구득도대폭도강저.
