AHB片上系统总线的建模与验证

• 作者: DONG Rong-sheng 张辉
• 来源期刊: 科技与创新
• 关键词: AHB 有限状态机 计算树逻辑 符号模型检验
• 年，卷（期）: 2008,（23）
• 所属期刊栏目: 片上系统SOC
• 页码范围: 152-154
• 页数: 3页
• 分类号: TP206
• 语种: 中文
• DOI: 10.3969/j.issn.1008-0570.2008.23.065

摘要

如何有效的对SoC设计进行验证已经成为缩短设计周期的关键问题.针对这个问题,本文提出一种形式化建模与验证方法,对片上系统AMBA工业总线规范的AHB总线协议进行形式化规格;建立了与AHB协议规格对应的有限状态机和SMV模型,使用CTL描述了仲裁器的公平性、从单元活性、从单元的交互操作性、互斥性和无饥饿属性;采用SMV模型检验器对AHB总线协议模型的无饥饿属性进行了自动化验证.结果表明所提方法能够有效应用于SoC的验证.