文档介绍：CMP中Cache一致性协议的验证        李崇民1,王海2,李兆麟3时间:2008年07月24日    字体:大中小        关键词:<"cblue""rch/?q=验证方法"target='_blank'>验证方法<"cblue""rch/?q=有限状态机"target='_blank'>有限状态机<"cblue""rch/?q=系统模型"target='_blank'>系统模型<"cblue""rch/?q=三种"target='_blank'>三种<"cblue""rch/?q=系统级"target='_blank'>系统级             摘要:CMP是处理器体系结构发展的一个重要方向,其中Cache一致性问题的验证是CMP设计中的一项重要课题。基于MESI一致性协议,本文建立了CMP的Cache一致性协议的验证模型,总结了<"cblue""rch/?q=三种"title="三种">三种<"cblue""rch/?q=验证方法"title="验证方法">验证方法——状态列举法、模型检验法和符号状态法,并给出了每一种方法的复杂性分析。关键词:CMPCache一致性状态列举模型检验符号状态模型集成电路工艺的发展使得芯片的集成度不断提高,一种新型体系结构——CMP(ChipMultiprocessor——片上多处理器)应运而生,通过在一个芯片上集成多个微处理器核心来提高程序的并行性。多个微处理器核心可以并行地执行程序代码,具有较高的线程级并行。由于CMP采用了相对简单的单线程微处理器作为处理器核心,使得CMP具有高主频、设计和验证周期短、控制逻辑简单、扩展性好、易于实现、功耗低、子通信延迟低等优点。此外,CMP还能充分利用不同应用的指令级并行和线程级并行,成为处理器体系结构发展的一个主要趋势。在CMP中,多个处理器核心对单一内存空间的共享使得处理器和主存储器之间的速度差距的矛盾更加突出,因此CMP设计必须采用多级高速缓存Cache,通过层次化的存储结构来缓解这一矛盾。图1给出了共享内存的CMP<"cblue""rch/?q=系统模型"title="系统模型">系统模型。与常规SMP系统类似,CMP系统必须解决由此而引发的Cache一致性问题以及一致性验证问题。采用什么样的Cache一致性模型与它的验证方法都将对CMP的整体设计与开发产生重要影响。从CMP中Cache一致性协议的验证技术的发展来看,目前应用比较广的验证方法有状态列举法[1]、模型检验法[2][3]、符号状态模型法[4]三种。本文结合CMP的特点,建立了基于MESI一致性协议的CMP验证模型,并在此模型基础上分析了这三种验证方法的基本原理,每一种方法的复杂性分析及优缺点。1Cache一致性协议的建模从本质上看Cache一致性协议是由一些过程组成的,这些过程包括Cache与内存控制器之间交换信息以及对处理器事件做出的反应。因此用<"cblue""rch/?q=有限状态机"title="有限状态机">有限状态机模型来描述Cache一致性协议是一件很自然的事情。Cache一致性协议可以在三种不同的层次上建立验证建模。最高层次是对整个协议行为的抽象,中间层次是在系统/消息传递一级进行抽象,最低层次则是在结构模型一级进行抽象,表1给出了这三个层次的抽象模型的特点[5]。目前