计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2012年
3期
268-270
,共3页
罗莉%欧国东%刘彬%徐炜遐%窦强
囉莉%歐國東%劉彬%徐煒遐%竇彊
라리%구국동%류빈%서위하%두강
CDC(Clock Domain Crossing)%异步FIFO%LTL%符号模型检验%SMV
CDC(Clock Domain Crossing)%異步FIFO%LTL%符號模型檢驗%SMV
CDC(Clock Domain Crossing)%이보FIFO%LTL%부호모형검험%SMV
跨时钟域(Clock Domain Crossing,CDC)设计和验证是SOC系统芯片设计的关键问题.讨论了异步FIFO的模型检验方法,利用模型检验工具SMV,建立了异步FIFO的有限状态机模型,使用时序逻辑LTL对该模型和属性进行了描述和验证.实验结果达到要求,同时表明该方法是行之有效的.与传统的模拟和仿真等验证方法相比较,模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点.
跨時鐘域(Clock Domain Crossing,CDC)設計和驗證是SOC繫統芯片設計的關鍵問題.討論瞭異步FIFO的模型檢驗方法,利用模型檢驗工具SMV,建立瞭異步FIFO的有限狀態機模型,使用時序邏輯LTL對該模型和屬性進行瞭描述和驗證.實驗結果達到要求,同時錶明該方法是行之有效的.與傳統的模擬和倣真等驗證方法相比較,模型檢驗具有能夠自動進行、驗證速度快、不用書寫測試激勵等優點.
과시종역(Clock Domain Crossing,CDC)설계화험증시SOC계통심편설계적관건문제.토론료이보FIFO적모형검험방법,이용모형검험공구SMV,건립료이보FIFO적유한상태궤모형,사용시서라집LTL대해모형화속성진행료묘술화험증.실험결과체도요구,동시표명해방법시행지유효적.여전통적모의화방진등험증방법상비교,모형검험구유능구자동진행、험증속도쾌、불용서사측시격려등우점.
