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