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

来源 :微计算机信息 | 被引量 : 0次 | 上传用户:xiaogaojuanJUAN
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
如何有效的对SoC设计进行验证已经成为缩短设计周期的关键问题.针对这个问题,本文提出一种形式化建模与验证方法,对片上系统AMBA工业总线规范的AHB总线协议进行形式化规格;建立了与AHB协议规格对应的有限状态机和SMV模型,使用CTL描述了仲裁器的公平性、从单元活性、从单元的交互操作性、互斥性和无饥饿属性;采用SMV模型检验器对AHB总线协议模型的无饥饿属性进行了自动化验证.结果表明所提方法能够有效应用于SoC的验证.
其他文献
由于足球运动训练强度和对抗性的增加,导致运动员受伤情况日益增多,尤其以踝关节损伤为主。本文主要针对足球运动员踝关节损伤的原因及预防措施展开了探讨,对足球运动员踝关节的
青少年学生拥有健康的身体条件是保障学习和生活的基础,也是一个民族旺盛生命力的体现和社会进步的体现。随着经济的发展和人民生活水平的提高,学生的健康水平有了一定的改善,但
“跳上成支撑--前翻下”是小学中高年级的单杠的教学内容,对于发展学生上肢、胸背和腰腹肌力量以及身体协调性具有显著的作用。由于教学内容对学生的身体能力有一定的要求,使学
小学生的业余排球训练中必须要因材施教、有张有弛,针对小学生特殊的身体素质属性特点,同时根据当前对排球训练的大纲要求制定科学而有效的训练方法,培养学生建立良好的团队协作
目的探索ISO(国际标准组织简称)体系中医院质量目标的建立、考核和效果评价,提高医院执行力,规范和强化医院管理。方法以ISO理论为框架,借助医院ISO认证,依据卫生行政管理法
The article mainly introduced the character of antimicrobial Natamycin, the preservative mechanism, the application in meat products was reviewed and the develo
目的分析本院11年间2个时段急性心肌梗死死亡患者的临床诊疗方法及死亡原因,为进一步降低急性心肌梗死病死率提供客观临床依据。方法对我院心内科1997-2000年199例急性心肌梗
吡咯喹啉醌(PQQ)是继烟酰胺和黄素核苷酸之后发现的氧化还原酶的第3种辅酶,具有多种生理功能,在食品、医药及农业等行业有广泛的应用前景.我们简要综述了PQQ参与醌酶电子传递
为了提高智能赛车的性能,需要得到赛车运行中的相关参数.本文以nRF2401无线数传芯片为核心,以HCS12DG128控制发射,以AT89C2051控制接收,采用MAX232将数据发送给计算机,在计算
近年来,微通道经皮肾穿刺术(MPCN)的应用日益广泛,一般采用俯卧位进行手术,这种体位对患者的呼吸循环系统影响较大,容易造成患者感觉非常不适,长时间手术不易耐受,而且给麻醉