（电子科学与技术专业论文）微处理器体系结构级测试程序自动生成关键技术研究.pdf

a bs t r a c t f u n c t i o n a lv e r i f i c a t i o ni sw i d e l ya c k n o w l e d g e da st h eb o t t l e n e c ko fm i c r o p r o c e s s o rd e s i g n a r c h i t e c t u r e - l e v e lv e r i f i c a t i o nc a l ld i s c l o s ef a i l u r e si nd e s i g nf l o we a r l y ，w h i c hg r e a t l yr e d u c e s l o s s s i m u l a t i o ni ss t i l lt h em a i nv e h i c l ef o ra r c h i t e c t u r e - l e v e lf u n c t i o n a lv e r i f i c a t i o n b u tt h e g e n e r a t i o no ft e s tp r o g r a mf o rs i m u l a t i o nb yh a n d si sv e r yl o we f f i c i e n t ，a n di t sf a i l u r e p r o b a b i l i t yi sh i g h t h e r e f o r e ，t h ea u t o m a t i cg e n e r a t i o no ft e s tp r o g r a mp l a y sam a j o rr o l ei nt h e v e r i f i c a t i o no fm o d e mm i c r o p r o c e s s o r e x i s t i n gt e s tp r o g r a mg e n e r a t o r sd o n tv e r i f yt h ew h o l ed e s i g n t h e i rm e t h o d sf o rm a k i n g a r c h i t e c t u r em o d e la r ec o m p l e x w h a t sm o r e m o s to ft h e mc a nb ei n t r i n s i c a l l yr a n k e dr a n d o m t e s tp r o g r a m g e n e r a t o r ，w h i c hr e s u l t si nl o wv e r i f i c a t i o ne f f i c i e n c y b a s e do no u ro w nf r a m e w o r kf o rm i c r o p r o c e s s o ra i - c h i t e c t u r e l e v e lt e s tp r o g r a mg e n e r a t i o n ， t h et h e s i sf o c u s e so nt h er e s e a r c ho fc o n s t r a i n t ss a t i s f a c t i o np r o b l e mo ft e s tp r o g r a m g e n e r a t i o n a n dd e v e l o p san o v e ls p e c i f i c a t i o nd r i v e na n dc o n s t r a i n t ss o l v i n gb a s e da u t o m a t i ct e s tp r o g r a m g e n e r a t o r t h ep r i m a r yw o r ka n dc o n t r i b u t i o n so f t h et h e s i si n c l u d ef o l l o w i n gt h r e ep a r t s ： f i r s t l y ，w eh a v ed e s i g n e dt h ec o r ec o m p o n e n to fo i ta u t o m a t i ct e s tp r o g r a mg e n e r a t o r t h e c o n s t r a i n t sc o m p i l e r , a n dw o r k e do u tt h es t r a t e g yf o rm a k i n gc o n s t r a i n t sm o d e l b e c a u s et h e c o m p i l e ri si n d e p e n d e n to fv e r i f i e dd e s i g n ，i tc a nw o r kf o ra l lk i n d so fm i c r o p r o c e s s o r sw i t h d i f f e r e n ta r c h i t e c t u r eb yc o n f i g u r i n gt h ea r c h i t e c t u r ei n f o r m a t i o n i m p l e m e n t e db yam e m b e ro f o u r g r o u p ，t h ec o n s t r a i n t sc o m p i l e rw o r k sw e l l s e c o n d l y ，w eh a v ea d v a n c e dan e wv e r i f i c a t i o n o r i e n t e da r c h i t e c t u r ed e s c r i p t i o nl a n g u a g e v a d l ，a n di m p l e m e n t e di t sc o m p i l e r v a d li sv e r yn a t u r a la n dh a sag o o dr e a d a b i l i t y i te a s e s t h ec a f i t u r eo fi n f o r m a t i o nf o rv e r i f i c a t i o n i nv a d l ，w ef o l l o was t r u c t u r ea n db e h a v i o r m i x e d - l e v e la p p r o a c ht of a c i l i t a t es p e c i f i c a t i o no ft h ea r c h i t e c t u r eo f m i c r o p r o c e s s o r ，w h i c hc a n c a p t u r es u 伍c i e n ti n f o r m a t i o nf o rt e s tp r o g r a mg e n e r a t i o n t h i r d l y ，w ed e s i g nt h ea r c h i t e c t u r ef e a t u r ec o n f i g u r a t i o nf i l e ( a c f ) ，a n dw eh a v eb e e na b l e t og e n e r a t ei ta u t o m a t i c a l l y a c fp r o v i d e sa r c h i t e c t u r ei n f o r m a t i o nt oc o n f i g u r et h ec o n s t r a i n t s c o m p i l e r l a s t ，w ed e s i g nt h ei n s t r u c t i o nt e m p l a t el i b r a r y ( i t l ) ，w h i c ha l s oc a i lb eg e n e r a t e d a u t o m a t i c a l l y b e c a u s ei t lc a nh e l pt os e p a r a t et h eg e n e r i cv e r i f i c a t i o nk n o w l e d g eo f m i c r o p r o c e s s o rf r o mt h a to fs p e c i f i ca r c h i t e c t u r e ，o u rs y s t e mc a ng e n e r a t et e s tp r o g r a mf o rm a n y k i n d so f a r c h i t e c t u r e t h ep r o t o t y p es y s t e m m a z t gc a nn o to n l yg e n e r a t et e s t p r o g r a mr a n d o m l y b u ta l s o g e n e r a t es p e c i f i ct e s tp r o g r a m ，i th a sb e e ns u c c e s s f u l l ya p p l i e dt ot h ev e r i f i c a t i o no fd l x p r o c e s s o ra n dl e o n 2p r o c e s s o r a n dt h ee x p e r i m e n tr e s u l t sh a v ep r o v e dt h ev a l i d i t yo fo u r m e t h o d i i 国防科学技术大学研究生院学位论文 k e y w o r d s ：a r c h i t e c t u r ed e s c r i p t i o nl a n g u a g e ，c o n s t r a i n ts a t i s f a c t i o np r o b l e m ， a r c h i t e c t u r ef e a t u r ec o n f i g u r a t i o nf i l e ，i n s t r u c t i o nt e m p l a t el i b r a r y 国防科学技术大学研究生院学位论文 插图索引 图微处理器的设计与验证流程1 图1 2 微处理器体系结构级验证框架7 图2 1m a 2 t g 系统框架1 0 图2 2v a d l 的组织结构1 2 图2 3d l x 指令集中a d d u i 的验证程序1 2 图2 4g 【发加法上溢和存储器未对准的约束1 3 图2 5 用户约束文件的结构1 4 图2 6 约束描述文件实例1 4 图3 ，1 约束编译流程2 1 图3 2 转移目标的四种情况2 3 图3 3 寻找合法标号位置的算法2 3 图4 。1v a d l 与约束编译器的关系2 6 图4 2 存储子系统的例子2 7 图4 3 典型指令的v a d l 描述3 0 图4 4 初始化操作数的指令组合示例31 图4 5 指令映射示例3i 图4 , 6 存储子系统示例3 3 图4 7 存储子系统描述示例3 4 图4 8 数据冲突部分描述示例3 5 图4 9 异常描述示例3 6 图5 1v a d l 编译器结构3 8 图5 ，2v a d l 编译器的中间代码组织结构3 9 图5 3 指令归类部分子树与存储部分子树结构4 0 图5 4a c f 的基本结构4 3 图5 5 指令类中部分方法示例4 5 图5 6c a c h e 失效事务的约束方法示例一4 7 图6 1 工具产生的部分测试程序4 9 图6 2d l x 验证框架5 0 图6 ，3 随机生成系统与m a 2 t g 系统的覆盖率曲线5 l 图6 _ 4 无覆盖率反馈方法与有反馈方法的覆盖率曲线5 2 图6 5 流水线状态覆盖率5 2 图6 6l e o n 2 体系结构一5 3 国防科学技术大学研究生院学位论文 表格索引 表1 1 各种a d l 之间的比较 表4 1 指令描述部分说明 表4 3 存储子系统中的参数 表6 1d l x 体系结构级功能测试程序段指令数 表6 2a d d 指令的覆盖率测度 表6 3 引入错误列表 ，4 ，2 9 ，3 2 ，4 8 ，5 1 5 4 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下迸行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含 其他人已经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它 教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任 何贡献均已在论文中作了明确的说明并表示谢意。 学位论文题目：邀矬墨墨釜鍪坌擅塑趔达蕉庄鱼殖生盛差壁基盔塑壅 学位论文作者签名 一4 j 1 日期：0 一年年j0 月j 己日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定。本人授权 国防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子 文档，允许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据 库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密学位论文在解密后适用本授权书。) 学位论文题目：邀笈堡墨签丞丝撞筮型达蕉痘宣邈生盛基毽撞苤盟窥 学位论文作者签名 作者指导教师签名 鑫牟 毒霉2 - 日期：山。q 年i2 月b 日 日期：必听年i 乙月 日 国防科学技术大学研究生院学位论文 第一章绪论 1 1 研究背景 随着微处理器功能复杂性增加和半导体工艺发展，单个芯片上的晶体管数越来越多， 设计验证面临着严峻挑战。在目前的设计队伍结构中，验证人员一般是设计人员的两倍， 验证所花的时间和精力已占整个设计过程的6 0 到8 0 。微处理器的验证已经成为硬件设 计周期的瓶颈”1 。 设计验证 r t l 验证 逻辑验证 版图验证 产品验证 图1 1 微处理器的设计与验证流程 图1 1 给出了自顶向下的微处理器设计流程。从微处理器的体系结构模型构思开始， 设计人员将这种构思转化为行为级描述，经过体系结构级设计验证以后进入集成电路 ( i n t e g r a t e dc i r c u i t ，i c ) 设计阶段。典型的集成电路设计过程首先将行为级描述转化为寄 第1 页 国防科学技术大学研究生院学位论文 存器传输级( r e g i s t e rt r a n s f e rl e v e l ，r t l ) 描述，这一过程称为行为综合，接着通过逻辑 综合将r t l 描述转化为门级网表，经过版图综合之后得到版图，投片之后就得到微处理器 芯片成品。 上述每一个阶段都称为一个抽象层次。在设计的过程中，为了保证每一步设计的正确 性，在每个抽象层次上都要验证该层次内部以及层次间的一致性，之后才能将设计转换到 下一个抽象层次。 所谓验证就是用来证明设计功能正确性的过程。它不仅要求一开始的行为级描述必须 正确，还要求确保各抽象层次内部优化前后以及抽象层次间转换的等价性。在设计过程中， 越早发现设计错误越容易改正，并且修正错误的开销也越小，而在底层( 包括r t l 、逻辑 级和版图级) 或者投片后发现错误，对设计的修改将涉及到上面各个层次，更正错误所需 要的开销不可想象。因此，目前微处理器验证的层次越来越高 2 】。高层验证与r t l 级验证 己经占整个设计开销的5 2 t “。 微处理器体系结构级验证主要采用两种方法：形式化验证和模拟验证。形式化验证方 法使用数学上的形式化方法证明设计能否部分或者全部满足体系结构功能要求。模拟验证 方法以测试程序为输入，直接模拟运行，根据模拟结果判断设计是否满足功能描述需求。 但是随着微处理器复杂性增加，上述两种方法都遇到了困难。形式化验证方法存在状态空 间爆炸问题，能处理的设计规模较小，还无法验证整个微处理器设计，因此不能完全解决 体系结构级功能验证问题。模拟验证方法仍然是主要验证手段口】，它通过在对象上模拟大 量测试程序来验证尽可能多的体系结构功能。但是完全用手工编写所有测试程序非常耗 时，而且缺乏质量保证。因此，有必要研究体系结构级测试程序自动生成技术，以提高模 拟验证的效率和质量【4 j 。 针对现有测试程序自动生成方法的缺点，我们提出了一种由描述驱动的基于约束求解 的体系结构级测试程序自动生成方法。本文设计了该方法的原型系统m a 2 t g 在研究 各种现有体系结构描述语言的基础上，本文专门面向体系结构级测试程序生成问题的体系 结构建模开发了一种新的体系结构描述语言v a d l ，该语言描述自然，可读性好，并 且v a d l 编译器能够为体系结构级测试程序生成自动建立面向验证的体系结构模型，大大 提高了测试程序生成效率：此外，本文还对约束求解领域进行了研究和分析，针对测试程 序生成的约束满足问题，为各种需要验证的体系结构级功能制定了约束建模策略，并选择 了适用于求解测试生成问题的约束求解库、约束求解算法，完成了约束编译器的设计工作。 1 2 相关研究 1 2 1 测试程序自动生成方法 目前，i n t e l 、a m d 、d e c 等公司和国外少数几所大学已经对体系结构级测试程序自动 生成方法_ 丌展了一系列研究，并且丌发了一些系统。其中，比较有代表性的0 n - f ： 第2 页 国防科学技术大学研究生院学位论文 基于模型的测试程序生成器( m o d e l b a s e d t e s t g e n e r a t o r ，m b t g ) 4 1 的主要代表是 i b mh a i f a 研究所的g e n e s y s 【5 1 系统。它是一种采用专家系统技术为处理器验证 开发的测试程序生成器，采用c + + 语言为指令建立语义模型，其建模工作比较费 时，例如为一块普通的d s p 建模需要3 4 个人月 6 1 。此外，m b 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 ，m p t g ) f 8 】是一种确定性生成 工具。它利用c a c h e 一致性协议作为抽象机模型，使测试需求能够直接控制促使 c a c h e 事件发生的特定测试序列生成。m p t g 对c a c h e 的验证非常有效，但验证范 围仅仅局限于c a c h e 。因此在实际使用中，必须与其他随机测试生成器( 例如 m b t g ) 结合使用。 体系结构验证程序生成器( a r c h i t e c t u r ev e r i f i c a t i o np r o g r a m sg e n e r a t o r ，a v p g e n ) 【9 】采用符号执行、约束求解等技术来生成测试程序。然而，它为用户提供了非常 详细的控制测试向量生成的方法，因此很难维护。 a h a r o n 等开发了随机测试向量生成器( r a n d o m t e s t p a t t e m g e n e r a t o r , r t p g ) 1 0 l ， 它采用b i a s 技术来创建能够为设计正确性提供高可信度的测试子集。 b i n 等【1 将测试程序生成问题当作约束满足问题处理，并开发了相应的求解技术。 l i e h m i n gw u l l 2 1 等提出了一种基于b n f 的测试程序生成器，它利用用户菜单控制 测试程序生成过程，可以生成随机的和指定的测试程序。但是，这种方法不能保 证一定生成满足用户约束( 例如数据冲突约束) 的测试程序，本质上仍是一种随 机生成器。 p m b h mm i s h r a 等 ”1 提出了a d l 描述驱动的测试程序生成方法，这种方法仅限于 流水线的验证。 上述各种系统存在的主要缺点在于不能胜任整个微处理器的验证；处理器体系结构建 模方法复杂，耗费的人力多，时间长；大多数自动生成系统仍然采用随机生成方法，导致 生成的测试程序质量不高。 1 2 。2 体系结构描述语言 虽然已有的各种硬件描述语言能够很好地支持微处理器的结构描述，但是，由于它们 本身处在较低的抽象层次上，因此没有足够的能力支持微处理器体系结构描述。于是，人 们设计了一类专门用于描述微处理器体系结构模板的语言一一体系结构描述语言 ( a r c h i t e c t u r ed e s c r i p t i o nl a n g u a g e ，a d l ) 。 体系结构模板包括微处理器上的各个组件、组件间的互连、每个组件的功能。按照各 种a d l 的针对性可将它们分为：面向综合的a d l 、面向编译爨产生的a d l 、面向仿真器 产生的a d l 、面向验证的a d l 和其它的a d l 。几类较有代表性的a d l 如下： m i m o l a ! ”】是德国d o r t m u n d 大学设计的一种面向综合的a d l 。m s s q 编译器f l q 第3 页 国防科学技术大学研究生院学位论文 和r e c o r d 编译器口7 j 都采用该语言描述目标机器。m i m o l a 不支持仿真器的自 动产生，但m i m o l a 描述可以采用m s s b u 仿真器仿真。m i m o l a 不能显式描 述处理器流水线和资源冲突，因此该语言为v l i w 和深度流水线处理器产生的代 码质量较差。 n m l 1 8 1 是t ub e r l i n 开发的面向编译器的a d l ，用在s i g h s i m 指令集仿真器 1 9 和c b c 代码产生器【2o j 中。由于n m l 假定除存储部件以外的所有功能部件都没有 延迟，所以它不支持对多时钟周期的功能部件和流水化功能部件进行描述。r u m l 的不足还包括不能显式描述多字指令。 l i s a 2 1 1 1 2 2 1 是r w t ha a c h e n 开发的一种面向仿真的a d l 。该语言支持d s p 仿真 器的产生和复杂流水线的描述，但不能显式描述指令集并行编译器的资源冲突。 a i d l ”j 是由t s u k u b a 大学开发的一种面向验证的a d l 。它用时序逻辑描述流水 线的时序行为，可用于流水线行为的验证，但不支持软件工具包的产生。 e x p r e s s i o na d l t “l 是由c a l i f o m i a 大学开发的一种功能强大的a d l 。它通过对 行为和结构进行混合描述来支持体系结构建模：采用类似于l i s a 的方法来支持面 向周期精确的仿真；与l i s a 相比，它还提供了对优化编译的支持；并能直接对存 储器子系统进行描述，提供对新的存储器组织和层次结构的支持。 表1 1 各种a d l 之间的比较 m i m o l ac o a c h - u d l ，in m ll s d lm d e se x p r e s s i o 咐l i s ar a d la i d l 编译器生成 是否为1 l p i l p 约束检查 仿真器生成 周期精确 综合 形式验证 指令集信息 网表信息 存储层次信息 流水线信息 根据各种现有a d l 语言对编译器生成、指令集并行约束检查、仿真、综合以及形式 验证所提供的支持，表1 1 对它们进行了比较。其中“”表示支持，“”表示有限支 持，“x ”表示不支持。 如表1 1 所示，在已有的a d l 中，e x p r e s s i o n 对体系结构建模提供了更强大的支 持其优点在于能够捕获各种新的存储层次信息，并且利用行为和结构的混合描述对设计 空侧探索提供有效支持，但是对验证的支持非常有限。因此，在现有的a d l 中，还没有 第4 页 国防科学技术大学研究生院学位论文 一种语言能够完全适用于微处理器体系结构级测试程序生成的体系结构建模。 目前，p r a b h a t m i s h r a 等已经对基于a d l 建模的微处理器验证方法进行了一些研究： 文献【2 5 】基于a d l 语言建立的体系结构图模型对体系结构特征进行分析，以确保流水线静 态行为的正确性：文献【2 6 基于采用a d l 建立的微处理器有限状态机模型来分析指令流， 以验证流水线的动态行为；文献【2 7 】利用e x p r e s s i o na d l 捕获微处理器结构和行为特 征，自动生成可综合的r t l 描述，然后以该描述作为参考模型对微处理器展开等价性检查； 文献 2 8 采用基于模型检验的方法为微处理器自动生成测试程序。这种方法首先将微处理 器体系结构的a d l 描述映射到s m v ( s i g n a lm o d e lv e r i f i e r ) 【2 9 j 描述，然后用s m v 对描 述进行形式化验证，通过生成反例来产生测试程序。 已有的描述方法主要是为微处理器的流水线验证而提出的，还没有考虑整个微处理器 的运行环境，不支持对存储层次、存储管理部件等进行验证，并且采用的验证方法以形式 化验证为主，受形式化验证固有缺点的影响较大；验证模型比较抽象，不能很好地应用于 微处理器底层设计的验证。 1 2 3 约束满足问题 约束表达了事务间的制约关系，是认识和刻画对象的一个重要方面。人工智能领域和 计算机科学其他领域的大量问题都可以形式化为约束满足问题( c o n s t r a i n ts a t i s f a c t i o n p r o b l e m c s p ) 1 3 0 1 ，例如，机器视觉、布局规划、调度等【3 1 1 。从形式化的角度来看，c s p 由变量和变量间的约束关系组成，每个变量都与一组数值关联，这组数值就构成了变量的 定义域，变量的数目称为c s p 的元，约束是建立在变量集合的子集上的一种关系，表示这 些变量的有效组合。任意一个满足所有约束关系的n 元组都是n 元c s p 的解。约束网络是 个以变量为结点的超图，结点间的边( 弧) 代表变量间的约束。 约束满足问题的求解就是找到所有变量的一个或多个赋值，使约束得到满足。经典的 c s p 求解方法是基于树的搜索算法，在此基础上，人们提出了各种改进方法，包括维持弧 致性( m a i t a i na r cc o n s i s t e n c e ，m a c ) 3 2 1 【3 3 】、路径一致性、前向检查( f o r w a r dc h e c k i n g ， f c ) c 3 4 】、向后标记以及一些变量赋值顺序和变量值选择的启发式策略1 3 ”。这些方法基本上 都是从元结构( 约束图的拓扑结构) 、宏观结构( 约束问的关系) 以及微观结构( 一个变量不同 值之间的关系) 三方面出发，试图通过缩小搜索空间和寻找最佳搜索路径来提高c s p 问题 的求解效率。 约束求解算法主要有三类：产生与测试( g e n e r a t e - a n d - t e s t ，g t ) 、回溯( b a c k t r a c k i n g ， b t ) 、约束传播( p r o p o g a t i n gc o n s t r a i n t s ，p c ) 。 1 产生与测试 采用产生与测试方法的求解器系统化地产生所有变量组合，并测试这些组合是否满足 所有约束。第一个满足所有约束的组合便是问题的解。这种方法非常低效，它需要考虑的 组合总数等于c s p 问题中所有变量定义域的笛卡尔乘积的数目。 第5 页 国防科学技术大学研究生院学位论文 2 回溯 在回溯【3 叫的方法中，求解器直接搜索问题的解。它按顺序对变量进行初始化，一旦所 有与某个约束相关的变量都被初始化了，那么该约束就是有效的。如果变量的任何一个部 分初始化违反了某个约束，则回溯到最近一个初始化的、仍然存在可选数值的变量。明显， 只要出现某个部分初始化的变量元组违反了某个约束，回溯就可以从变量定义域的笛卡尔 乘积空间中删除一个子空间。回溯方法的关键思想是对约束满足问题的潜在解空间进行深 度优先搜索。 虽然：回溯方法优于产生与测试方法，但对于大多数问题来说，其复杂度仍然是指数 级的。简单回溯算法低效的主要原因之一是结点的不一致性。举个简单的例子，假设变量 v 。的定义域包含了某个不满足v - 的一元约束的数值a ，那么，在进行搜索的过程中，每次 旦将a 赋值给v 。就会立即导致失败。另一个原因则是缺乏弧一致性。假设变量按照v - ， v 2 ，v f v j ，v n 的顺序初始化，且v 与v j 间的二元约束使得v i 不能取a 。在这样的 回溯搜索中，每次v - 被初始化为a 时，v j 的任何赋值都会失败。对于变量v k ( i a l e a d s d = r 3 ，a d s s 2 = i m m l ) ； 1 1 i n d e x = 5 = s g t ( ，a d s s 2 = r t 8 ) ； 1 2 i n s e n d ； 1 3 r e l b e g i n ： 1 4 r lf _ r 2 ； 1 5 r 3 = r t 8 ； 1 6 i m m l ：= i r g ： 1 7 r e l e n d ； 1 8 e n d r e q u i r e m e n t ； 图2 6 约束描述文件实例 各种指令所占比例的定义位于总的指令条数范围说明之后，也属于可选部分。用户可 以灵活控制具体类型的指令( 例如：a l u 类、访存类、跳转分支类等等) 或者具体的某种 指令( 例如：a d d 、s u b 等) 在测试程序中出现的频度。编译器会根据这里的定义和前面 测试程序的指令总数定义计算出规定指令的条数。由于编译器对指令总数的处理是不精确 塑：堕坠型堂全更坌生堕竺堡坐墨至堕塑盟! 第1 4 页 国防科学技术大学研究生院学位论文 变量和范围说明主要是对后面的指令说明和操作数关系说明语句中使用的变量进行 声明。 指令说明块说明用户对测试程序的约束，这里的约束主要包括如下几种类型的约束： 1 指定某个具体位置上出现的指令类型或者具体指令； 2 约束指令中操作数的类型、立即数数值、使用的寄存器或者访存地址； 3 ，如果在要验证的指令集结构中，同一指令可关联多种寻址方式，还可以指定要验 证的寻址模式； 4 直接指定出现何种类型的数据相关； 5 通过在约束文件中安排指令的位置来控制引起数据相关的具体指令； 6 某条指令要产生的异常，例如：上溢； 7 要求产生的与指令无关的异常，例如：存储器未对准异常。 操作数关系说明语句位于指令说明块后面，它是约束描述文件的最后一个部分，主要 负责定义指令说明块中操作数变量间的关系。 图2 6 给出了一个约束描述文件的例子。从文件中可以知道用户想验证指令的异常处 理、寻址模式、数据相关以及某几种指令的正确性。文件中要求测试程序大小为8 1 0 条 指令；在生成的约束代码中a d d 指令条数占1 5 ；测试程序的第一条指令为a d d ，它的 源操作数l 与目的操作数不能使用相同的寄存器。且要求它产生上溢异常；第三条指令为 访存类指令，要求它采用第二种寻址模式( a d l 编译器会给出目标微处理器的寻址模式编 号) ：第四条指令为a l u 类指令，它的源操作数2 是立即数，且在1 0 2 5 内：第五条为 s g t 指令，且要求它的源寄存器2 与上一条指令的目的寄存器相同。 这种约束语言给用户赋予了灵活的控制权，使得m a 2 t g 系统具有如下的特征： 1 用户可以定义测试程序中用到的指令或者指令组合； 2 用户可以控制测试程序中发生异常的种类以及它们出现的频度。 3 用户可以指导生成器生成满足资源共享的指令序列。所谓资源共享就是指在指令 流的一个小的指令窗口内，尽量密集地使用相同的资源( 例如：寄存器，存储器 位置等等) 。 4 用户可以调用测试知识过程。所谓测试知识过程就是一些在测试程序生成的过程 中可以直接调用的，能够影响生成的测试程序中指令元素选择的生成函数。 5 用户可以控制测试程序中包含各种类型的循环。 2 7 约束编译器 约束编译器是m a 2 t g 系统的核心部件，它的主要任务是编译用户约束文件，根据用 户的约束需求为测试程序约束满足问题建立约束模型。由于约束编译器的约束建模策略适 第1 5 页 国防科学技术大学研究生院学位论文 用于各种类型的体系结构，所以约束编译器按照体系结构特征配置文件配置之后，能够为 不同体系结构的微处理器建立能够生成有效测试程序的约束模型。测试程序的约束模型由 约束编译器根据普遍微处理器体系结构级验证知识建立的约束模型和i t l 针对特定体系结 构建立的约束模型共同组成，这两种模型都采用c + + 语言表示，因此它们与约束求解库链 接得到一个可执行程序，执行该程序就产生满足用户需求的面向目标微处理器的测试程 序。约束编译器的详细讨论参见本文第三章内容。 2 8 本章小结 m a 2 t g - 系统是微处理器体系结构级测试程序自动生成方法的原型系统。该方法不仅 可以随机生成测试程序，最主要的是可以基于用户约束描述文件，采用约束求解的方法产 生针对满足用户需求的测试程序。 本章通过对m a 2 t g 系统的特点进行分析，指出由描述驱动的基于约束求解的方法的 优点；系统地介绍了m a 2 t g 的总体框架和工作流程；概要介绍了系统的各个组成部分： 体系结构描述、体系结构特征配置文件、指令模板库、约束需求描述以及约束编译编译器。 第1 6 页 国防科学技术大学研究生院学位论文 第三章约束编译器的设计 约束编译器是m a 2 t g 系统的核心部件。它独立于目标微处理器的体系结构，是一种 可配置的编译器。其主要任务是编译用户约束描述文件，根据用户需求约束和指令模板库 所提供的体系结构级固有约束为测试程序建立c + + 约束模型。 3 1 测试程序生成约束满足问题 用于微处理器体系结构级验证的模拟矢量通常都以测试程序的形式产生，以触发特定 体系结构级事务。这些测试程序应该满足两个需求：1 ) 必须有效，也就是说，程序行为 和指令格式必须符合目标微处理器的体系结构定义。2 ) 应该具有高质量。即生成的测试 程序应该尽可能多地覆盖用户的约束需求和功能点，能够找出潜在错误。因此，个理想 的测试程序应该在满足约束的前提下尽可能随机产生。所以，我们很自然地将这种有效的、 满足验证需求的测试程序生成问题建模为c s p 。测试程序生成器的任务是根据微处理器的 体系结构模型和用户的验证需求建立测试程序的约束求解模型，这些约束求解模型与相应 的约束求解库链接执行，产生满足约束的测试程序。与通常的c s p 相比，测试程序生成问 题具有如下两大特点： 1 变量定义域大 要将测试程序生成问题建模为c s p 就需要将体系结构级资源建模为c s p 变量。这些 资源包括寄存器单元、存储器单元、c a c h e 单元等等。而在现代微处理器中，这些单元的 取值范围都相当大。例如，6 4 位寄存器的取值范围包括2 ”个数值。因此，代表这些资源 的c s p 变量对应的定义域都非常庞大。这些大定义域的简单组合、线性约束以及非线性非 单调的约束使得对这些定义域的存储和操作都相当困难。因此，c s p 的建模和求解面临着 严峻的挑战： 首先，无论是显式地表示一个大小为2 “的集合，还是求解这些具有大定义域的变量都 存在问题。对于变量来说，它们的约束只能隐式地表示。 其次，这些具有大定义域的变量将使得n 元约束与二元约束的转化件i j 不可行。在c s p 建模过程中，一个非常重要的建模策略就是确定约束的元数。约束要么建立在两个变量的 关系上，即二元约束，要么建立在多个( 三个或者三个以上) 变量之间的关系上，即多元 约束。在测试程序生成领域，大部分约束都是多元的，例如；构建加法上溢异常时，“加” 是一个三元约束。原始的m a c 算法是为二元约束网络设计的。它使用m a t h w o r k 提出的 r e v i s e 过程【4 2 1 来获得二元约束的致性。虽然问题很容易被建模为多元的，但在理论上， 任意c s p 都可以被转化为二元约束网络。转化过程为每一个多元约束建立一个新的变量， 该变量的定义域由约束允许的多元组集合构成。但是当为某些问题建模时，变量定义域太 大会导致这种转化方法不可行。m a c 算法还有一些处理多元约束的传统方法，例如：将 第1 7 页 国防科学技术大学聊f 究生院学位论文 多元约束表示为一个显式的元组列表的方法。但是，这些方法仍然不能处理定义在大定义 域上的c s p 。 2 解空间的均匀分布 目标微处理器设计中存在的错误数目和要触发这些错误所需测试场景的数目都是非 常惊人的。依靠约束描述文件毫无冗余地精确定义恰好能够实现完全覆盖的测试程序是不 可能的。因此，我们希望测试生成器能够尽可能填充描述与验证需求之间的缺口。换句话 说，测试生成器应该在满足用户验证需求的前提下，尽可能覆盖更多的功能点。因此，测 试生成问题需要在解空间上随机的、均匀分布的解。这一点与传统的约束求解相悖，传统 的c s p 通常要求找到任意一个解、所有的解或者最好的解。 测试程序生成问题的上述两个特点给c s p 建模和求解都带来了极大的挑战。 3 2 约束建模策略 典型的测试程序是由一系列测试场景构成的。从处理器运行的角度看，每个场景都可 以触发特定的体系结构级事务，即指令的执行和系统级交互( 例如：c a c h e 失效) 。在测 试程序的c s p 模型中，许多变量都可以看作这些事务的属性变量。大多数情况下，同一事 务的内部变量之间都存在大量的约束，而事务之间的约束并不太多。因此，测试生成问题 的完整约束网络是一个由大量网间约束关系松散、内部约束关系相对紧密的小约束网络连 接而成的大网络。其中，每个小约束网络代表一个事务。我们把那种能够影响多个小网络 中变量的约束称为全局约j 包 根据测试程序的约束网络所具有的特点，为测试程序建立约束模型存在三种可选策 略： 1 按照测试生成问题的完整约束网络建立一个总的约束模型； 2 按照体系结构级事务，将测试生成问题分解成若干个子问题，每个子问题对应一 个事务。从约束网络的角度讲，就是将测试生成问题的完整约束网络划分为体系 结构级事务对应的小约束网络，然后为每个事务对应的小约束网络建立约束模型。 3 首先，按照上面第二种策略将测试生成问题的完整约束网络分解为体系结构级事 务对应的约束子网；然后分解体系结构级事务的约束子网内部的约束关系，将子 网进一步划分为内部约束祸合更为紧密的指令内部约束子网，为单条指令内部约 束子网建立约束模型。我们把事务内部的指令间约束称为局彩乡9 荣： 约束编译器采用第三种策略打破全局约束和局部约束，仅为指令内部的约