（计算机系统结构专业论文）asip体系结构形式化建模与验证方法研究.pdf

摘要 摘要 专用指令集处理器( a p p l i c a t i o ns p e c i f i ci n s t r u c t i o n ss e tp r o c e s s o r ，a s i p ) 是专为某个或某类应用而设计的处理器。随着a s i p 体系结构的不断发展，设 计的复杂性不断增加，如何有效地验证体系结构设计的正确性问题在a s i p 设 计中日益突出。a s i p 体系结构本身具有指令行为定义的多样性和逻辑结构设计 的灵活性等特点，使得构造验证模型与精确地刻画系统特征非常困难，尚未形 成一套能够有效地解决a s i p 体系结构层设计自动验证问题的理论和方法。 本文针对上述问题，在分析a s i p 体系结构的层次化设计特征的基础上， 提出了基于p e t r i 网理论和模型检测方法的a s i p 体系结构验证框架，对a s 口 体系结构进行描述和验证。通过对已有的a s i p 体系结构设计的分析，将a s i p 体系结构需要满足的属性分为静态属性和动态属性两个方面，分别进行研究。 静态属性是指系统中的结构特征和单条指令的执行情况的检测，动态属性关注 的是指令并发执行设计的正确性，主要包括与数据相关、控制相关等方面相关 的控制结构设计的正确性的检测。主要研究工作包括： ( 1 ) 基于p e t r i 网描述a s i p 体系结构。首先根据a s i p 体系结构设计的特 点提出一个新的扩展的p e t r i 网- h d p n ( h a r d w a r ed e s i g nb a s e d o np e t r in e t ) ， 用其描述a s i p 体系结构，刻画处理器设计中的结构和行为特征。然后给出a s i p 设计需要满足的静态属性，用以检测a s i p 设计中的静态需求是否得到满足。 ( 2 ) 基于模型检测方法对动态属性进行验证。首先建立待验证的a s i p 体 系结构模型并提取该模型需要满足的动态属性，然后采用模型检测工具对模型 和动态属性的一致性进行验证。本文给出了基于模型检测方法建立a s i p 体系 结构模型的方法，针对流水线处理器和乱序处理器两种抽象处理器描述了具体 的建模方法，分析了它们的动态属性，并对其进行了验证，证明了此方法的有 效性。 ( 3 ) 结合a s i p 设计的层次化特点，提出了层次化和局部化的建模方法。 采用抽象模型描述设计的整体特性，采用细化模型来刻画局部设计的细节，从 而控制模型的规模，规避模型检测方法中的状态空间爆炸问题。 ( 4 ) 提出了从h d p n 描述到模型检测描述的转换规则。在此基础上，实 现了一个支持结构检测和指令执行正确性检测的体系结构验证框架。 本文做出的贡献主要体现在： ( 1 ) 面向体系结构建模的需求，基于p e 拄i 网理论，提出了一种a s i p 体系 结构描述方法啪p n 。h d p n 继承了p e t r i 网的直观性特点，可以很好地刻 画体系结构中模块间的互连关系；在此基础上加强了对设计中的存储单元、功 摘要 能单元以及数据通路的刻画，通过对p e t r i 网中的基本元素库所、变迁和弧 的扩展，分别对存储单元中存储的数据添加了类型定义，对功能部件添加了接 口参数、执行条件和具体的行为描述，对数据通路定义了所传递的参数，提高 了模型的描述能力。基于h d p n 描述提出a s i p 设计需要满足的静态属性，对 设计的结构描述正确性和单条指令执行的正确性进行验证。 ( 2 ) 将模型检测方法应用于a s i p 体系结构验证中。提出了基于模型检测 方法建立a s i p 体系结构模型的方法，针对流水线处理器和乱序执行处理器描 述了具体的建模方法，并给出了处理器正确执行所需满足的属性。在建模时采 用分层和局部建模的方法有效规避模型检测方法中的状态空闯爆炸闯题，提高 了模型检测方法的可用性。 ( 3 ) 建立了h d p n 描述和模型检测描述之间的转换规则，形成一个完整 的a s i p 体系结构验证框架。将a s i p 体系结构的验证问题合理地划分为静态属 性( 结构正确性和单条指令执行的正确性问题) 和动态属性( 指令并行执行的 正确性问题) 两个子问题，分别通过基于p e t r i 网的静态属性检测方法和基于模 型检测的动态属性的检测方法对其描述和验证。 关键词；a s i p 体系结构设计形式化验证p e t r i 网 模型检测 木本论文工作得到国家自然科学基金( 6 0 2 7 3 0 4 2 ) ，高等学校博士学科点专 项科研基金( 2 0 0 5 0 3 5 8 0 4 0 ) ，安徽省自然科学基金( 0 7 0 4 1 2 0 3 0 ) 的支持，在 此表示感谢。 l l a b s t 聪i c t a b s t r a c t a p p l i c a t i o ns p e c i i n s t r u c t i o n ss e tp r o c e s s o r s ( a s i p ) i sak i n do fs p e c i a l p r o c e s s o rd e s i g n e df o r ap a n i c l l l a rt ) ，p e o f 印p l i c a t i o n s w i t l lt 1 1 ec o n t i n u o u s d e v e l o p m e n to fa s i pd e s i g n ，t h ec o m p l e x i t ) ，o ft h ed e s i g ni sa l s oi n c r e a s i r 唱，a l r l dt h e v e r m c a t i o ne f f o r t so nt 1 1 ec o r r e c t i l e s so fd e s i g na r ei n c r e a s i n g l yp r o m i n e n t l y a c c o r d i n 9 1 y d u et ot l l ed i v e r s i t ) ro fi i l s t r u c t i o n s b e h a v i o r sa n d 也ef l e x i b i l i t yo f l o g i c a ls t 】咖e s ，i ti sv e r ) rd i 伍c u l tt ob u i l dag e n e r a lm e t h o d t 0v e r i 匆t h e c o n e c t n e s so ft 1 1 ea s i pd e s i g i la u t o m a t i c l y s of 缸m e r ei sn o ta n ye f i e c t i v et 1 1 e o r y a i l dm e m o d o l o g yo nt l l ea u t o m a t i cv e r i f i c a t i o no f a s i pd e s i g na ta r c l l i t e c t u r el e v e l o nn l ep r o b l e m sm e n t i o n e da _ b o v e ，也et l i e r a r c h yc h a r a c t e r i s t i c so fa s i p a r c m t e c t u r ed e s i g nw e r ea n a l y z e dd e e p l y af r a m e w o r ko nt l l ev e r i f i c a t i o no fa s i p a r c l l i t e c t u r ed e s i g n ，w h i c hi sb a s e do np e t r in e ta 1 1 dm o d e lc h e c l ( i n gm e o 巧a n d m e t h o d o l o g y ，i sp r e s e n t e di nt h i st h e s i s t h ep r o p e r r t i e s 、h i c ha na s i pd e s i g nn e e d s t 0s a t i s 鸟a r ed i v i d e di n t os t a t i cp r o p e r t i e sa n dd y n a n l i cp r o p e r t i e s s t a t i cp r o p e r t i e s a r eu s e dt os p e c i 句t h er e q u i r e m e n t so fs t m c t u r ea u l d i n d i v i d u a li n s t r u c t i o n s e x e c u t i o n ，、：h i l ed y n 锄i cp r o p e r t i e sa r eu s e d t o s p e c i f yt | l er e q u i r e m e n t so f c o n c u 盯e n ti n s t r u c t i o n s t h em a i nr e s e a r c h 、v o r k si n c l u d e ： ( 1 ) d e s c r i p t i o no ft 1 1 ea s i pa u r c t l i t e c t u r eb a s e do np e t r in e t h a r d w a r ed e s i g n b a s e d o np e t r in e t ( h d p n ) ，a ne x t e n d e dp e t r in e t ，i su s e dt od e s c r i b et h es t r u c n l r a l 砒l db e h a v i o r a lc h a r a c t e r i s t i c so fa s i pa r c l l i t e c t u r e t h es t a t i cp r o p e n i e sw l i c ha n a s i pd e s i g ns h o u l do b e ya r ea l s op r o p o s e d ( 2 ) v e r i f i c a t i o no fm ed y n a m i cp r o p e r t i e sb a s e do nm o d e lc h e c k i n g f i r s t l y ， t l l em o d e lo fa s i pa r c k t e c n l r et ob ev a l i d a t e di sc o n s t m c t e d ，a n dm ed ) ，1 1 锄i c p r o p e r t i e sw k c hap r o c e s s o r s h o u l do b e ya r ee ) m a c t e d 舶mc u s t o m e r b u i l t r e q u i r e m e n t s t h e nm o d e lc h e c k e ri su s e dt oc l e c kt h ec o n s i s t e n c yo fm e m o d e la i l d o ft h ep r o p e r t i e s t h em e m o di sa p p l i e dt oap i p e l i n ep r o c e s s o ra n da no u t o f o r d e r p r o c e s s o rt op r o v et h ea v a i la _ b i i i t y ( 3 ) m o d e l i n gm e t l l o db a s e do nt h eh i e r a r c h i c a la i l dl o c a lc h a u r a c t e r i s t i co fa s i p d e s i g n i n o r d e rt o e m c i e n u yv e r i 匆m ed e s i g n ，t l l e m o d e l s s c a j es h o u l db e r e s t r i c t e d t w ol ( i n ( 1 so fm o d e l s ，g l o b a ld e s i g na 1 1 dl o c a lm o d e l sa r cc o n s 订u c t e dm 吐l i sm e t h o d 7 n l eg l o b a ld e s i g n ，i nw h i c hm a n yd e t a i l sa r eh i d d e nt or e d u c et l l es c a l e o ft h em o d e l ，i su s e dt oc h e c kt l l ev a l i d i t yo fm ei n t e r a c t i o nb e t w e e n t h ec o m p o n e n t s i l i a b s t r a c t w k l el o c a lm o d e l s ，i 1 1w h i c hc o n c r e t ed e s i 弘so fe a c hi n d i v i d u a lc o m p o n e n ta r e d e s c r i b e d ，a r eu s e dt 0v e r i 匆d e 协i l e ds p e c i f i c a t i o n s i i i 锄ss i t u a t i o n ，t 诧o t h e rp a r t s o ft h ed e s i g na r e 臼e a t e da so u t e re n v i r o n m e n t ，a n dt h ei n t e r f a c ep a r a m e t e r so fm e m o d e la r es e ta ss t o c h a s t i cv a l u e si nm ep o s s i b l er a i l g e ( 4 ) 1 1 l et r a i l s l a t i o nr u l e s 丘o mh d p nb 2 l s e dd e s c 邱t i o nt om o d e lc h e c k e r b 2 l s e d d e s c 邱t i o n b a s e do nt h et 凇s l a t i o np r o c e d u r e ，av e r i 丘c a t i o n 丘a m e w o r kw 1 1 i c h s u p p o n s t h ev a l i d a t i o no n 也ec o r r e c t l l e s s0 fs 仃l l c t u r e sa 1 1 di n s t n l c t i o n s e x e c u t i o no f a i la s i pa r c h i t e c t u r ed e s i g ni sc o n s t l m c t e d t h em a i nc o n t r i b u t i o n so ft h i st h e s i sa r ea sf o l l o 、程： ( 1 ) a i m i n gt 0 t h ed e s i g no fa s i pa r c h i t e c t u r e ，an o v e le x t e n d e dp e t r in e t m o d e ln 锄e dh d p ni si n t r o d u c e d i tc a nd e s c 曲et a r g e ta r c h i t e c t u r ei nas u c c i n c t a n dp r e c i s ew a y i l l 玎) p n ，t o k e n sa r ee n d o w 酣w i t l lc o n c r e t ei n f l o n n a t i o na c c o r d i n g t ot h es p e c i f i cd e s i 盟，b u tn o to n l ya b l a c kd o ti nt r a d i t i o n a lp e t r 主n e t 。t h e r e f o r en l e e l e m e n t si 1 1t h ep l a c e sa r ea d d e dw i t l lt y p e s a n dt 锄s i t i o n s ，砌c ha r eu s e dt o d e s c r i b et h em n c t i o nu 1 1 i t s ，a r ea p p e n d e dw i t l li m e r f i a c ep a r 锄e t e r s ，e x e c u t i o n c o n d i t i o n sa n dc o n c r e t ea c t i o nd e s c r i p t i o n a r c s ，w h i c ha r eu s e dt 0d e s c r i b ed a t a p a m ，a r ea l s oa p p e n d e d 惭t hp 娥盥e t e r s 。t 0s 啪u p ，a sam o d e l i n gt o o l ，h d p nc a n s u m c i e n t l yd e s c r i b et h es t m c t u r a li n f 0 衄a t i o na n di n d i v i d u a li n s t m c t i o n s e x e c u t i o n o ft l l ea s i pa r c h i t e c t u r e t h em e t h o db a s e do nh d p n ，t a k i n ga d v a n t a g eo fi t ，c a i l e f f i c i e n t l yv e r i f yt h es t a t i cp r o p e r t i e sa c c o r d i n g l y ( 2 ) m o d e lc h e c k i n g i s a p p l i e dt o t h ev e r i 丘c a t i o no fa s i pa r c h i t e c t u r e m o d e l i n gm e t h o db a s e do nh i e r a r c h i c a la i l dl o c a ld e s c r i p t i o ni sp r e s e n t e da n du s e d t oa b s t m c tm o d e l sf r o map i p e l i n ep r o c e s s o ra n da i lo u t o f - o r d e re x e c u t i o np r o c e s s o r t h e s em o d e i i n gm e t h o d sa r ee f f e c t i v et 0a v o i ds t a t es p a c ee x p l o s i o l l t h ed y l l a m i c p r o p e r t i e su s e dt oc h e c k t h ec o r r e c t n e s so fap r o c e s s o re x e c u t i o na r ea l s op r o p o s e d ( 3 ) t h et r a n s l a t i o nm l e s 舶mh d p nd e s c r i p t i o nt ot h ei n p u tl a l l g u a g eo fm o d e l c h e c k e r 二n u s m v2 l r e p r e s e n t e d t h e r e f o r e ，a ni n t e 斟a t e d 矗锄e w o r k f o ra s i p a r c h i t e c t u r ev e r i f l c a t j o ni sb u i l t t h ep r o p e n i e sf o rt h ev 丽f i c a t i o na r ed i v i d e di n t 0 s t a t i c p r o p e n i e sa n dd y n 锄i cp r o p e n i e s t h e y a r ec h e c k e d 缸o u 曲m es t a t i c p r o p e r t yc h e c k i n gm e m o d b a s e do nh d p na r l dd y n 撇i cp r o p e r c yc h e c k i n gm e t l l o d b a s e do nm o d e lc h e c k i n g ，s e p a r a t e l y k e yw o r d s ：a s i p a r c h i t e c n 鹏d e s i g n ，f o m a lv e r i f i c a t i o n ，p e t r in e t ，m o d e l c h e c 虹n g 目录 图目录 图1 1a s i p 设计中的关键步骤2 图1 2 可重构代码生成器3 图1 3 可重构编译器4 图1 4 模型检测方法的流程图9 图1 5a s i p 设计的验证框架1 7 图2 1d l x 流水线的h d p n 模型2 7 图3 1 库所输出到单个变迁和变迁输出到单个库所3 7 图3 2 一个库所对应多个输出变迁3 8 图3 3 一个变迁对应多个输出库所3 8 图3 4 一个库所对应多个输入变迁3 9 图3 5 一个变迁对应多个输入库所：4 0 图4 1 一个n u s m v 程序实例4 6 图4 2l t l 运算符的语义。4 8 图4 3 流水线h d p n 模型的抽象5 3 图4 4 流水线h d p n 的层次化模型5 4 图5 1 转化后的n u s m v 表达式6 1 图6 1 流水段控制的f s m 表示6 7 图6 2 使用n u s m v 进行验证的框架。7 0 图6 3 对i d l e 出发的条件进行修改后的反例7 1 图6 4 流水线的数据相关7 3 图6 5 采用定向技术消除数据相关7 4 图6 6 带有转发机制的流水线7 5 图6 7 部分旁路流水线结构7 6 图6 8 流水线支持的指令格式7 7 图7 1 基于t o m a s u l o 算法的m i p s 浮点部件的基本结构8 4 图7 2t o m a l s u l o 算法中提取的寄存器模型8 6 图7 3 使用t o m a s u i o 算法，能够处理猜测的m i p s 浮点部件结构8 8 图7 4 寄存器备份模块8 9 图7 5 一个基于t o m a s u l o 算法的简单处理器结构9 l 图7 6t o m a s u l o 算法中提取的存储器模型9 3 图7 7 存储器备份模块9 4 目录 表目录 表2 】库所与体系结构部件的对应，2 7 表2 2 变迁与体系结构部件的对应2 8 表2 3 从微操作到串操作的转换3 0 表5 1 从h d p n 描述到n u s m v 输入语言的转换5 8 x 中国科学技术大学学位论文相关声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工 作所取得的成果。除己特别加以标注和致谢的地方外，论文中不包 含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对 本研究所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即： 学校有权按有关规定向国家有关部门或机构送交论文的复印件和电 子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进 行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论 文。 保密的学位论文在解密后也遵守此规定。 作者签名：五鸷国 2 叼年弓月刁日 、，可 | 第1 章绪论 1 1 引言 第1 章绪论 专用指令集处理器( a p p l i c a t i o n - s p e c i f i ci n s 劬c t i o np r o c e s s o r ，a s i p ) 针对 特定应用进行指令集专用性设计，具有灵活性与性能权衡最优的特点，有良好 的应用前景，为嵌入式系统的研发提供了一种低风险、短上市时间的实现途径， a s i p 的设计和验证也随之成为近些年的研究热点。 在本章中，首先介绍a s i p 的应用背景和a s i p 的设计方法，然后阐述a s i p 设计的验证方法研究现状，引出本文的组织结构。 1 2 a s i p 应用背景 近年来，处理器被越来越多地应用到电子产品中。依据应用背景的不同， 芯片需要处理不同类型的应用程序，满足特定的性能、芯片面积、以及功耗等 方面的需求，这对基于通用处理器的电子系统设计提出了新的挑战。虽然通用 处理器对各种应用的适用性很强，但是通常无法达到在特定应用环境下对芯片 性能、面积及功耗的要求。 解决这些问题的最常用的策略是设计专用集成电路( a p p l i c a t i o ns p e c i f i c i n t e g r a t e dc i r c u i t ，a s i c ) 。但是随着工艺发展，专用集成电路的设计成本越来 越高，而且这些专用集成电路的可编程性也不好，灵活性低，因而人们提出a s i p 来解决上述问题。a s i p 以一个通用的处理器核为基础，设计者在这个核的基础 上根据应用的具体特征对其定制，以获得满足具体应用对性能寸成本、功耗等 多方面要求的处理器。 随着i c 设计技术的发展，现在已经可以使用高层综合工具设计大规模的 a s i p ( s a t o ，i m a ie ta 1 1 9 9 1 ) 。a s p 根据约束( 如芯片面积和功耗) 定制体系结 构和优化指令集以最大化a s i p 性能，降低实现成本。与a s i c 相比，由于a s i p 具有更好的可编程性和灵活性，有利于在设计后期依照发现的错误或调整的功 能需求对设计进行修改，而a s i c 由于具有固定的计算资源和指令集的特点， 不具备这样的优势。 由于同一应用领域中不同应用程序之间的计算方式往往存在很大的相似 性，通过这种修改便可以使其在面向某一应用领域时的性能大大提高，而且这 种设计方式只需在原有芯片的基础上进行少量修改就可以快速设计出适应特定 第1 章绪论 应用的新芯片，大大缩短了芯片开发周期和上市时间。 1 3a s i p 设计 在a s i p 设计方法中，较为经典的方法是将a s i p 设计分为五个关键步骤： 应用分析( a p p l i c a t i o n 心l a l y s i s ) 、体系结构设计空间搜索( a r c l l i t e c t u r a ld e s i g l l s p a c ee x p l o r a t i o n ) 、指令集生成( i i l s t m c t i o ns e tg e n e r a t i o n ) 、代码综合( c o d e s y n 龇s i s ) 和硬件综合( h a r d w s y r l n l e s i s ) ( j a 氓b a l a l ( r i s h n a i le ta 1 2 0 0 1 ) 。这 些步骤如图1 1 所示。 图1 1a s i p 设计中的关键步骤 a s i p 设计过程从分析应用开始，以一个或一组应用以及它们的测试数据和 设计约束作为输入。在进一步的设计过程之前，使用一些合适的分析器静态和 动态地分析这些应用和它们的测试数据。通过应用分析得出的结论可以指导硬 件综合和指令集生成。应用通常采用高层语言书写，应用进行静态和动态分析 后的信息被存储为某些合适的中间格式，用于后续步骤。已有的研究包括( s a t 0 ， i m a ie ta 1 1 9 9 1 ；s a g h i r ，c h o we ta 1 1 9 9 4 ；g h a z a l ，n e w t o ne ta 1 2 0 0 0 ；g u p t a ， s h a n n ae ta 1 2 0 0 0 ；s u r e s h ，n 匈i a re ta 1 2 0 0 3 ) 。 2 第l 章绪论 根据应用分析的结果，设计者在一系列候选体系结构中选择合适的体系结 构。针对专门的应用，使用应用分析的输出和给定的设计约束对一系列可能的 体系结构进行选择。选择过程通常由性能评估器驱动的设计空间搜索方法组成， 合适的体系结构需要满足性能和功耗约束。主要有两种性能评估方法：基于调 度程序的方法和基于仿真器的方法。已有的研究参见( g l o r i aa n df 觚a b o s c h i1 9 9 0 ； g o n g ，g 萄s k ie ta 1 1 9 9 5 ；b i i 】1 1 ，i m a ie ta 1 1 9 9 6 ；k i e n h u i s ，d 印r e t t e r ee ta 1 1 9 9 8 ； k i n ，l e ee ta 1 19 9 9 ；g h a z a l ，n e 、t o ne ta 1 2 0 0 0 ；g u p t a ，s h m m ae ta 1 2 0 0 0 ) 。 确定体系结构后需要针对专门的应用生成指令集。这个指令集被用于代码 综合和硬件综合步骤。指令集生成的方法可以分为指令集综合方法和指令集选 择方法。在指令集综合方法中，基于应用需求为专门的应用综合指令集，根据 需要的微操作和它们的使用频率进行量化，如( h u a i l ga n dd e s p a i n1 9 9 5 ) 、( c h o i ， p a r ke ta 1 1 9 9 8 ) 和( g s c h 谢n d1 9 9 9 ) 。在指令集选择方法中，使用指令的扩展集 ( s u p e r s e t ) 在体系结构约束内选择满足性能需求的子集，如( a l o m a d r ，n a l c a t ac t a 1 1 9 9 3 ) 、( b i i l l l ，i m a ie ta 1 1 9 9 6 ) 、( l i e m ，m a ye ta 1 1 9 9 4 ) 和( s h u ，w i l s o ne ta 1 1 9 9 6 ) 。 生成指令集后需要对代码进行综合以获得目标代码。代码综合方法可以分 为可重构代码生成器方法和可重构编译器方法两种。可重构代码生成器方法将 体系结构模板、指令集体系结构和应用作为输入生成目标代码( 图1 2 ) 。这种 方法的实例包括( w i l s o n ，骶、v a le ta 1 1 9 9 4 ；心e u z g o t s c m i c he ta 1 1 9 9 6 ； l e u p e r sa i l dm a 刑e d e l19 9 6 ；p r a e t ，l a n n e e re ta 1 19 9 6 ；h a i l o n 0a n dd e v a d a s 1 9 9 8 ) 。所有这些方法试图解决如下的代码生成中的子问题：指令映射、资源分 配、绑定和调度。有些方法( ( l e u p e r sa 1 1 dm 锄e d e l1 9 9 6 ) 、( 融e u z e r ，g o t s c h l i c h e ta 1 1 9 9 6 ) ) 在生成代码时还会进行代码压缩。 图1 2 可重构代码生成器 第l 章绪论 可重构编译器方法则是将体系结构模板和指令集体系结构作为输入，生成 一个定制的编译器，由其为给出的高层语言描述的应用生成目标代码( 图1 3 ) 。 这些方法的实例如( h a t c h e ra n dt m l e rl9 8 8 ) 和( l e u p e r sa n dm a 蹦e d e ll9 9 7 ) 。与普 通编译器的运行阶段划分相似，用这种方法生成的编译器也包括程序分析、中 间代码优化和代码生成等阶段。不同的是，在中间代码优化阶段的优化策略根 据具体的体系结构应用组合进行裁剪。 图l ，3 可重构编译器 确定体系结构并生成指令集后，需要进入硬件综合步骤。根据给定的a s i p 结构模板及指令集结构，从v e l o g h d l 描述开始，使用标准工具进行硬 件实现( j a i n ，b a l a 妯s 1 1 1 1 a ne ta 1 2 0 0 1 ) 。目前商业上常用的高层综合工具的基本目 标都是面向嵌入式微处理器( 包括数字信号处理器) 的a s i c 市场( 杨君2 0 0 6 ) 。 综合过程可以完全自动化，也可以在流程中插入新的约束，主要表现为包括模 块选择、模块调度、资源分配和模块间互连综合的粗粒度约束和包括操作调度、 操作与评估的映射等细粒度约束。但这些工具大多要求提供预定义的体系结构， 所以还不能完全满足a s i p 设计的需求。 1 4a s l p 验证的研究动机与目标 a s i p 作为面向专门应用领域的处理器，既继承了通用处理器的编程能力， 也具有a s i c 对专门应用的高效性，是两者在灵活性、能耗、性能等方面的折 中。但是这种灵活性也造成了验证上的困难。传统的面向g p p 的形式化验证方 4 第l 章绪论 法通常是基于由抽象的i s a 模型的细化关系组成的属性集合( l o i t z ，w e d l e re ta 1 2 0 0 8 ) 。专用的指令集结构使其不具有建立好的、成熟的指令集结构和属性规范， 难以像通用处理器一样直接根据已有的属性集合对设计进行检验。同时随着 a s i p 应用范围的不断扩大，a s i p 复杂度和规模持续增加，要求的设计周期和 上市时间却不断缩短。因此，如何有效地开展a s i p 设计的验证工作成为业界 面临的一个瓶颈。 传统的处理器验证主要是在寄存器传输级或更低层次进行的。在基于体系 结构描述语言的a s i p 设计中，这种验证方法很不方便，且容易产生错误 ( c h a n o p a d h y a y ，s i l l l l ae ta 1 2 0 0 6 ) 。我们针对这一需求，构建了一个形式化的 a s i p 验证框架，对体系结构的正确性进行检验，从设计初始阶段就可以开展对 设计的正确性的验证工作。 传统的验证主要采用仿真方法对设计出的电路或寄存器级的设计进行验 证。在这些阶段的设计规模较大、结构复杂，需要的验证实例的数目随着电路 规模的增加呈指数增长，花费的验证时间较长，发现错误后返工的时间也较长。 采用形式化方法( c l d ( ea n dw i n g1 9 9 6 ) 则可以从体系结构层次开始对设计进行 验证，避免将错误带入后续的设计阶段，对错误的修改也相对简单。 基于数学模型和方法，形式化方法( c l a r k ea n dw i n g1 9 9 6 ) 通过对执行模型 和需要满足的属性的一致性检验进行系统验证。形式化验证方法中最常用的是 理论证明( c y r l u k1 9 9 3 ；s a w a d aa 1 1 dh u m1 9 9 7 ) 和模型检测方法( c l a r k ea n dw i n g 1 9 9 6 ) 。在已有的形式化验证研究中，多数研究成果是基于理论证明方法展开的， 如( t a h a ra i l dk l l n l a r19 9 8 ；h o s a b e t t i l ，s r i v 嬲e ta 1 19 9 9 ；j a c o b i 姐d e n i i l g2 0 0 0 ； k 囊u f m a ma i l dr 邯s i n o f j f 2 0 0 0 ；r a ya n dh u n t2 0 0 4 ) 。理论证明方法为模型和属性 建立公理体系，使用定理证明系统，运用公理和已经证明的定理对属性表示成 的定理进行推导以证明设计的正确性。但由于涉及很多数学推理方面的知识， 需要用户有很强的数学功底，这也是这种方法不能推广的一个原因。定理证明 系统的运行过程中通常还需要进行人工制导，难以自动化完成。模型检测( m o d e l c h e c k i n g ) 方法( m i s h m ，d 眦e ta 1 2 0 0 l ；m i s h r a t 0 m i y a m ae ta 1 2 0 0 4 ) 提取模型 的全部状态，采用二叉判定树( b d d ) 表示状态集合，用深度优先和广度优先的 方法搜索状态转换图。如果属性得到满足，模型检测方法会返回正确结果；如 果属性无法被满足，模型检测方法会给出一个反例，指出不满足此属性的一条 状态转换路径，便于设计人员检查模型。状态搜索技术比理论证明更容易用计 算机实现，搜索过程通常不需要进行人工干预，具备自动化的特征。目前已有 一些模型检测器应用在实际的硬件设计验证中。模型检测方法的不足之处在于 其受限于状态空间的规模，过大的状态空间规模会产生状态爆炸问题，剪枝算 第l 章绪论 法是模型检测算法的主要研究内容之一。 在a s i c ( a p p l i c a 虹o n s p e c i 矗ci n t e 掣砸e dc i r c u i t ) 和g p p ( g e n e r 8 2 p t 珥，o s e p r o c e s s o r ) 芯片的物理设计验证中，已经有一些形式化的研究的尝试( t 如a r 距d k 啪a r19 9 8 ；h o s a b e n u ，s r i v a se ta 1 19 9 9 ；j a c o b ia n dk r o e l l i n g2 0 0 0 ；k a u f m 锄 a n dr u s s i n 0 行2 0 0 0 ；j h a l aa n dm c m i l l a i l2 0 0 l ；j a c o b i2 0 0 2 ；r a ya n dh u n t2 0 0 4 ； w i n k e i m a n n ，研i u se ta 1 2 0 0 4 ；m j s h r aa 1 1 dd u t t2 0 0 5 ；k 0 0a n dm i s h r a2 0 0 8 ； m i s l 】r aa i l dd u t t2 0 0 8 ；k d oa n dm i s h r a2 0 0 9 ) 。但一方面，这些形式化验证的研究 主要针对底层设计进行；另一方面，这些形式化验证方法通常基于由抽象的i s a 模型的细化关系组成的属性集合。与传统的a s i c 和g p p 具有固定的指令集和 低层详细的属性集合相比，a s i p 的设计更具有灵活性，需要根据应用需求对逻 辑结构和指令集进行调整，难以拥有固定的属性集合。一条a s i p 指令可能包 括许多经典的s c 指令，同时还会依赖于实际的数据通路配置，指令可以按 照很多种方式配置的操作序列定义，因此验证起来更加复杂。现有的a s i p 验 证多