（计算机系统结构专业论文）基于petri网的asip体系结构形式化建模和验证.pdf

独立完成与诚信声明 本人郑重声明：所提交的学位论文，是本人在指导教师的指导下，独立进 行研究工作所取得的研究成果。尽我所知，文中除特别标注利致谢的地方外，学 位论文中不包含其他人或集体己经发表或撰写过的研究成果，也不包含为获得巾 国科学技术大学或其它教育机构的学位或证书所使用过的材料。对本文的研究做 出重要贡献的个人和集体，均己在文中以明确方式标明。本人完全意识到本声明 的法律结果由本人承担。 签名：地日期：盐6 ：6 ： 关于学位论文使用授权的说明 本人完全了解中国科学技术大学有关保管、使用学位论文的规定其中包 括：学校有权保管、并向有关部门送交学位论文的原件与复印件；学校可以 采用影印、缩印或其它复制手段复制并保存学位论文：学校可允许学位论文被 查阅或借阔；学校可以学术交流为目的，复毒峨送和交换学位论文；学校可 以公布学位论文的全部或部分内容。 ( 涉密的学位论文在解密后应遵守此划定) 签名：必日期：逸j = 6 一 彦一6 么 中国科：攀技术入学硕上毕业论文 中文内容摘要 随着大规模集成电路工艺的不断提高以及嵌入式系统功能需求等多方面要求的 日益增加，寻找正确有效地进行嵌入式系统设计的方法成为种普遍需求，相关的 研究也被广泛地展开。 a s i p ( 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 s e tp r o c e s s o r s ) 是针对特定应用领域而设计 的，是兼具a s i c ( a p p l i c a t i o ns p e c i f i ci n t e g r a t e dc i r c u i t s ) ) 的高性能和g p p ( g e n e r a l p u r p o s e p r o c e s s o o 的灵活性的类特殊的处理器，在嵌入式系统中的应用越来越多。 我们采用的是基于体系结构描述语言( a d l ) 驱动的体系结构设讣空间搜索d s e 的a s i p 设计方法，因此，在设计初期保证设计的正确性，以及在整个自上而下的 设计流程中保证必要的属性被保留，即保证设计的一致性，可以减少后期改l e 或重 新设计的代价。业界在对设计正确性进行检验时主要是采用仿真的方法，但是由于 其固有的局限性，形式化方法被提出，并得到广泛的应用。 本论文在对国内外主要的形式化验证技术进行深入研究的基础上，结合a d l 驱动的a s i p 设计流程的特点，提出一种基于p e t r i 网的形式化建模和验证技术。主 要工作如下： 提出p n p ( p e t r in e tr e p r e s e n t a t i o nf o rp i p e l i n em o d e l i n g ) 模型，给出其定义和 建模方法，以及p n p 模型中的层次和等价等概念，用于基于模型的验证。 提出了两种基于p n p 模型进行a s i p 验证的方法，一是使用已有的模型检验工 具，用于系统状态相关的验证；另一个是基于p e t r i 网模型的仿真，用于系统行为相 关的验证。 最后，我们将基于p n p 模型的建模及验证与我们的设计开发环境相结合，提出 了由x p a d l 体系结构描述自动生成p n p 模型的方法，以满足设计流程对形式化建 模的要求。 上述研究，对构成完整的a s i p 体系结构设计环境有重要的意义。 关键词：a s i p 体系结构设计、形式化验证、p e t r i 网、时序逻辑 中国科：学技术大学硕上毕、l p 论文 a b s t r a c t t h eg r o w i n gc o m p l e x i t yo fe m b e d d e ds y s t e m st o d a yd e m a n d sm o r es o p h i s t i c a t e d d e s i g na n dv e r i f i c a t i o nm e t h o d o l o g i e s s y s t e mi n t e g r a t i o nl e v e l sh a v ei n c r e a s e da sm o r e f u n c t i o n a l i t i e sa n df e a t u r e sa r er e q u i r e df o rt h ep r o d u c tt os u c c e e di nt h em a r k e t i ti s c r i t i c a lt oe s t a b l i s he f f e c t i v ev e r i f i c a t i o nt e c h n o l o g i e sf r o mt h es y s t e ml e v e l ，a l lt h ew a y d o w nt ot h ei m p l e m e n t a t i o n s a p p l i c a t i o ns p e c i f i c i n s t r u c t i o n - s e t p r o c e s s o r s ( a si p s ) ，i n b e t w e e nc u s t o m a r c h i t e c t u r e ss u c ha sa p p l i c a t i o ns p e c i f i ci n t e g r a t e dc i r c u i t s ( a s i c s ) a n dc o m m e r c i a l p r o g r a m m a b l ep r o c e s s o r ss u c ha s g e n e r a lp u r p o s ep r o c e s s o r s ( g p p s ) ，a r ed e s i g n e d s p e c i f i c a l l y f o rap a r t i c u l a ra p p l i c a t i o no rs e to fa p p l i c a t i o n s au n i f i e da r c h i t e c t u r e d e s c r i p t i o ni s u s e d b o t ht oc o n d u c tt h ed e s i g ns p a c ee x p l o r a t i o n ( d s e ) a n dt h el a t e r s y n t h e s i s t h e r e i sag r o w i n gd e m a n df o rd e s i g nm e t h o d o l o g i e st h a tc a ny i e l dc o r r e c t d e s i g n so nt h ef i r s tf a b r i c a t i o nr u n a tp r e s e n t ，t h eb e s tt o o l sa v a i l a b l et oe n g i n e e r sf o r f i n d i n ge r r o r sb e f o r ef a b r i c a t i o na r es i m u l a t o r s t h e i rw i d e l yk n o w ns h o r t a g er e n d e r e d t h ep r e v a l e n c eo ff o r m a lv e r i f i c a t i o n t h i sp a p e rf i r s ta d d r e s s e ds o m et y p i c a lf o r m a lv e r i f i c a t i o nt e c h n i q u e s ，u p o nw h i c h o u rn e wm o d e l i n gm e t h o di sp r e s e n t e d t h em o d e lb a s e do np e t r in e ta n dc h a r a c t e r i z e d t h ek e yi s s u e si na s i pd e s i g n w i t hh i e r a r c h i c a la n dm o d u l i z e da b s t r a c t i o n ，t h em o d e li s c o m p a c ta n de x p r e s s i v e ，m e a n w h i l er e s u l t si nt h ef a c i l i t i e s t ou s es o m eu p t o d a t et o o l s f o rc e r t a i nv e r i f i c a t i o n a n o t h e rv e r i f i c a t i o nm e t h o db a s e do np e t r in e ts i m u l a t i o ni sa l s o i n t r o d u c e da sac o m p l e m e n tt ot h ef o r m e ro n e w ea l s oh a v ec l u e dt h el i a i s o nb e t w e e nx p a d la n dp n pm o d e l ，w i t ht h ep r o c e d u r e t ot r a n s f o r ma na r c h i t e c t u r ed e s c r i p t i o nt oah i g ha b s t r a c tl e v e lo fp n pm o d e l a l lt h em e t h o d sa n di d e a sa b o v et o g e t h e rh e l pt oc o m ns h t u t eac o m p r e h e n s i v ea s i p a r c h i t e c t u r ed e s i g ne n v i r o n m e n t k e y w o r d ：a r c h i t e c t u r ed e s i g n 、f o r m a lv e r i f i c a t i o n 、p e t r in e t 、t e m p o r o ll o g i c 2 中国科：学技术大学硕上毕j l k 论文 第一章绪论 本章从总体上对a s i p 的应用背景及设计流程进行介绍。说明了a s i p 设计的特 点及需求，从而引出了形式化验证的必要性。在本章的最后，给出了全文的组织结 构。 第一节a s i p 及其设计流程简介 近年来，嵌入式计算机系统己被广泛地应用于航空航天、武器装备、机器人、 通信设备、工业控制、汽车、船舶直至个人电了等广阔的领域，形成了巨大的产业 规模。巨大的市场需求推动了嵌入式系统向更高的技术水平发展，系统设汁的复杂 性对设计自动化以及验证工具也提出了进一步的需求。 摩尔定律指出，至少在未来的几十年里，各种数字电路的功能性和复杂性将持 续增长；与此同时，系统级设计技术的进步却跟不卜- 底层工艺的进步，这一技术差 距成为嵌入式系统发展中的一个瓶颈。对于面向特定应用领域的嵌入式系统，如果 使用传统的通用处理器作为系统的处理功能单元核心，会存在下面的问题：一方面， 通用的指令集通常不能很高效的完成系统功能，例如在多媒体应用中需要加大浮点 计算功能的力度；另一方面，通用处理器通常无法达到嵌入式系统发计中的低功耗 和有限芯片面积的约束。如果使用专用集成电路a s i c ，虽然可以很好的满足性能、 功耗的约束，但同时又带来了新的问题：a s i c 的专用性意味着适应不同应用需要 的灵活性较弱，系统开发周期远远超出使用通用处理器。嵌入式系统需要快速上市 极大地局限了a s i c 的实用性。 为权衡二者的优劣，定制指令集处理器a s i p 应运而生。它针对特殊应用领域， 以已有的处理器( g p p 或者a s i p ) 为模板，根据实际需求进行指令集裁减，并进 一步最大限度的整合硬件资源，从而满足特定的性能和非功能性的要求。 图一是典型的s o c 设计流程。首先，设计者根据应用需求和备选的i p 库，将 系统的功能按照软件实现和硬件实现进行初步划分，并使用a d l ( a r c h i t e c t u r e d e s c r i p t i o nl a n g u a g e ) 对s o c 体系结构模板进行臼然而简单的定义。s o c 中的模块 根据电子杂志“e s ld e s i g nc o r n e r ”2 0 0 6 年对电子电路发汁的统汁和分析报告。 - 5 - 中国科学技术大学硕士毕业论文 可能包含处理器、存储器、a s i c 、1 1 0 接口电路以及互连结构( 例如总线) 等，而 每个模块又可能包含多种结构，比如处理器，就可能是r i s c 处理器、vl 1 w 处理 器、超标量处理器、a s i p 或是具有不规则数据通路结构的d s pj ! j = 片。 然后，利用a d l 描述驱动软件工具包的自动生成。生成的软件可能包括编译 器、仿真器等。编译器进行指令调度时需要的信启、，如指令级并行的冲突信息等， a d l 都可以进行描述。仿真器可以用于刁；同的仿真目的，如评估性能和功耗、分析 资源利用率、硬件功能验证、软件调试或软硬件协同凋试等。因而生成的仿真器也 可能是多种多样的，如功能级，指令级，阶段精确的，周期精确的仿真器等。 一方面，我们利用生成的软件工具包对应用软件进行开发设计，评估不同实现 的优劣；另一方面，利用反馈的应用特性对指令集进行修改，通过调整相应的a d l 描述，以支持对a s i p 指令集体系结构的设计空间搜索。 当整个系统的性能评估达到特定的需求时，便进行后期的综合和实现。 该设计流程的两个主要特征一是软硬件协同设计，它使得对指令集进行裁减的 过程涵盖了对上层软件应用和底层硬件资源的综合考虑，并同时进行对软件和硬件 的设计；二是基于体系结构描述语言驱动的d s e ，它可以在一定程度上支持软件工 具的自动生成。 我们知道，随着电路综合工艺的不断提高，在设计后期发现某些设计初期引起 的错误并进行修改的代价是庞大的。虽然通过可编程技术，可以将这一代价在一定 范围内减少，但至少在当前，如何在设计初期便发现错误以避免这一代价的需求与 日俱增。该方法在性能和面积上占绝对劣势。 当前，设计工程师用以发现错误的工具主要是仿真器，它通过预先拟定的或随 机的输入模式来检查系统行为是否满足实际需求。然而仿真器有两个弊端：一个是 输入模式集合往往不足以暴露所有的系统错误，二是其对正确性行为的定义有着很 大的局限性。在这种情况下，学术界和工业界开始加强研究并尝试采用形式化的方 法来进行软硬件系统的验证。 形式化验证基于数学的模型与方法，通过证明抽象说明( s p e c i f i c a t i o n ) 与设计 实现( i m p l e m e n t a t i o n ) 的对应关系来验证系统的正确性。形式化的方法采用无二义 的形式化语义来描述说明与实现，并证明实现满足全部或部分的说明。同时尽可能 的使用c a d ( c o m p u t e r a i d e dd e s i g n ，计算机辅助化设计) 来缩短验证的时间并提 高验证方法的可用性。如果形式化验证的方法与设计流程配合的很好的话，可以大 - ： - 国科学技术火学硕二l 毕业论文 大加强验证有效性。当然，如果不能在全过程中使用形式化的方法，可以采用形式 化的手段来描述需求或对高层进行抽象，这种精确的描述对于系统设计的正确性至 关重要。 当然，形式化验证的方法不是万能的。即使验证了设计的网表模型满足形式化 需求也不能完全保证最后得到的设计可以按照意图工作。这是因为，首先设计者的 意图不能被完全形式化；还有就是形式化验证时一般需要许多的假设条件，但是存 真实环境中这些假设不一定都满足；最后，形式化方法虽然借助c a d 工具，但是 多是由数学与验证的专家来操纵，有的时候还必须手动完成部分操作，如何提高形 式化工具的自动化还是个问题。 图1 基于a d l 语言的s o c 设汁流程 需求和目标简介 第二节形式化验证简介 由于形式化验证本身的局限，当前，其成功的应用及实现主耍在于数字电路设 计的验证、协议验证和类型系统中。其他关于验证的研究和方法大都仍处于一个探 索和实验的阶段。也就是说，并没有一种标准的体系结构层次的形式化验证方法可 以为我所用。本论文的主要贡献，并不是设计出一种完全新型的形式化验证方法， 而是基于已有的验证理论和工具，给出了实用ta s i p 设计的建模、验i i f 的系统的 方法。在介绍我们的方法之前，需要对形式化验证技术的关键问题进行一些交待。 中国羊= 学技术大￥碗上堆、i h 论文 在一个形式化验证的系统中，包括三个基本的概念。首先，我们需要一个模型， 即使用基于数学和逻辑来刻画我们要验证的对象，它口r 以看成是实际系统在抽象领 域的一个镜像。为了使这样一个镜像有意义，我们需要一个在其所在的数学抽象领 域的一套理论，它用于推倒模型在该范畴的所有可能的以及正确的 亍为。通过观察 这些断言，决定特定的系统行为是否有意义，因此，还必须有一个严谨的方法来比 较和判断系统行为是否满足正确性约束。 a s i p 的设计流程多采用软硬件协同设计的方式。首先，根据应用需求分析，进 行初期的设计，并将需要实现的功能向下层逐渐过渡，i 耐确保下层的实现机制确 实可以完成上层期望的功能。再根据仿真及验证的评估反馈信息对上层描述及实现 机制进行阔整。因此，整个设计流程同时涉及了软件证明和硬什验证的问题。在形 式化验证领域，软件- 正明和埂件验证有着完全不同的内涵和机制。其区别主要体现 在以下几点： ( 1 )硬件电路的可达状态总是有限的，虽然在很多情况下会存在状态空问爆炸 问题，而程序的状态空问通常是无限的。 ( 2 )由于程序证明是在硬件和编译器之上进行的，因此实现机制的改变可能影 响系统的语义。而硬件证明基于差分方程或是电路的数字抽象( 如有豫状态机) ，因 此更接近于真实世界。 ( 3 )程序通常是终止的，且并行度总是有限的，或者说是在一个可以掌握的范 围内。而硬件通常是反应式的( r e a c t i v e ，1 i 终止) ，计+ 行发生的门的行为的数量级 是手动无法操作的。 ( 4 )由于上面的本质区别，在数学领域，它们所依赖的基础逻辑丁具也是不同 的，通常，程序证明依赖于h o a r e 逻辑，而硬件验证使用时序逻辑。 体系结构层次的验证是为了在设汁早期发现井处理设计方案的捅洞以保证后期 综合的正确性。我们借助于p e t r i 网，对其进行扩展，使其可以对流水化的处理器 的存储部件和执行部件进性简洁直观的描述。通过层次化抽象技术使其可以很好地 刻画流水线处理器的行为，有效控制验证空间的规模和复杂度；同时，我们在验证 中引入了对已有的成熟的验证工具的使用该工具不能直接用于体系结构层次的验 证，但是通过我们p n p 模型层次间抽象及转化，可以为整个验证提供极大的便利。 下面，我们首先需要对本沦文相关的p c t r i 网及硬件验证技术做个简单介绍。 中国科! 攀技术人。7 ：硕上毕j i k 论文 二、背景 很多模型被提出用以表示软硬件协同设计的系统，尤其被广泛使用的工具是 p e t r i 网。m a c i e l i 】使用p e t r i 网作为软硬件协同设计的中间模型，给出了一个形式 化的定性及定量分析方法来执行软硬件划分。它使用扩展的p e t r i 网来分析分离过程 ( p a r t i t i o n i n gp r o c e s s ) 中的负载平衡，共享互斥和通讯代价等属性，可以同时对多 个软件部件进行分析，并对底层硬件面积进行评估。s t o r y 2 给出了一种带有受限变 迁规则的时序p e t r i 网来表达软硬件中控制流的建模方法。【3 给出了一个用以检查 安全网的模型，而 4 】给出了一个分析和验证有界p e t r i 网的方法，它们都使用b d d 来表示标识集。 和p e t r i 网模型样被广泛用于软硬件协同设计的另一类方法主要采用有限状 态机模型和时序逻辑公式。 5 】提出了一种协验汪的方法，它利用线性混合自动控制 模型，通过将复杂系统分解成单个硬件、软件和接口进行分析和验证，来处理状态 空间爆炸问题。b a l a r i n 6 介绍了一种基于协同设计有限状态机c f s m 的方法，它将 c f s m 转化成传统的状态自动控制以检查是否所有可能的输入输出序列均满足系统 属性。 7 】提出的验证框架则以一个分解的系统为输入，评估c t l 和t c t l 公式， 以检查行为和时序属性。 除此之外，很多相关研究领域使用了多种不同的形式化模型和方法，下面我们 对具有代表性的几种技术进行简单的介绍和比较。 1 离散事件模型 在离散事件模型 3 2 】中，进程之间的通讯采用多个进程写，单个进程读的策略， 其中每个事件都是带有时间标记并且全局有序的。冈为离散事件模型是明确带有时 间标记的，它比较适合模型执行和仿真。然而离散事件操作模型对时间戳要进行排 序，是很消耗时间的，它主要适合那些大的，有频繁空运转和自动操作的系统，因 为离散事件模型仿真器通常对发生变化的系统执行，而不是针刘整个系统。 进程的行为用时序语言描述，只要有输入事件进程就执行，并且产生带有相同 或是比输入事件大的时间标记的输出事件。对于多个进程的执行，如果它们的事件 的时间标记是一样的，它们的执行顺序没有给出说明。不同的离散事件模型仿真器 采用的策略是不同的。 叶i 国科学技术大学硕上毕业论文 离散事件模型的执行是非常低效的，因为必须要通过离散事件模型仿真器的上 层模块调度从而确保仿真和执行行为的一致性。数字硬件通常用离散事件模型实现， 例如v e r i l o g 语言就被设计成离散事件模型仿真器的输入语言，v h d l 语言也是离 散事件操作模型的一个实现。 2 数据流进程网络模型 在数据流进程网络( d a t af l o wp r o c e s sn e t w o r k s ) 3 3 模型中，一个程序被表示 成一个有向图。节点( 也称为角色) 代表操作，而弧线( 也称为令牌) 代表事件在 全局的顺序。有很多等同于数据流的语言已经开发出来了，比如：k a r pa n dm i l l e r s c o m p u t a t i o n g r a p h s ，l e ea n dm e s s e r s c h m i t t ss y n c h r o n o u sd f g s ，l a u w e r e i n se ta 1 s c y c l o s t a t i cd a t a f l o wm o d e l 。 进程之间的通讯采用的是单个进程读、单个进程写，带有局部有序标志( 令牌) 的通道。在数据流进程网络中，进程的行为被详细说明为该进程的发射序列，在每 次原子发射中，进程会消费掉一些令牌，同时随着顺序执行语言中的行为会产生相 应的令牌。一个进程是不能测试输入通道为每一次发射所需要的令牌数的，因此采 用一种阻塞的读限制来确保行为的确定性。同时必须遵循令牌的生产和消费过程中 所强加的偏序限制。正因为数据流没有明确的时间，因此数据流模型不过多的限制 操作过程中的执行顺序。由于进程之间的互连，数据流网络模型不能进行组合。而 自由的选择发射顺序，使其执行非常有效。 3 有限状态机模型f s m 有限状态老f l 3 4 ，3 5 可分为同步有限状态机和异步有限状态机。 在同步有限状态机( s y n c h r o n o u sf i n i t e s t a t em a c h i n e s ) 模型中，进程之问的通 讯是采用一种共享变量的机制，进程的读和写都是在零时间内完成的，操作和通讯 都是在瞬间完成的。进程的行为被详细说明为一种有限的带有标记的转换系统，其 中在状态转换中任何对状态都是被标记为带有输入变量和输出变量的。同步有限 状态机模型的组合相对是比较容易的，因为f s m s 的互连能够被i 剥步组合成另一个 f s m 。然而，在很多系统中，该模型所假定的零操作和通讯延迟是非常网难和低效 率的。 在异步有限状态机( a s y n c h r o n o u sf i n i t e s t a t em a c h i n e s ) 模型中，进程之间的 通讯采用通道来确保通讯双方同时发生。除了这种经由通道的同步之外，两个异步 噜，国科：学技术火：擎硕上毕、l k 论文 的f s m 通常不在同- - b , - j - i 司执行一个转换。异步有限状态机的执行比同步有限状态 机要容易一些，但在某些需要处理同步机制的系统中会有些问题。 此外，针对特定应用还定义了二些特殊的有限状态机，如a c f s m 3 6 ， e c f s m 3 7 等。 4 理论证明 理论证明实际上是通过数学推导检验一个m p l e m e t a t i o n 是否满足s p e c i f i c a t i o n ， 通常它的证明模型是下面的过程： 广 i m p i ： 这里的i m p 和s p e c 一般被描述为形式化的逻辑公式。由上面的过程可以看出， 潞幽 证明方法有两种：一种是证明i m p 能够嘻豪后者，一种是证明两者等价。 一个理论证明系统包括两个集合：一个公理集合和一个推理规则集合。公理集 合包括几个核心的理论和由其推出的许多的定理，是验证的基础。推理规则是验证 进行推理证明的必要支持，通过很多的策略来对证明作指导，例如：根据已经被证 明过的或事先定义过的定理来重写论证结果，或者移除一些不必要的全局变量，达 到简化的目的等。 理论证明具有严谨的数学基础，高度的抽象化能力和强大的逻辑描述能力。然 而，理论证明的过程必须在专家指导下完成，属于半自动化证明系统类，且由于其 对数学能力的要求，仅仅适用于专家或者有经验的人群。当前被比较广泛地应用于 研究的理论证明系统包括：b o y e r m o o r e 3 8 】，h o l 3 9 】，p v s 4 0 ，l a m b d a c a l c u l u s 4 1 1 ，a c l 2 1 4 2 等。 5 a u t o m a t a 通常，把根据输入可以决定输出的系统抽象为自动机模型，它是具有不依赖于 输入大小且具有固定存储空间的数学模型。被模型化的系统一般分为有限运行与无 限运行两种情况，在考虑自动机时，则分为在有限词卜的自动机与在无限词卜的自 动机。自动机的般形式是五元组a = ( ，q ，6 ，q o , f ) ：是有限字母表集合。 q 有限状态集合。5 c _ q x e x q 是转移关系。e o e 是初始状态集合。f e 是 1 1 困 ： 中国科学技术大学硕士毕业论文 结束状态集合。 用自动机来做模型检查的一个主要优点是系统的模型与要验证的描述都町以用 自动机来表达。在多数情况下，用a u t o m a t a 验汪时可以找到一个有条理的算法来使 验证能完全自动完成，而且这些算法有反例机制。这一特性使得调试更加容易控制， 更适用于实际应用。 然而，自动机系统通常只能为某些逻辑和模型进行验证。比如：为验证基- 丁 k r i p k es t r u c t u r e s 的c t l 公式所设计的算法和为验证基于f a i rt r a n s i t i o ns y s t e m s 的 l t t l 公式所设计的算法就有很大差别。对a u t o m a t a 提出一种统一的模型验证策略 已经起步，但是真正实现还有很多工作要做。 目前比较常见的几种自动机模型包括：b t i c h i 自动机 4 3 ，4 4 ，4 5 ，a b t a 4 6 】， t i m e da u t o m a t a 4 7 51 ，h y b r i da u t o m a t a 5 2 ，5 3 ，a l t e r n a t i n gt r e ea u t o m a t a 5 4 ，55 等。 6 p e t r i 网 p e t r i 网【8 ，9 ，1 0 是一种网状的信息流模型。包括条件和事件两类结点，在条件和 事件为结点的有向二分图基础上添加表示状态信息的托肯( t o k e n ) 分布，并按引发 规则使得事件驱动状态演变，从而反应系统动态运行过程。通常情况下，用小矩形 表示事件( 称作变迁) 结点，用小圆形表示条件( 称作位置) 结点，变迁结点之间、 位置结点之间不能有有向弧，变迁结点与位置结点之间连接有向弧，由此构成的有 向二分图称作网。网的某些位置结点中标上若干t o k e n ，从而构成p e t r i 网。其形式 化描述如下。 定义1 三元式n = ( p t ；f ) 称作网当且仅当： ( 1 ) put ，pnt = ； ( 2 ) f ( p t ) u ( t 尸) ； ( 3 ) d o m ( f ) u c o d ( f ) = p u t 这里，p 表示位置结点集合，t 表示变迁结点集合，f 为位置结点与变迁结点问 的有向弧集合。 定义2 四元式p n = ( p , t ；f ，m o ) 称作p e t r i 网当且仅当： ( 1 ) n = ( p ，t ；f ) 是一个网； ( 2 ) m ：p - ) z ( 非负整数集) 为标识( 也称状态) 函数，其中，m 。是初始标识； ( 3 ) 引发规则： 1 ， i j = 1 国科学技术大学硕士毕、1 p 论文 a ) 变迁t t 称为使能的( e n a b l e d ) 当且仅当：v p t ：m ( p ) 1 ，记 作m t ； b ) 在m 下是使能的变迁t 可以引发( f i r e ) ，引发后得到后继标识m ，则 m ( p ) + l ，p t 一t m ( p ) = m ( p ) 一1 ，p c t f 。 i m ( p ) ， 其他 记作m t m 。 直观的，我们希望使用p e t r i 网的基本元素对现实系统进行描述。通常，位置用 于描述可能的系统局部状态( 条件或状况) ，例如，计算机和通信系统的对流、缓冲、 资源等。变迁用于描述修改系统状态的事件，例如，计算机和通信系统的信息处理、 发送和资源的存取等。弧使用两种方法规定局部状态和事件之间的关系：它们引述 事件能够发生的局部状态；由事件所引发的局部状态的转换。 在p e t r i 网模型中，t o k e n 包含在位置中，它们在位置中的动态的变化表示系统 的不同状态。如果一个位置描述一个条件，它能包含一个标记或不包含标记，当一 个标记表现在这个位置中，条件为真；否则，为假。如果一个位置定义个状况， 在这个位置中的标记个数用于规定这个状况。 一个p e t r i 网模型的动态行为是由他的实施规则( f i r i n gr u l e ) 规定的。如果一个 变迁的所有输入位置至少包含一个t o k e n ，那么这个变迁可能实施( 相联系的事件有 可能发生) 。对这种情况，这个变迁称为司实施。一个可实施变迁的实施导致从他所 有输入位置中清除一个标记，在它的每一个输出位置中产生一个标记。当使用大于 l 的弧权( w e i g h t ) 时，在变迁每一个输入位置中都要包含至少等于连接弧权的标记 个数，它才实施：这个变迁的实施，要根据相连接的弧权，在它每个输出位置中 产生相应标记个数。变迁的实施是一个原子操作，在输入位置中清除标记和在输出 位置中产生标记是一个不可分割的完整操作。 p n 模型的状态转换是局部的，它仅涉及一个变迁通过输入和输出弧连接位置 的状态变化。这是p n 模型的一个关键特性，利用这个特性可以容易描述并行、分 布系统。 很多研究和应用基于p n 模型展开 5 6 6 3 】。p n 模型以研究模型系统的组织结构 和动态行为为目标，着眼于系统中可能发生的各种状态变化以及变化之问的关系。 p e t r i 网易于表示系统变化发生的条件及变化发生后的系统状态，但不易表示系统中 中国科学技术大学硕士毕业论文 数据值或属性的具体变化或运算。在大型、复杂系统的模型中，p e t r i 刚应用的主要 困难是模型状态空间的复杂性问题，它将随实际系统的规模增大而呈指数性增长。 因此，很多领域针对不同系统特性对p e t r i 网进行了扩展 6 4 6 9 。 本论文的一个主要贡献在于：如何使用层次化抽象技术，在使用p e t r i 网对体 系结构关键元素流水线进行建模的同时，可以保证他的复杂性被很好的控制。 7 模型检查( m o d e lc h e c k i n g ) 模型验i 正 7 0 7 3 , 币f l 理论证明是系统验证中的两个主流的手段。他们的实质是利 用特定的数学手段来检查系统行为是否满足一定的属性要求。理论证明是基于严格 的公理系统和推导过程来完成的。对于系统设计上程师，往往提出了过高的数学能 力的要求，因而难以推广。模型检查的主要对象是系统的状态空间。他通过在整个 状态空间中的遍历检查，确定某逻辑公式是否在系统的所有状态可以被满足。模型 检查是由一定的自动化工具( m o d e lc h e c k e r ) 来完成的。因此它不需要系统设计者 和工程师具有很高的理论背景，但与此同时，穷尽的搜索方法通常与计算复杂度紧 密关联。因此使用这些自动化工具，我f f j 必须保证我们的输入模型的状态空间是很 大的。 m o d e lc h e c k e r 主要基于两大类理论。一是时序逻辑，主要包括计算树逻辑 c t l 7 4 ，7 5 1 ，和线性时序逻辑l t l 7 6 ，7 7 ；另一类是自动状态机( 各种a u t o m a t a ) 及由其引申的迹( t r a c e ) 理论。 基于树逻辑c t l 的模型检查方法最先分别由c l a r k ea n de m e r s o n 【2 4 】以及 q u i e l l ea n ds i f a k i s 2 5 1 提出。首先，由系统描述建立一个完整的系统状态空间图， 对时序逻辑公式所表达的属性进行检查的算法是基于将这个公式在状态图中扩散直 到取得一个连续函数的极值不动点。不需要证明公式对于整个状态空间成立，该方 法只需要涉及到一个特定的状态集合。对于分支时序逻辑，该算法的复杂度是可接 纳的。它不仅可以完全的自动化，而且当属性公式不成立时，可以找到一个反例。 对于线性时序逻辑l t l ，其属性检查的方法主要是将一个公式通过状态表 ( t a b l e a u ) 构造方法转化成一个自动控制。状态表中的每个状态对应该状态成真的 公式集合。因此它的状态空间的大小由公式集合的大小决定，而一i 是像c t l 那样由 系统大小决定。根据实际验证的需求对二者进行合理的选取甚至组合，叮以尽可能 地减小状态空间。 中国科学技术大：学硕士毕、i k 论文 基于自动状态机的证明则更多的依赖于等价的概念。将实际系统的行为和期望 的系统行为分别以状态机所表达的可接受的语言表示。通过检查两个语言间的可包 含性( c o n t a i n m e n to f t h el a n g u a g e ) ，来决定系统行为的正确性。在此基础上，一些 针对特定领域的技术被引出。其中，被广泛应用的是迹理论和进程代数理论。它们 对系统行为的历史轨迹进行观察和断言，从而完成属性检查。 p n p 模型中要使用模型验证，其主要原因是因为我们的属性描述是由时序逻辑 公式来表达的。此外，作为一项成熟的验证技术，对于底层的p n p 模型，可以借举 其他工具协助验证的完成。 第三节体系结构描述对象和验证目标 a s i p 设计在体系结构层次所描述的信启、，一方面，需要能够提供足够的行为信 息来生成仿真器，以评估设计过程中各种不同的配置和考虑的性能。一方面，需要 能够提供目标指令集和这些指令的语义，用于编译器后端的生成。此外，它还需要 提供信息处理后期的综合。 整个体系结构描述通常分为两部分：行为的描述和结构的描述。行为的描述包 括对指令及指令组合的描述、指令行为的描述、以及基本指令集中典型指令与目标 指令集中相应指令映射关系的描述。结构的描述包括对存储子系统的描述、流水线 和数据通路以及可能出现的各种冲突的描述、以及一些体系结构功能和控制子部件 的描述。 在a s i p 的设计流程中，通常由应用程序入手，抽取出系统需要完成的功能描 述，然后，从指令模版库中选取出合适的指令集来为这些功能提供支持。将待选的 体系结构作为系统模型，我们验证的目标就是该系统司以满足设计需求和属性描述 的约束。 体系结构验证的另一个关键因素是流水线的验证。现代处理器都南流水线实现， 它通过指令的重叠增加系统指令执行的吞吐量。这带来了另一个验证问题：指令的 流水执行是不是与单条执行的结果致。流水线的状态包括停顿、流动和n o p 等， 一些简单的流水线应满足的属性包括：指令在流水线中的动作是确定的，他们在流 水中顺序执行，不考虑流水线停顿，每条指令流出的周期数应该是一定的等。 已经提出很多用于流水线验证的方法，我们提出的模型基于p e t r i 网的直观和分 析能力，可以对体系结构的各种信息包括流水线的结构进行建模，并进步为验证 1s 中国科学技术大学硕士毕业论文 提供支持。 第四节论文组织结构 本论文的主要目的是针对a s i p 设讨流程中的验证需求，提出一套对系统设计， 尤其是体系结构层次进行验证的方法。该方法以基于p e t r i 网的扩展模型p n p 模型 为基础，通过提供层次化、模块化的描述和分析方法，允许系统设计者在设计初期 就可以对特定的系统行为进行检验。通过逐层向底层综合，对设计后期m 现的问题 也进行了考虑。这个验证的流程与a s i p 的设计流程紧密结合在起。 第一章概括介绍了a s i p 设计的背景和我们的形式化验证方法的意义。介绍了 当前该领域形式化验证的主要背景和论文中需要涉及的相关技术的理论基础，引出 了我们进行验证的需求和一些关键因素。 第二章从p n p 模型的形式化定义入手，举例说明了如何使用p n p 模型对流水 线行为建模。介绍了p n p 模型中的层次和等价概念，以及与传统p e t r i 网问的对应 关系。 第三章详细介绍了如何使用p n p 模型进行验证，主要介绍了两种方法，一种是 基于工具m o d e lc h e c k e r 的自动验证，通过一个简单的示例表明如何操作。基于状态 空间和高层抽象等考虑，给出种半形式化的基于p e t r i 网仿真的方法。并对如何生 成p n p 模型的仿真程序和输入实例，以及确保达到尽可能大的仿真覆盖度的分析手 段也作了分析。 第四章与我们整个a s i p 的开发环境相结合，说明了如何从a d l 描述中抽取 p n p 模型。使用x p a d l 作为体系结构语言，它是一种基于x m l 进行扩展的体系结 构描述语言。我们从它对体系结构中行为和结构的描述中抽取建立p n p 模型所需的 信息。并对具体过程进行了介绍。 第五章对本文所做的工作进行总结。 中国科学技术人丫：硕上毕、i k 论文 第二章p n p 模型及相关概念 本章从介绍p n p 模型的形式化定义入手，通过一个流水线建模实例说明了p n p 模型的主要特点。为了实现基于p n p 模型的验证，第二节介绍了p n p 模型中的层 次和等价的概念，从而指导如何从一个高层的模型得到细粒度的模型。第三节说明 了p n p 模型与传统p e t r i 网模型之间的对应关系，通过将底层的p n p 模型转化到传 统p e t r i 网模型，可以得到系统的状态空间，为后期的使用m o d e lc h e c k e r 工具进行 自动验证奠定了基础。 第一节p np 模型 p n p 模型的形式化定义 为了描述具有流水线结构的复杂处理器的行为，我们对传统的p e t r i 网进行了扩 展，扩充了基本p e t r i 网的托肯、变迁等概念，得到了一种新的p e t r i 网扩展模型一 一p n p 【1l ，1 2 ，该模型形式化定义如下： 定义3 一个托肯( t o k e n ) 是一个数对k = ，其中v 是托肯值，值可以是 任意类型( 如布尔、整数) 或是任意复杂性的自定义类型( 如结构体、集合、记录) 值的类型称为t o k e n 类型。集合k 表示一个给定系统所有可能的t o k e n 类型的集合。 r 是托肯时间，是一个表示托肯时间戳的非负实数，即r r 。 定义4 一个p n p 模型是一个五元组= ( p ，丁；f ，s ，m 。) ，其中 ( 1 ) p ： p 1 ，p 2 ，to ，p m ) 是一个有限非空库所( p l a c e ) 集； ( 2 ) t = ( t 1 ，t 2 ，t n ) 是一个有限非空变迁( t r a n s i t i o n ) 集： ( 3 ) ，p t u t p 是一个有限非窄的弧( a r c ) 集，定义库所与变迁之间的 流关系。 ( 4 ) ssp t 是一个有限非空的弧集，定义库所中的托肯对变迁的限制关系。 ( 5 ) m 。是网的初始标识( 定义5 ) 。 定义4 ( 3 ) 中的流关系称为“般弧”，以带箭头的连线表示(