（计算机科学与技术专业论文）ccnuma系统中cache一致性协议模拟验证方法研究.pdf

国防科学技术大学研究生院硕士学位论文 摘要 c a c h e 一致性协议作为c c - n u m a ( c a c h ec o h e r e n c yn o n u n i f o 咖m e m o r y a c c e s s ) 系统的硬件基础，在系统设计过程中占有举足轻重的地位。大规模的 c c - n u m a 系统往往采用复杂的多层c a c h e 致性协议，通常难以对这种复杂协 议进行完全形式化验证，因此软件模拟验证仍然在大规模c c - n u m a 系统的c a c h e 一致性协议验证中扮演着重要角色。 本文针对某型c c n u m a 系统，重点研究了对其c a c h e 一致性协议进行模拟 验证的问题。设计了一套覆盖率驱动的高效c a c h e 一致性协议模拟验证方法，并 使用s y s t e m c 实现了验证系统。本文的主要工作和贡献如下： 1 在分析目标系统协议表的基础上设计了一套覆盖率驱动的c a c h e 一致性协 议伪随机模拟验证方法； 2 使用s y s t e m c 语言实现了全系统模拟器。在此基础上，为了加速模拟器执 行，针对验证目标系统的特点，提出了一种基于m p i 并行函数库的s y s t e m c 模拟应用分布式并行化方法，并基于此方法设计实现了一个支持模拟验证 系统并行执行的分布式并行系统模拟器； 3 基于朴素贝叶斯方法提出了一种用于测试激励自动生成的有效测试激励分 类算法。使用此算法设计并实现了一个有效测试激励分类器，并将其应用 到验证系统中。该分类器将随机产生的测试激励中不具有运行价值的无效 测试激励滤除，提高了测试激励的产生效率； 4 基于相关分析提出了一种用于测试激励自动生成的验证结果快速扩展算 法。使用此算法设计并实现了一个验证结果扩展器，并将其应用到验证系 统中。该验证结果扩展器对已运行过的测试激励施加偏置，通过运行带偏 置的测试激励，快速覆盖已被覆盖验证目标的相似项目。 基于上述研究成果建立的完整高效率c a c h e 一致性协议验证系统已经成功的 应用于某型c c n u m a 系统的c a c h e 一致性协议验证工作中，应用结果表明了本 文方法的有效性。 主题词：c a c h e 一致性协议；功能验证；s y s t e m c ；m p i ；机器学习；测试 激励自动生成 第i 页 国防科学技术大学研究生院硕士学位论文 a b s t r a c t a st h eh a r d w a r ef o u n d a t i o no ft h ec c n u m a ( c a c h ec o h e r e n c yn o n u n i f o r m m e m o r ya c c e s s ) s y s t e m ，c a c h ec o h e r e n c ep r o t o c o lp l a y sav i t a lr o l ei n t h es y s t e m d e s i g np r o c e s s l a r g e s c a l e c c j n u m as y s t e m sa r eo f t e nt h eu s eo fc o m p l e x m u l t i 1 a y e r e dc a c h ec o h e r e n c ep r o t o c o l ；i ti sd i f f i c u l tt op e r f o r mf o r m a lv e r i f i c a t i o nt o t h ec a c h ec o h e r e n c ep r o t o c o lb e c a u s eo fi t sg r e a tc o m p l e x i t y ，a n dt h et r a d i t i o n a l p s e u d o r a n d o ms i m u l a t i o nv e r i f i c a t i o ns t i l lp l a yi m p o r t a n tr o l ei nc c n u m as y s t e m v e r i t i c a t i o n i nt h i sp a p e r ，w ef o c u so nt h ec a c h ec o h e r e n c ep r o t o c o lv e r i f i c a t i o nm e t h o d so fa c e r t a i nt y p ec c - n u m as y s t e m s ah i g he f f i c i e n ts y s t e m ss i m u l a t o rb a s e do ns y s t e m c s i m u l a t o rh a sb e e nd e s i g n e da n di m p l e m e n t e d t h em a i nw o r ka n dc o n t r i b u t i o no ft h i s p a p e ri sa sf o l l o w s ： 1 as e to fc o v e r a g e - d r i v e np s e u d o r a n d o ms i m u l a t i o nc a c h ec o h e r e n c ep r o t o c o l v e r i f i c a t i o nm e t h o dh a sb e e nd e s i g n e db a s e do nt h ea n a l y s i so ft h et a r g e ts y s t e m p r o t o c o lt a b l e 2 u s i n gt h es y s t e m cl a n g u a g et oi m p l e m e n tf u l l - s y s t e ms i m u l a t o r a n db a s e do n i t ，ap a r a l l e lm p i b a s e dl i b r a r yo fs y s t e m cs i m u l a t i o no fad i s t r i b u t e dp a r a l l e l a p p l i c a t i o nm e t h o dh a sb e e np r o p o s e df o rs p e e du pt h ee x e c u t i o n o ft h e s i m u l a t o r av e r i f i c a t i o ns y s t e mw h i c hs u p p o r td i s t r i b u t e dp a r a l l e le x e c u t i o nh a s b e e nd e s i g n e da n di m p l e m e n t e db a s e do nt h i sm e t h o d 3 at e s ts t i m u l u sa u t o m a t i c a l l yg e n e r a t e dc l a s s i f i c a t i o na l g o r i t h mb a s e do nn a i v e b a y e s i a nc l a s s i f i e r sh a sb e e np r e s e n t e d ，at e s ts t i m u l u sc l a s s i f i e rb a s e do ni th a s b e e nd e s i g na n di m p l e m e n t t h ec l a s s i f i e rs c r e e no u tt h eh i g hv a l u eo fr u n i n c e n t i v ef r o mt h ep s e u d o r a n d o mg e n e r a t e dv e r i f i c a t i o ns t i m u l u st oi m p r o v et h e g e n e r a t ee f f i c i e n c yo f t h e m 4 b a s e do nc o r r e l a t i o na n a l y s i sp r e s e n t sar a p i de x p a n s i o na l g o r i t h mf o rt e s t i n g r e s u l t s at e s tr e s u l t se x p a n d e rb a s e do ni th a sb e e nd e s i g na n di m p l e m e n t i t a p p l i e sb i a st ot h er u n o f fv e r i f i c a t i o ns t i m u l u s ；m a k eaf a s tc o v e rt h er e s u l t so f s i m i l a rp r o j e c t sh a v e b e e nc o v e r e db yr u n n i n gt h eb i a s e dv e r i f i c a t i o ns t i m u l u s b a s e do nt h ea b o v er e s e a r c h ，ah i g h e f f i c i e n c yv e r i f i c a t i o ns y s t e mh a sb e e n s u c c e s s f u l l ye s t a b l i s h e da n da p p l i e dt o t h ev e r i f i c a t i o nw o r ko fac e r t a i nt y p eo f c o m p l e xc c - n u m as y s t e m ；t h ea p p l i c a t i o nr e s u l t ss h o wt h ee f f e c t i v e n e s s o ft h i s m e t h o d k e yw o r d s - c a c h ec o h e r e n c ep r o t o c o l ；f u n c t i o nv e r i f i c a t i o n ；s y s t e m c ；m p i ； m a c h i n el e a r n i n g ；a u t ot e s ts t i m u l a t i o ng e n e r a t i o n ； 第i i 页 国防科学技术大学研究生院硕士学位论文 表目录 表2 1协议表示例1 4 表3 1状态寄存器编码方法2 1 表4 1 m p i 的一些主要实现2 8 表4 2并行模拟器与串行模拟器执行时间对照表3 4 表5 1朴素贝叶斯方法求得的概率分布表3 9 第1i i 页 国防科学技术大学研究生院硕士学位论文 图目录 图1 1c c - n u m a 系统结构示意图1 图1 2验证目标系统结构示意图2 图1 3双环路的覆盖率驱动验证流程【酬4 图1 4在c + + 开发环境中的s y s t e m c l l 7 1 6 图2 1无冲突的簇内访存1 2 图2 2无冲突的簇间访存1 2 图2 3有冲突的访存1 3 图2 4改进后的验证系统工作流程1 8 图3 1基本模拟器结构框图。1 9 图3 2网络模拟器结构2 3 图3 3 伪随机模拟覆盖率随时间增长曲线一2 4 图4 1并行化的全系统模拟器3 0 图4 2m p i 交换核心结构示意图3 1 图4 3m p i 接口存根示意图3 2 图4 4并行模拟器启动同步流程3 3 图4 5并行化后的系统模拟器对协议表的覆盖率随时间增长曲线3 4 图5 1分段机器学习流程图4 0 图5 2使用机器学习分类器后覆盖率随时间增长曲线。4 1 图6 1应用测试激励扩展器后覆盖率随时间增长曲线4 5 第1 v 页 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：丝型唑! 盖选主丛二丛垒盟：堕塑叁墨童坠鸳塞 学位论文作者签名： 歪叁 日期： z 吵年，五月岁。日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：c a - l a 帅主；毛呻厶如一蔹娃玮眦彳叹旌坯君砧研之 学位论文作者签名：丕盘 日期： 2 。吵年，乇月，。日 储擀刻嗍：一嗍： z 。夕年，2 月3 0 日 国防科学技术大学研究生院硕士学位论文 第一章绪论弟一早硒记 1 1 研究背景 c a c h e 一致的非均匀存储器访问( c a c h ec o h e r e n c yn o n u n i f o r mm e m o r y a c c e s s ，以下简称c c n u m a ) 是目前应用于大规模并行计算机设计中的一种重要 系统结构，图1 1 给出了一个简单的c c n u m a 系统示意图。 、厂、 p r o c e s s o rip r o c e s s o rjp r o c e s s o r + c a c h ej j + c a c h e + c a c h e p r o c e s s o rjjp r o c e s s o r ；p r o c e s s o r + c a c h e+ c a c b e+ c a c h e j 7、 图1 1c c - n u m a 系统结构不意图 在c c n u m a 系统中，分布于各个结点上内存全局统一编址，结点之间通过 互连网络相连，各结点的c p u 通过互连网络可以透明的访问全局内存，因为访问 不同节点上的内存所需时间不同，因此被称为“非均匀的”。在这种全局统一编址的 情况下，为了保证的全局c a c h e 一致性，需要在互连网络上运行由硬件维护的全 局c a c h e 一致性协议。对于c c n u m a 系统，此种由硬件维护的全局c a c h e 一致 性协议是其重要组成部分和硬件基础，因此对c a c h e 一致性协议的验证工作也成 为c c - n u m a 系统设计验证工作中的重要组成部分。 单芯片多处理器( s i n g l e c h i pm u l t i p r o c e s s o r ，以下简称c m p ) 或称多核微处理 器( m u l t i c o r em i c r o p r o c e s s o r s ) 是上世纪9 0 年代以来集成电路制造工艺的进步与 微处理器体系结构的发展所带来的微处理器发展必然方向，是目前解决频率墙、 功耗墙等问题的最优方法。在普遍使用商用微处理器构建大规模并行计算机的潮 流下，使用高性能商用多核微处理器构建c c n u m a 系统也成为一种必然的趋势， 此种使用大量c m p 构造的多层复杂c c n u m a 系统也被称为m u l t i c m p 系纠2 1 。 为了支持多处理器并行，目前的高端商用微处理器基本都支持多路直连扩展，在 第1 页 国防科学技术大学研究生院硕士学位论文 直连扩展的条件下，若处理器使用内置的存控并对全局访存空1 2 j 统一编址，则多 个直连的处理器即可构成一个小型的c c - n u m a 系统。然而受处理器直连接口数 量限制，仅使用处理器直连方式难以构建大型系统，为了构建更大规模的 c c - n u m a 系统，通常需要在处理器直连的基础上做进一步扩展，此种情况下， 需要在处理器直连c a c h e 一致性协议的基础上扩展建立多层次的协议。如今，多 层的m u l t i c m p 系统已经逐渐成为构造大规模并行计算机的重要系统结构之一。 而为了能在大量的处理器之间保持c a c h e 一致性，在多层m u l t i c m p 系统中，多 层c a c h e 一致性协议往往相当复杂。 本课题的主要工作为验证某型基于c m p 直连扩展构建成的复杂多层 c c - n u m a 系统的c a c h e 一致性协议。该系统简要结构如图1 2 所示： i n t e r c o n n e c t i o nn e t w o r k jlj lj l r t bb r i d r t hb r t a l p n m t h 阶i d p r彳广 1 r ，殳 芷，二乙 l 一l c 辩“ c 扯h c k “h c 耻k l c 毒刽遽刽l ! 递剑 ；i i h o r ti i m r y 啕剑也竺! 二l “t 掣- 叫 j l 一 jljl i l e 劬r ?1 1 1 o r y ： 自m _ t i g ； “ 矛 c 时h c 牡k 子 l 一。 c 越h 子 c 扯k 一_ | ! 【，一 ! ； i 。l l “。o r 。y ，i l 。1 1 2 。m ，o 。r 。v 。，l剧l 。篡搿。l l 。“t r o ”l l 。，l i 。n e 。s ，。o r 。y 。j j i ， j l j 1 j 【 j i i ， c l u m po i b m d r ? i - _ o r ， l l r y e 时t l i t s o t ? c l u m pl c i u m pn 图i 2 验证目标系统结构示意图 该系统由多个簇( c l u m p ) 构成，全系统访存空间全局统一编址。在每个簇中 安装有若干多核微处理器与一个北桥芯片，处理器采用了内置存控的设计，簇内 部各处理器和北桥芯片通过高速内部互连网络直连，而簇间由北桥芯片通过一个 全交换的高速互连网络进行连接。系统使用两层c a c h e 一致性协议一一在簇内， 北桥芯片和其它处理器共同构成了一个小型的c c n u m a 系统，使用处理器直连 c a c h e 一致性协议；在簇间，北桥芯片使用扩展的c a c h e 一致性协议。我们的验证 目标即为此扩展的c a c h e 一致性协议。 该系统中两层协议均为基于目录的c a c h e 一致性协议，各自拥有独立的目录 表用于保存内存的一致性状态。为了简化互连网络设计，簇内和簇间的互连网络 均采用不保序设计，即系统采用完全乱序的c a c h e 一致性协议，这导致整个协议 体系十分复杂。其中，原处理器直连的c a c h e 一致性协议包含了超过1 0 0 种消息 类型和近1 0 0 0 条的协议表条目；而基于北桥芯片的扩展c a c h e 一致性协议中使用 第2 页 国防科学技术大学研究生院硕士学位论文 了超过1 5 0 种消息类型和超过4 0 个状态寄存器，协议表条目超过了1 4 0 0 项。如 此复杂的协议给验证工作带来了巨大的挑战。 目前针对c a c h e 一致性协议的验证方法主要包括形式化验证和软件模拟验证 两种【3 】【4 1 。然而由于固有的状态爆炸问题，完全形式化的验证目前还难以应用到复 杂c a c h e 一致性协议的验证工作中；而对于软件模拟验证，传统的伪随机验证则 存在验证效率低下的问题，尤其通过人工方式撰写约束模型，效率低下且难以覆 盖到所有边界条件，所以高速、全面的模拟验证仍然难以实现【5 1 。 针对目标系统c a c h e 一致性协议所具有的特点，我们设计了一套覆盖率驱动 的伪随机软件模拟验证方法。我们使用s y s t e m c 语言构建了基本的软件模拟验证 环境；在其基础上我们针对模拟目标系统的特点提出了一种基于m p i 并行库的分 布式并行化方法，并使用该方法设计实现了一个并行的系统模拟器，大幅度提高 了模拟系统执行效率；在对验证结果的覆盖率测度基础上，我们基于朴素贝叶斯 方法提出了一种有效测试激励分类算法，提高了有效测试激励的生成效率；我们 基于相关分析的思想提出了一种验证结果快速扩展算法，加速了对协议表中近似 条目的验证覆盖。 1 2 1 覆盖率驱动的验证方法学 1 2 相关研究 使用模拟验证的方法来进行功能验证，核心思想是将设计者的意图与观察到 的模拟器实际行为进行比较，以确定它们的一致性。当一个设计在模拟中能够像 设计者所期望的那样运行并且达到设计要求的时候，我们认为这个设计就已经被 验证了。通常情况下，验证一个设计需要回答两个基本问题：一个是被测设计 ( d e s i g nu n d e rt e s t ，以下简称d u t ) 的功能是否正确? 即我们的设计是否符合参 考模型；另一个是d u t 被充分测试了么? 即我们是否已经回答了足够多的第一 类问题【6 1 。 如何较好的回答以上两个问题是能否建立一个优秀的验证方法学的关键，而 以覆盖率为驱动的验证方法学较好的解决了这个问题。覆盖率驱动的验证方法从 带有约束的伪随机测试激励自动产生方法发展而来的，结合了形式化验证和模拟 验证的优势，在验证过程中，通过对己产生的测试激励模拟结果覆盖率的分析， 结合由系统功能描述中导出的信息，改进进一步验证的测试激励生成算法或者测 试激励生成约束，使得再次生成的测试激励能使模拟系统达到更高的覆盖率。 图1 3 展示了一个简单的以覆盖率为驱动的双环路验证工作流程： 第3 页 国防科学技术大学研究生院硕士学位论文 d e s i g n s p e ci f i c a t i o n i i o n e 、 图1 3双环路的覆盖率驱动验证流程【6 】 在此过程中，模拟验证不断被进行，如果发现有违背设计参考的验证模拟结 果出现，则修改模拟实现，并再次投入模拟；如果没有违背设计参考的模拟出现， 则分析是否已经达成了目标覆盖率，如果未达成，则修改测试激励，并再次投入 模拟；如果已经达成目标覆盖率，则验证工作完成。 覆盖率驱动验证方法的核心技术是覆盖率测度报告与测试激励自动生成【4 1 。 覆盖率测度和报告方法一般分为以下几种【7 】： 基于代码覆盖率的测度，使用类似软件验证的方法对h d l 代码进行分析， 使用如分支覆盖率，表达式覆盖率和路径覆盖率等方法进行分析。但是由 于h d l 代码的并发工作特性，同时可能有多段代码处于工作状态，所以此 种串行化的覆盖率测度是比较低的要求。 基于电路结构覆盖率的测度：此种测度又被称为跳变覆盖率( t o g g l e c o v e r a g e ) ，要求电路中的每个二元结点在整个模拟过程中必须完成从o 到 l 或者1 到0 的一次跳变。 基于有限状态机( f s m ) 覆盖率的测度：使用f s m 来描述硬件系统是最自 然的方式，因此可以使用基于f s m 的覆盖率测度指标。基于f s m 的覆盖 率测度要求在模拟中覆盖到每个可达状态，经过每条状态迁移，或者覆盖 到一定长度的状态转换路径。 基于功能覆盖率的测度：此种覆盖率测度多用于系统级验证，验证中要求 覆盖到系统中所有功能。 第4 页 国防科学技术大学研究生院硕士学位论文 此外，在近期的文献中还有报道将熵理论应用到覆盖率测度的方法【引。上述这 些测度方法没有很好的可比性，而且在不同的验证阶段，不同的验证领域所能使 用的覆盖率测度方式也不尽相同，因此也有采用多种覆盖率测度的组合来提高可 信度。 测试激励自动生成技术经历了长期的发展，已经形成了多种方法，主要包括： 基于状态机模型的生成方法，从描述系统的有限状态机出发，通过遍历所 有可达状态来生成模拟矢量，一般以基于有限状态机的覆盖率测度为指导 软件测试数据生成方法，直接通过对r t l 级的h d l 代码分析，借鉴软件 测试技术中生成测试激励的方法来生成模拟矢量，常常以代码覆盖率测度 为指导。 系统级生成方法，主要包括基于系统描述的方法，基于事务的方法，基于 事件的方法等，此类方法一般站在比r t l 级描述更高层次的级别，主要关 注系统的行为功能，如指令集，体系结构状态等。 早期，还常常使用人工方式描述激励产生的条件约束，如i b m 的m p t g ( m u l t i p r o c e s s o rt e s tg e n e r a t o r ) 系统【9 】。后期逐渐有人工智能方法被应用到测试 激励自动生成中，如i b mh a i f a 研究所的g e n e s y sm b t g ( m o d e lb a s e dt e s t g e n e r a t o r ) 系统【l o l ，使用了专家系统技术；近年来基于机器学习的入工智能技术 也有被应用到功能验证中的，如使用人工神经网络技术【1 1 】的，以及使用遗传算法【1 2 】 的。一般使用机器学习的思路都是将机器学习应用到对测试激励自动生成的约束 上，如上述使用神经网络的应用中，首先定义测试激励在覆盖率空间上的距离概 念，每次模拟后将已有的覆盖率统计数据加入到神经网络训练集中，训练神经网 络算法，使之可以筛选出相对己被模拟的激励部分最远的测试激励，以此来快速 提高覆盖率。 目前有很多e d a 公司和机构在从事此方面进行研究并推出了相应的产品，如 美国的m e n t o rg r a p h i c s 公司的t h em e n t o rf u n c t i o n a lv e r i f i c a t i o np l a t f o r m 1 3 】； c a d e n c ed e s i g ns y s t e m s 公司的i n c i s i v ef u n c t i o n a lv e r i f i c a t i o np l a t f o r m 1 4 l ；s y n o p s y s 公司的d i s c o v e r yv e r i f i c a t i o np l a t f o r m 巧1 ；o b s i d i a ns o f t w a r e 公司的r a v e n v e r i f i c a t i o ns o f t w a r e 1 6 】等。而n u s y mt e c h n o l o g y ，i n c 公司则专门为智能验证建立了 产品线等。在历年的d a t e 和d a c 会议中，也都为验证方面的问题建立了专题。 第5 页 国防科学技术大学研究生院硕士学位论文 1 2 2s y s t e m g 及其分布式并行化研究 s y s t e m c 是用c + + 语言编写的一组宏和运行库，通过在c + + 语言上添加硬件 建模的能力，s y s t e m c 扩展了c + + 语言，使之可以用来对硬件系统进行描述和建模， 同时，s y s t e m c 还提供了一个仿真内核，使得用户可以对自己编写和描述的建模系 统进行仿真【l7 。它是为了提高电子系统设计效率而逐渐发展起来的产物，许多科 学研究团队和计算机辅助设计软件公司一同为s y s t e m c 的发展做出了贡献， s y s t e m c 的开源开发团队“o p e ns y s t e m ci n i t i a t i v e ( o s c i ) 与1 9 9 9 年成立【1 8 】， s y s t e m c 近年来越来越多的被应用于各种硬件设计工作中。图1 4 展示了一个在 c + + 开发环境中使用的s y s t e m c 进行开发的流程。 图1 4 在c + + 开发环境中的s y s t e m c 【1 7 】 一般来说，早期计算机系统的软硬件划分十分明显，软件工程师使用c 和c 抖 等程序设计语言；硬件工程师使用v h d l 和v e r i l o g 等硬件描述语言，软硬件分别 进行设计、仿真、实现和改进，最后将软件部分和硬件部分结合起来形成完整系 统。但是，随着电子系统的不断发展，系统结构越来越复杂，在先期进行软硬件 划分时，必须对对整个系统性能有很好的了解和掌握，以便更好地划分软件和硬 件，从而减小设计中不必要的失误所带来的损失和风险。s y s t e m c 即在此环境下被 开发出来l l 圳。s y s t e m c 语言的发展大致经历了两个大的阶段：s y s t e m c1 o 可以用 来进行硬件描述；s y s t e m c2 0 的推出使s y s t e m c 成为真正的系统级设计语言，能 够用来对s o c 体系结构进行更加自然和有效的描述。由于s y s t e m c 是基于c + + 语 第6 页 国防科学技术大学研究生院硕士学位论文 言编写的，其模拟仿真内核完全采用c 十+ 设计与实现，所以s y s t e m c 能完全兼容 使用标准c + + 编写的各种模块，可以很方便的进行从算法层次的模型到寄存器传 输级层次模型的开发。这样s y s t e m c 被大量应用在对系统进行快速建模和性能分 析上。目前，s y s t e m c 除了可以建立时钟周期精确的模型以外，还对以下三个种描 述提供了方法学上的支持： 系统级设计； 软件算法； 硬件架构。 这样就使s y s t e m c 语言涵盖了从系统概念直到实现的针对系统软、硬件建模 的能力。 使用s y s t e m c 建模虽然较之使用纯粹的硬件描述语言模拟运行效率要高，但 是不断增长的硬件复杂性使得对建模进行模拟仿真所需消耗的资源越来越大，甚 至于超过了单一处理器所能接受的极限，因此，对于s y s t e m c 的并行化分布式仿 真运行也成为了一种必然的需求。 目前对s y s t e m c 的分布式改造主要包含以下两种途径： 使用并行离散事件仿真( p a r a l l e ld i s c r e t ee v e n ts i m u l a t i o n ) 修改s y s t e m c 的模拟内核，使整个s y s t e m c 的模拟仿真环境并行化。如b c h o p a r d l 2 0 1 在 公开的s y s t e m c 版本基础上建立了一个并行化的s y s t e m c 模拟核心的原型； 使用自己开发的通信库封装系统的逻辑部件间的通信，即扩展s y s t e m c 的 通信库，以此达到并行的目的。如v g a l i a n o 2 1 】使用m p i 扩展了s y s t e m c 的通信协议。 1 2 3 机器学习方法在模拟验证中的应用 机器学习( m a c h i n el e a r n i n g ) 是继专家系统后人工智能应用的又一重要研究 领域，也是人工智能和神经计算的核心研究课题之一。虽然目前缺乏对机器学习 的公认和准确的定义，但是一般来说，机器学习指研究如何使用机器来模拟人类 学习活动的一门学科。或者更为严格的提法是：机器学习是一门研究机器获取新 知识和新技能，并识别现有知识的学问【2 2 】。 机器学习背后的思想是感知不仅应该对进行中的行动有用，而且应该能够改 进智能体未来的行动能力。机器学习一般分为三种类型【2 3 】： 第7 页 国防科学技术大学研究生院硕士学位论文 有监督学习，此种学习方法涉及从问题的输入和输出的实例中学习出一个 函数。对于完全可观测的环境，智能体总能够观察到他的行动所带来的影 响，因此可以采用监督学习的方法来学习预测他们。 无监督学习，此种学习方法涉及在未提供明确的输出值的情况下，学习输 入的模式。纯粹的无监督学习智能体无法学习要做什么，因为它没有信息 说明什么能构成正确的行动或者所期望的状态。因此一般主要在概率推理 系统的上下文中研究无监督学习。本文使用的基于朴素贝叶斯模型的机器 方法即为无监督学习的一种，关于朴素贝叶斯方法的将在第五章中进行具 体的描述。 强化学习，是三类学习问题中最普遍的一个，此种学习方法是从强化物( 起 加强作用的事物) 中进行学习，而不是根据训练说的应该做什么进行学习。 典型的强化学习包括学习环境是如何运转的。 机器学习方法在很多应用领域都被证明是很有实用价值的。目前一般认为机 器学习在以下一些方面特别有用【2 3 】： 数据挖掘问题，即从大量数据中发现可能包含在其中的有价值的规律。 在某些困难的领域中，人们可能还不具有开发出高效算法所需的知识。 计算机程序必须动态地适应变化的领域。 此外，本课题的主要研究方向一一功能验证( f u n c t i o n a lv e r i f i c a t i o n ) 问题是 一个复杂的问题，与软件验证问题等价，这已被公认是一个n p 难( n p h a r d ) 问 题【2 4 】，因此如在1 2 1 节中所列举的那样，人工智能方法已经在硬件系统的功能验 证方面得到了广泛的应用，近年来将机器学习方法应用到功能验证方面已经成为 了一个热门的研究领域。 1 3 本文的主要工作 为了完成本课题的验证任务，我们详细研究了目标协议表，并对协议表进行 了数学分析，基于分析的结果，我们以覆盖率驱动模拟验证方法为基本思想设计 了一套完整的验证方案，本文的主要工作如下： 使用s y s t e m c 语言设计并实现了全系统模拟器。在此基础上，为了加速模 拟器执行，我们基于m p i 并行函数库，针对验证目标系统的特点，提出了 一种s y s t e m c 模拟应用分布式并行化方法，并基于此方法设计实现了一个 支持模拟验证系统并行执行的分布式并行系统模拟器，使得模拟验证系统 可以在多处理器或多机环境中以较高的效率分布式并行执行； 第8 页 国防科学技术大学研究生院硕士学位论文 测试激励自动产生方面，我们在对协议表进行数学分析的基础上，基于朴 素贝叶斯方法提出了一种有效测试激励分类算法，并使用此算法设计实现 了一个测试激励分类器。在模拟器运行过程中，根据目标覆盖率的变化对 随机产生的测试激励进行分类，遴选出具有较高概率使模拟器覆盖到新目 标的测试激励作为有效测试激励，并予以执行，提高了有效测试激励的产 生效率； 为了进一步提高测试激励自动产生的效率，我们基于相关分析的思想提出 了一种验证结果快速扩展算法，并使用此算法设计实现了一个验证覆盖结 果扩展器。通过对已经被模拟器覆盖到验证结果进行扩展，使得当有较小 概率协议表项被覆盖时，与其相似的小概率协议表项能够被迅速扩展覆盖 到。 我们使用实现后的模拟验证系统对目标协议表进行了大量的模拟验证工 作，在验证过程中发现了三处协议表设计过程中的失误；我们以纯粹伪随 机模拟验证系统作为参考，对比研究了我们的验证系统的验证效率，对比 结果表明：覆盖率驱动的验证系统对于加快覆盖率增长速率，缩短模拟验 证时间有明显的效果。 本文的工作对于c a c h e 一致性协议模拟验证研究领域具有实践意义和研究参 考价值，并已经被应用在某型复杂c c - n u m a 系统的c a c h e 一致性协议的实际验 证工作中。 1 4 论文结构 全文共分七章 第一章概述课题背景、研究现状及本文的主要工作，并给出了本文的结构框 架。 第二章详细描述了模拟验证目标协议表，对验证协议表进行了数学分析，并 在分析的基础上提出了模拟验证系统的总体设计思路。 第三章描述了系统模拟器的具体编码设计与实现，并分析介绍了使用纯伪随 机测试激励发生器作为测试输入的验证测试结果。 第四章针对目标系统的特点提出了一种有针对性的基于m p i 并行库的 s y s t e m c 模拟应用分布式并行化方法，介绍了应用此方法设计的分布式并行系统模 拟器的具体设计与实现工作；给出了使用并行系统模拟器后，模拟验证系统进行 验证的测试结果及其分析。 第9 页 国防科学技术大学研究生院硕士学位论文 第五章提出了一种基于贝叶斯方法的有效测试激励分类算法，并介绍了应用 在此算法的有效测试激励分类器的具体设计与实现工作；给出了应用该分类器后， 使用模拟验证系统进行验证的测试结果及其分析。 第六章提出了一种基于相关分析的验证结果快速扩展算法，并介绍了应用此 算法的验证结果扩展器的具体设计与实现工作；给出了应用此扩展器后，使用模 拟验证系统进行验证的测试结果及其分析。 第七章总结全文并展望未来的工作。 1 5 本章小结 本章首先对复杂c c 小m a 系统中的c a c h e 一致性协议验证工作进行了介绍； 并概述了本文工作目前面临的主要问题和挑战，介绍了目前在本文工作所涉及的 相关领域已有的研究工作；而后介绍了本文所做的主要工作和成果，最后给出了 本文的结构框架。 第1 0 页 国防科学技术大学研究生院硕士学位论文 第二章模拟验证系统总体设计 在对目标系统的c a c h e 一致性协议进行模拟验证的过程中，设计套完整的 伪随机模拟验证方案是整个工作的基础。本章详细分析了验证目标系统的c a c h e 一致性协议，并在分析该协议的基础上提出了整个模拟验证系统的总体设计思想 和设计方案。 2 1 目标系统的c a c h e 一致性协议、 如在第1 1 节中所述，验证的目标系统包含有两层基于目录的乱序c a c h e 一致 性协议：在簇内，使用处理器直连c a c h e 一致性协议连接各处理器和北桥芯片； 在簇间，使用扩展的c a c h e 一致性协议连接各簇的北桥芯片。 在该协议体系中，访存“事务”是最小的可管理访存单位，每个完整的访存 操作称为一个访存事务，访存事务从c a c h e 发出一条访存请求消息开始，以c a c h e 收到特定的完成消息结束。在访存过程中，当访存目标地址与c a c h e 在同一簇内 时，访存事务由处理器直连c a c h e 一致性协议处理；当访存目标地址与c a c h e 不 在同一簇内时，访存事务在处理器直连c a c h e 一致性协议处理的基础上须通过北 桥芯片翻译为扩展的c a c h e 一致性协议在簇间转发。 为了实现高效的访存请求处理，北桥芯片并非直接简单翻译转发直连c a c h e 一致性消息，而是在翻译转发的基础上，增加了自己的目录表。该目录表中存储 了本簇内每块存储区在其他簇中被c a c h e 缓存的副本情况，当有远程访存请求到 达时，如果该请求对远程副本有失效要求，则北桥芯片会首先查询自己的目录， 如果发现对应的存储区在其他簇内有副本，北桥芯片将会首先根据访存事务的类 型对其他拥有副本的簇发广播相应的失效消息，收到其他各簇返回的全部响应消 息后，再将访存请求发向本簇内访存地址对应的存控。 在实际的访存过程中，多个访存事务常常可能并发的产生，这些并发的访存 事务可能发生在同一个簇中，也可能发生在不同的簇之间。同时由于互连网络的 无序性，即使不存在并发的访存事务在运行时间上也可能存在交叠，当有访问同 一个地址的不同访存事务在运行时间上发生交叠时，即有可能产生冲突。而由于 使用了优化的扩展c a c h e 一致性协议，系统中两层协议均存在发生冲突的可能性， 冲突有可能发生在不同层次的协议中，甚至也可能同时发生在两个层次中，实际 的冲突情况可能及其复杂。 下面分别介绍几种有代表性的访存事务或事务组的流程： 第11 页 国防科学技术大学研究生院硕士学位论文 无冲突的簇内访存： 在这种访存事务中，c a c h e 发出的读或写请求消息直接到达本簇内对应的存 控，存控立即处理该请求并给出响应，图2 1 给出了此种访存事务的流程示意图。 m e r r o r l ； cach。c o n t r o l l e r 。 图2 1 无冲突的簇内访存 无冲突的簇间访存： 在此种访存事务中，c a c h e 发出的读或写请求消息先到达本簇的北桥芯片，由 北桥芯片将访存消息翻译为扩展的访存协议消息发送到目标簇的北桥芯片，目标 簇的北桥芯片再将消息翻译为对应的读写请求消息发送到目标存控，存控立即处 理该请求并给出响应，相应的响应消息同样由北桥芯片转发回请求簇中的访存发 起c a c h e 。图2 2 给出了此种访存事务的流程示意图 m e m o r y n o r t hnorth c o n t r o ll e r b r i d g ebb r i d g ea ；a c h e 图2