Wishbone片上总线协议的形式化建模与模型检验分析
片上总线协议是片上总线技术的核心,其设计的好坏对片上系统的可靠性有着重大影响.由于片上总线协议自身的特点和复杂性,使得对其进行有效建模和验证提出了挑战.本文针对Wishbone片上总线协议的特点和复杂性,给出了一种形式化建模与验证方法.首先建立了共事总线互连模式下的IP核交互模型,并在此基础上,给出了协议执行的有限状态机分析模型;然后,用CTL对协议的无饥饿属性、公平性和互斥性进行了形式化规约;最后,采用SMV模型检验工具进行了验证.验证发现协议存在安全缺陷;该研究表明仲裁机制的不公平性容易导致总线饥饿的发生；同时也表明所给出的形式化建模方法的有效性.
片上总线 Wishbone总线协议 形式化建模 模型检验
谭华 古天龙 常亮
桂林电子科技大学计算机与控制学院 桂林 541004
国内会议
西安
中文
45-50
2009-08-17（万方平台首次上网日期，不代表论文的发表时间）