（交通信息工程及控制专业论文）基于可编程逻辑的硬件平台的设计与形式化验证.pdf

中文摘要 摘要：安全硬件平台通过先进的计算机、电子技术来现实。随着计算机、电子技 术的迅猛发展，系统性能大大提高，结构也变得越来越复杂。安全硬件平台作为 安全苛求系统的重要部分，其安全性是至关重要的。在设计阶段就应充分考虑安 全性，以免由于潜在的设计缺陷导致整个系统存在安全隐患。由于系统逐渐向规 模大、性能强、复杂性高的方向发展，单纯利用仿真、测试等方法无法对系统进 行无穷验证，因此在硬件平台设计阶段，利用形式化方法对硬件平台设计的正确 性和完备性进行验证。 论文以基于通信的列车控制( c o m m u n i c a t i o n - b a s e x tt r a i nc o n t r o l ，c b t c ) 系 统为应用背景，详细分析了安全硬件平台需求。通过对比各种平台结构的优缺点， 选取了二乘二取二结构为本文设计的总体结构。在分析各种安全计算机结构的基 础上，结合c b t c 系统对安全硬件平台的功能需求，提出一种新的二取二系统结 构方案。 论文设计的安全硬件平台是以安全性、通用性为重点。论文详细介绍了保证 安全性、通用性和调度策略的具体功能实现方法。以微同步和硬件数据比较方式 来保证平台的安全性；以处理器的约束、数据帧结构的确定和接口格式的固定来 保证了平台的通用性。 安全硬件平台中的重要单元是安全比较核。安全比较核基于可编程逻辑设计 与实现。使用可编程逻辑不仅可以缩减电路的体积，提高电路的稳定性，而且先 进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中，将安全比较 核划分为不同的功能子模块，对每个子模块进行设计与实现，并且对仿真结果进 行分析，保证其设计基本正确。 仿真验证只能保证比较核的仿真结果正确，但对于复杂系统，无穷尽的仿真 是不现实的。为了避免存在潜在的设计错误，论文利用基于断言的方法( p r o p e r t y s p e c i f i c a t i o nl a n g u a g e ，p s l ) 对安全比较核进行形式化验证，对其内部设计的正 确性和完整性进行检验。当断言失败，发现设计错误时，对检验出的设计错误进 行分析、修改。再进行新的验证，直到形式化验证证明其设计没有潜在的设计缺 陷为止。 论文结果表明，对于基于可编程逻辑设计的安全硬件平台，利用断言对设计 进行形式化验证，可以检验出仿真无法检验出的错误，保证其设计的完整性和正 确性，从而得到一个无设计缺陷、通用的安全硬件平台。 本文用图5 7 幅，用表4 个，参考文献3 2 个。 关键词：安全计算机；二乘二取二；f p g a ：形式化验证；p s l 分类号：t p 3 0 9 1 a b s t r a c t a b s t r a c t ：t h es a f eh a r d w a r ep l a t f o r mi s a c c o m p l i s h e dt h r o u g ha d v a n c e d c o m p u t e ra n de l e c t r o n i ct e c h n o l o g y w i t ht h ed e v e l o p m e n to fc o m p u t e ra n de l e c t r o n i c ， t h ec a p a b i l i t yo fs y s t e mi n c r e a s i n gw h i l et h ec o m p l e x i t yi n c r e a s i n g h a r d w a r ep l a t f o r m 勰ai m p o r t a n tp a r to fs a f e - c r i t i c a ls y s t e m ，s a f e t yi sv i t a li m p o r t a n c e t h es a f e t yo ft h e h a r d w a r ep l a t f o r mm u s tb ef u l l yc o n c e r n e da tt h e d e s i g np h a s e , f o rf e a r t h e d i s f i g u r e m e n to fd e s i g nw i l lb er e s u l ti n t h eh i d d e ns a f e t yt r o u b l ee x i s t i n gi nt h es y s t e m d u et ot h es y s t e m sd e v e l o p i n gt ot h el a r g es c a l e ，h i g hp e r f o r m a n c e ，h i g l lc o m p l e x i t y d i r e c t i o n , i tc a nn o ta c c o m p l i s hw i t ht h es i m u l a t i o na l o n e s oi nt h ed e s i g np h a s eo f h a r d w a r ep l a t f o r m ，n e e dt ou $ et h ef o r m a lv e r i f i c a t i o nt ov a l i d a t ei t i ti sn e c e s s a r yt o v a l i d a t et h ec o r r e c ta n dt h em a t u r i t yo ft h eh a r d w a r ep l a t f o r m c b t cs y s t e mi st h eb a c k g r o u n do ft h i sp a p e r , a n a l y s i st h er e q u i r e m e n to f h a r d w a r ep l a t f o r m t r o u g ht oc o m p a r es o m ed i f f e r e n tk i n d so fp l a t f o r ma r c h i t e c t u r e , s e l e c tt h e2x2 - o u t - o f - 2a st h ed e s i g na r c h i t e c t u r e o nt h eb a s eo fa n a l y s i sa r c h i t e c t u r e o fs a f ec o m p u t e r , c o m b i n ew i t ht h er e q u i r e m e n to fc b t c ，p r o p o s ean e ws y s t e m a r c h i t e c t u r e s a f e t ya n dc u r r e n c ya r et h ee m p h a s e so ft h es a f eh a r d w a r ep l a t f o r mi nt h i sp a p e r t h em e t h o d st oa c h i e v es p e c i f i cf u n c t i o n a l i t yo fs a f e t y , c u r r e n c ya n ds c h e d u l i n g s t r a t e g ya r ed e s c r i b e di nt h i sp a p e r 1 1 1 es a f e t yo ft h ep l a t f o r mi se n s u r e db yn s eo ft h e m i c r o s y n c h r o n i z a t i o na n dt h ed a t a c o m p a r ew i t hh a r d w a r e t h ec u r r e n c yo ft h e p l a t f o r mi se n s u r e db yp r o v i s i o no f t h ep r o c e s s o r , d a t af l a m ea n di n t e r f a c e t h es a f ec o m p a r ec o r ei st h ei m p o r t a n tp a r to ft h es a f eh a r d w a r ep l a t f o r m t h e s a f ec o m p a r ec o r ei sd e s i g na n dc o m p l e m e n tb a s e do nt h ep r o g r a m m a b l el o g i c w i t h p r o g r a m m a b l el o g i cn o to n l yc a nc u tt h es i z eo fc i r c u i t ，b u ta l s oi n c r e a s et h es t a b i l i t yo f c i r c u i t w h i l et h ea d v a n c e dt o o l sw i l ls a v et h et i m eo fs y s t e md e s i g n i nt h ei m p l e m e n t p h a s e ，t h es a f ec o m p a r ec o r ei sd i v i d e di n t os o m es u b - m o d u l ew i t hd i f f e r e n tf u n c t i o n t oa c c o m p l i s ha n ds i m u l a t ea n ys u b - m o d u l ee n s u r et h er e s u l to fd e s i g nc o r r e c t t h ef o r m a lv e r i f i c a t i o no ft h ep l a t f o r mb a s e do na s s e r t t h es i m u l a t i o nc a no n l y e n s u r et h er e s u l tc o r r e c t ，b u tf a c et h ec o m p l e xs y s t e m ，s i m u l a t i o nw i t h o u te n di s u n p r a c t i c a l i no r d e rt oa v o i dt h ed e s i g ne r r o r , u s ep s lt ov a l i d a t et h ec o m p a r ec o r e ， m a k ef o r m a lv e r i f i c a t i o no ft h ev a l i d i t ya n di n t e g r a l i t yo ft h ec o m p a r ec o r ed e s i g n w h e nt h ea s s e r tf a i l ，t h ee r r o rc a i lb ed e t e c t e d a n a l y s i st h ee r r o ra n dm o d i f yt h ed e s i g n ， v t h e ns i m u l a t ei ta g a i n a f t e rs i m u l a t i o n ，m a k ef o r m a lv e r i f i c a t i o na g a i n ，u n t i lt h e r ei sn o e r r o ri nt h ed e s i g n p a p e rr e s e a r c han e wp l a t f o r ma r c h i t e c t u r e ，a n du s et h ep r o g r a m m a b l el o g i ct o a c h i e v e t h e n ，t h ed e s i g nv e r i f i e dt h r o u g ha s s e r t a tl a s t , w eg e tan o n - b u g , h i g h e f f i c i e n c ya n dc u r r e n c ys a f eh a r d w a r ep l a t f o r m k e y w o r d s ：s a f ec o m p u t e r ；2x2 - o u t o t - 2 ；f p g a ；f o r m a lv e r i f i c a t i o n ；p s l c l a s s n o ：t p 3 0 9 1 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 学位论文作者签名：签字日期： 0 2 7 年月，6 日 6 1 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国 家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文作者签名：跟前 签字日期：o ? 夕年6 月，d 日 导师签名： 签字日期：口 致谢 本论文的工作是在我的导师马连川副教授的悉心指导下完成的，马连川副教 授严谨的治学态度和科学的工作方法给了我极大的帮助和影响。在此衷心感谢三 年来马连川老师对我的关心和指导。 唐涛教授对于我的科研工作和论文都提出了许多的宝贵意见，在此表示衷心 的感谢。 感谢王悉老师、袁彬彬师兄、陈树权师兄对我科研工作的指导和帮助。 在实验室工作及撰写论文期间，实验室里王艺燕、刘辉、雷小玲、陈通对我 论文中的研究工作给予了热情帮助，在此向他们表达我的感激之情。 另外也感谢我的父亲、母亲，他们的理解和支持使我能够在学校专心完成我 的学业。 本论文由国家自然科学基金项目“列车运行控制及组织的基础理论与关键技 术研究 ( 项目号：6 0 6 3 4 0 1 0 ) 支持。 1 绪论 1 1选题的目的和意义 社会经济迅猛发展，人们的生活节奏日益加快，高效、安全、便捷的交通方 式是人们所追求的。同时，人类社会发展正面临着人口膨胀、资源超前消费、环 境急剧恶化的空前挑战，所以发展公共交通是解决城市交通拥堵问题的最佳途径。 城市轨道交通以安全、准时、运输能力大、节能、高效、环保，并且有效减缓地 面交通压力等优点，成为缓解人口密集的大城市交通问题的有利手段。 目前正处于国内轨道交通高速发展的时期，列车提速和行车间隔缩短，都给 列车控制系统带来了很大的压力和挑战，只有保证控制系统的安全，才能保证列 车行驶的安全。列车控制系统的主要作用是对列车运行进行控制，确保运行安全， 提高运输效率。为了适应城市轨道交通高密度的运营要求，列车控制系统正朝着 自动化、智能化、系统化、网络化和信息化的方向发展。基于通信的列车控制 ( c o m m u n i c a t i o n s b a s e dt r a i nc o n t r o l ，c b t c ) 系统式目前全球轨道交通界公认 的最先进的列车控制技术，它代表着当今世界范围内轨道交通信号技术的发展趋 势。c b t c 系统一般包括列车自动监控系统( a u t o m a t i c t r a i ns u p e r v i s i o n ，a t s ) ， 数据存储单元( d a t a b a s es t o r a g eu n i t ，d s u ) ，区域控制器z c ( z o n ec o n t r o l l e r ， z c ) ，计算机联锁( c o m p u t e ri n t e r l o c k i n g ，c i ) ，轨旁设备( w a y s i d ee q u i p m e n t ， w e ) ，车载控制器( v e h i c l eo nb o a r dc o n t r o l l e r ，v o b c ) ，数据通信系统( d a t a c o m m u n i c a t i o ns y s t e m ，d c s ) 等。其中z c 和d s u 子系统的应用软件都需要搭建 在安全硬件平台上乜1 。 安全硬件平台通过先进的计算机、电子技术来现实。随着计算机、电子技术 的迅猛发展，系统性能大大提高，结构也变得越来越复杂。由于计算机的广泛应 用，其可靠性成为一个突出问题。安全苛求系统中要求计算机能长期、稳定、安 全、可靠地运行，否则就会造成人身、财产等重大损失。由于计算机本身并不具 备故障安全特性，要保证系统的安全可靠，必须从系统的结构入手，加大研究力 度。使系统不仅拥有高效、准确的运行能力，还拥有很高的安全性和可靠性。 安全硬件平台的关键是其安全性。平台通过系统设计、结构设计、功能设计、 具体实现、仿真运行、测试、现场测试等过程，获得的结果正确，代表系统可用， 但并不能说明系统完善、安全。 随着系统的功能日益复杂，使得功能验证工作更加困难。在庞大的系统中， 人为检查设计漏洞难以实现，尽管采用了各种计算机辅助设计，仍然不能排除设 计漏洞。模拟技术是目前广泛使用的设计验证方法之一，但对于一个复杂的系统 进行穷尽的模拟是不切实际的。于是人们开始寻找新的途径来保证设计的正确性。 形式化验证就是一种具备这种能力的途径。 论文以铁路信号设备安全硬件平台为研究对象，使用通用处理器接口和可编 程逻辑设计一个安全硬件平台，并采用形式化方法对其进行功能检验，保证系统 设计正确、安全、可靠。 1 2安全硬件平台的研究情况 安全硬件平台对于整个列车控制系统非常重要，其输出的所有数据信息的安 全性都至关重要。既要满足故障安全特性又要保证可靠性，因此引进了冗余容错 技术，保证系统在有故障的状况下可以正常工作、正常输出。 1 2 1故障安全概念 故障安全技术诞生于信号系统发展初期，它是一种安全技术，强调的是当器 件、部件和系统发生故障时不产生危险侧输出的技术。在铁路行业标准 t b t 2 6 1 5 9 4 铁路信号故障安全原则中将故障安全定义为“故障后导向安全 。 随着电子业的发展，故障安全系统也发展为结构复杂的计算机系统。由于通用电 子元器件本身具备故障状态的不对称性，对于轨道交通运行控制领域，一旦计算 机系统不能正常工作，有可能造成严重的人员伤亡和财产损失小。 1 2 2安全计算机发展情况 安全计算机广泛应用于航空航天、轨道交通、核电站、银行金融、通信等安 全苛求领域中，避免系统遭遇由计算机失效所引起的事故。轨道交通信号系统的 核心是安全计算机，对它的研究具有重要的理论和实践意义。 1 9 6 5 年开始，信号设备开始使用计算机技术。日本国铁采用了故障安全变参 数为中心的逻辑器件，成功地开发了安全计算机联锁设备，试验结果表明，该设 备在日常控制和故障一安全性方面获得了良好成果。但出于经济考虑，并没有实际 应用。 1 9 7 8 年瑞典国铁在世界上最早是想了使用计算机的联锁设备。该系统采用了 1 台通用控制机，使用2 个不同版本的程序实现安全计算机，并将处理结果传给设 2 在现场设备、满足故障安全的比较器，二者输出一致，则控制相应的信号等现成 设备。 随后，日本国铁开发出了总线同步方式的安全计算机。这种方式是在2 台微 机中，安装有相同的程序，这样虽然加大了硬件投资，但简化了软件开发流程。 采用总线同步方式分为两类：三取二方式和二取二方式。 为了降低设备成本，因此出现了相位差安全计算机。它的特点是程序每执行 l m s 时，设有校验点，并且通过比较电路对校验点的数据进行校验，检测出计算机 故障。 后来，产生了任务同步方式的安全计算机。它的比较电路构成需要满足故障 安全，而计算机采用通用型。这使得安全硬件平台有了更大的发展空间哺1 。 1 3形式化验证 目前，超大规模集成电路的设计技术落后于制造工艺。由于设计系统日益复 杂化，难以保证设计的正确性。尽管采用了各种计算机辅助设计技术，仍然不能 越过这种“复杂性的栏栅。下面四个事件确切说明了形式化验证的重要性。 1 9 8 9 年，i n t e l8 0 4 8 6 微处理器预计投放市场，但由于浮点处理单元的一个设 计错误而推迟生产。 1 9 9 4 年，奔腾处理器被发现在执行某个特定的浮点运算时出现错误，这种错 误2 7 0 0 0 年才可能出现一次。对此，i n t e l 付出4 7 5 亿美元的巨额代价回收有缺陷 的奔腾处理器。 1 9 9 6 年6 月4 日，欧洲航天局研制的阿里亚娜五型火箭在发射后不到4 0 秒爆 炸。事后调查发现，原因在于当一个很大的6 4 位浮点数转换为1 6 位带符号整数 时出现异常。细微错误，使得十年的努力毁于一旦。 最近，a m d 四核处理器出现了旁路转换缓冲( t l b ) 和三级缓存中存在底层 错误。尽管a m d 随后推出了牺牲性能为代价的软件修正补丁，但最终a m d 还是 重新设计来消除上述错误。 形式化验证就是在一个有坚实理论基础的形式化系统中描述硬件设计的行为 规范和实现结构，并证明前者是后者的逻辑结果。完成了这种证明就保证了在任 何允许的输入条件下设计都是正确的。例如要验证一个组合电路设计的正确性， 可以用布尔代数公式作为它的模型。模拟方法要对某些典型的输入组合计算出相 应的输出真值是所期望的。而形式化证明可以在一个布尔代数的公理系统用布尔 代数式表示电路的行为规范，用公理和定义表示逻辑元件的行为规范和连接关系， 然后用布尔代数的定理从电路实现结构的描述推证出行为规范。一旦完成了这种 推导，也就证明了在各种输入条件下输出都是正确的。尽管这种证明不一定容易 完成，但实践表明这条路径是可行的。在一些场合己达到了实用的程度。因而有 人预言，硬件设计的形式化验证方法将同模拟技术一起成为未来的设计验证工具。 随着大规模集成电路( l a r g es c a l ei n t e g r a t e dc i r c u i t e s ，v l s i ) 的发展，将需要大批的 硬件验证专家。当然，形式化验证方法在当前还是昂贵的，验证一个复杂的设计 需要硬件验证专家的大量时间和精力尽管如此，在有些场合还是合算的。在安全 性极高的设计中如飞行控制、列车控制、心脏起搏器等，设计的失误会造成严重 的人身伤亡；还有些硬件是难以更换的，如某些传感器和监视器要安装在边远地 区，一旦失效，更换时代价太高；有些大批量生产的芯片，设计错误会造成巨大 损失。所有上述场合都值得对硬件的设计进行严格的形式化验证7 1 。 1 3 1形式化验证方法分类 形式化验证可以分为定理证明( t h e o r e mp r o v i n g ) 、等价性验证( e q u i v a l e n c e c h e c k i n g ) 和模型检验( m o d e lc h e c k i n g ) 。 1 等价检查( e q u i v a l e n c ec h e c k i n g ) 等价性检查的基本原理是建立被比较的两个模型之间的关系，依据数学定理 和公理，检查它们之间的等价性。使用该方法可以大大减少验证工作量，但是它 需要一个标准模型做参考，不能发现模型本身存在的错误。 2 模型检验( m o d e lc h e c k i n g ) 在模型检验算法中，用布尔公式表示所验证系统的状态，并以二叉判决图 ( o r d e r e db i n a r yd e c i s i o nd i a g r a m ，o b d d ) 形式进行存储，通过遍历o b d d 来检查 系统是否满足验证工程师用c t l 公式所描述的各种属性。 3 定理证明( t h e o r e mp r o v i n g ) 定理证明是一个纯粹的数学推导和证明过程，虽然该方法在学术界应用广泛， 但是由于它要求验证人员掌握扎实的数学功底，代价过高，因此在业界的使用并 不普遍嵋1 。 与传统的仿真验证方法相比，形式验证的优势在于它不需要任何测试用例就 可以进行全面的功能验证，可以实现验证对象中功能属性点的全部覆盖，而模型 检验算法则是形式验证中最具发展潜力的算法。 1 3 2 基于断言的模型检验 断言可以描述设计的输入、输出等功能行为。用一种语言来描述设计的功能 4 行为，然后将此断言嵌在设计中，或放在一个单独的外部文件中，在仿真或形式 验证的过程中。断言将被仿真工具或形式验证工具检查，设计者就能够知道设计 是否满足所描述的功能行为。这种验证方法就是基于断言的验证( a s s e r t i o n b a s e d v e r i f i c a t i o n ，a b v ) 【9 】o 断言的插入点可以被认为具有和软件内部测试点类似的概念，它在验证过程 中不停地监视着设计的预期行为，并且不断地为设计工程师和验证工程师提供各 种相关信息。例如当在某一个插入点存在设计缺陷时，相关的缺陷报告就会被打 印出来。通过这种验证方法，设计工程师和验证工程师可以节省大量的时间和精 力。使用传统的基于仿真的验证方法时，验证工程师必须手工编写测试向量，并 且要花费大量时间、精力来思考什么样的测试向量才会使设计内部的错误能传播 到输出端口上，仿真完成后，分析波形和日志文件也是一个费时费力的过程。这 种方法的验证效率低下，而且往往不能找出设计的内部缺陷。断言验证方法可以 作为传统验证的有效补充，改善了传统验证方法中的很多问题，具体优点描述如 下： 1 断言改善了传统验证方法的验证质量 仿真验证方法的仿真工作通常在芯片级进行，模块级的仿真有很多的限制。 因此，很多的设计缺陷是在项目设计的最后阶段才被发现，并且很难确定这些缺 陷的位置。在模块级的代码开发时，在硬件描述语言( h a r d w a r ed e s c r i p t i o n l a n g u a g e ，h d l ) 代码中插入断言，不仅可以减少设计人员手工编写模块级测试 向量的工作量，而且可以在项目进程的早期就开始验证工作，有助于较早的发现 设计错误。 2 断言验证提高了设计的可观察性和可控性 使用仿真验证查找设计错误时，必须通过分析波形和日志文件，来检查设计 中是否存在错误。而断言验证需要了解设计模块的实现结构，当断言监视到设计 中有违反断言描述的行为特性时，它就会报告出设计缺陷的相关信息，大大提高 了设计的可观察性。内嵌在h d l 里的断言，不但可以用来增加可观察性以方便侦 测错误，还可以用来表达设计者的设计意图与叙述设计里的要点。当整合多个模 块时，断言也可以用来隔绝与抓住问题的所在。 3 断言增加了模块间的协调性 断言一般插入在模块中，也可以插入在设计的输入输出接口，监视设计的接 口行为特征。现代的集成电路( i n t e g r a t e d c i r c u i t ，i c ) 设计一般是由多名设计者合 作完成，每名设计者设计不同的模块，在最后的系统集成时，用断言来监视各个 模块的接口行为是必须的，因此断言可以验证多个模块能否协调工作。 4 断言具有可重用性 5 专门为了对某个模块进行验证而编写的测试向量一般不能用来验证其它功能 模块，但是同一个断言可以使用在不同模块的验证工作中，这样就保证了先前工 作的可重用性们。 根据设计中断言所描述的功能行为的不同，可以将其分为3 种：应用断言 ( a p p l i c a t i o na s s e r t i o n ) 、接口断言( i n t e r f a c ea s s e r t i o n ) 和结构断言( s 伽l 醐】瑚l a s s e r t i o n ) 副。 应用断言主要描述整个设计总的功能行为，如发送一个字节后必须有一个应 答信号；接口断言主要描述模块间的通信协议、控制信号的传递等；结构断言主 要描述低层次模块内部的属性，如f i f o 中的溢出等，断言类型如图1 1 所示。 结构断言 应用断言 图1 - 1 断言类型 f i g 1 - 1k i n d so f a s s e r t i o n f s m 1 3 3断言方法的确定 目前，在i c 设计中获得广泛应用的断言验证语言有开放验证库( o p e n v e r i f i c a t i o nl i b r a r y , o v l ) 、特性规范语言( p r o p e r t ys p e c i f i c a t i o nl a n g u a g e ，即p s l ) 和s y s t e m v e r i l o g a s s e r t i o n 。 o v l 被定义成库的形式，这个库中包含一系列预定义模块。把这些模块例化 在硬件设计代码中，就可以得到预期的断言效果。这个库的实现机制具有结构和 语义的限制，因此，不能直接对库中的断言监视器进行扩展1 。使用断言的基本方 法是在设计中例化模块，其实际定义则在o v l 中的相应模块里，因此，增加新的 断言特性仅能通过增加新端口和参数来实现。 p s l 是在以前属于个人，后来被捐赠出来的s u g a r 语言的基础上开发出来的 断言验证语言，它也是一种用来定义和验证设计属性的语言，但是要把这个语言 完整的压缩在v e r i l o g 语言中并不太容易实现，不过可以直接在r t l 代码中使用 p s l 结构，这种方式通过p r a g m a 机制实现。在不支持p s l 的r t l 设计工具中， 6 这种机制可以让用户方便地使用p s l 语言n 别。通常，可用p s l 验证的设计属性范 围超过了o v l 库中的断言监视器，其验证能力也比o v l 强大。p s l 也和o v l 一 样提供了一些最常用的检查器，这些检查器可以简化p s l 的应用。 s y s t e m v e r i l o g 目前由a c c e l l e r a 组织所制订，但是技术来源则主要是由各家公 司所贡献。a c c e l l e r a 下的s y s t e m v e r i l o g 委员会的会员来自模拟器、合成器、验证 方法学等厂商，以及i e e e1 3 6 4v e r i l o g 标准小组、资深设计与验证工程师，版本 到目前3 1 版为止【1 3 1 。一般来说，s y s t e m v e r i l o g3 0 着重在于更高抽象度的模型建 立( m o d e l i n g ) ，允许硬件设计者与系统设计者使用同一描述语言；而s y s t e m v e d l o g 3 1 则是侧重在验证部分，结合s y n o p s y s 与i b m 在验证技术上的成果：它包括断 言和功能覆盖率的特性。这个特性可以让验证工程师和设计工程师使用同一种语 言完成各自的工作，而且可以让他们明白彼此编写的模块功能。它是一种纯粹的 硬件描述和验证( h d v l ) 语言，硬件描述和验证工作都可以用s y s t e mv e r i l o g 语 言完成。 k a u s i k d a t t a 和p p d a s 对这三种断言验证语言进行了的详细比较n 钔，见表1 1 。 表卜1 三种断言验证技术的比较 t a b l e l - 1c o m p a r eo f t h r e ea s s e r t i o nv e r i f i c a t i o n s 。 p a r a m c t e r so v lp s l s y s t e m v e r i l 0 9 3 1 特性声明yyy 特性检查yyy 约束规范nyy 顺序机制yyy 功能覆盖nyy 时钟同步yyy 即时断言nny 声明断言nyy 程序断言yny 编程语法nyy 内嵌函数nyn 使用难度不太容易 二 相当容易相当容易 工具开发难度容易不太容易容易 可见，p s l 是一种可执行、形式化、无二义性的性质描述语言，可以严格精 确地捕获设计者意图，在不同的抽象级别都可以轻松定义电路的复杂设计行为。 p s l 的开发被业界认为是一种变革性的飞跃，开始在i c 设计验证流程中占据举足 轻重的位置。 7 1 4论文的研究内容和组织结构 论文研究内容主要是以轨道交通运行控制系统为背景，故障安全技术为核心， 对比各种安全硬件平台结构，应用可编程逻辑和通用微处理器接口，设计一款安 全硬件平台，并对其进行形式化验证，保证其安全比较核的设计正确。论文根据 c b t c 系统对安全硬件平台的需求，确定平台的结构和功能，并用可编程逻辑实现 安全比较核的设计。平台设计、仿真后，利用形式化验证方法，对安全比较核进 行基于断言的模型检验，排除设计漏洞，确保比较核的安全性。 论文整体结构如下： ( 1 ) 第一章给出论文的选题目的和意义，介绍安全硬件平台的相关概念和安 全计算机的发展情况。介绍形式化验证方法的概念、重要性和分类最后 确定本论文所选用的验证方法。 ( 2 ) 第二章对常见的安全计算机结构进行分析，然后重点比较几种二取二安 全计算机结构。最后根据实际应用，结合专业需求，设计出一种新的平 台结构。本文设计的安全硬件平台分为安全比较核和安全处理器两部 分，安全比较核为设计重点。 ( 3 ) 第三章介绍安全硬件平台的功能设计。在每节中分类描述几个安全硬件 平台重要处理机制，包括安全性设计、通用性设计、调度策略设计等， 使平台最大可能实现安全、通用、透明、升级简化等优点。 ( 4 ) 第四章描述基于可编程逻辑的安全比较核的具体设计与实现。首先介绍 f p g a 和v h d l 的特点，再对安全比较核划分模块进行设计、实现，详 细介绍设计方案、功能、步骤。最后对各模块进行仿真，并对结果进行 分析，保证仿真结果正确。 ( 5 ) 第五章对安全比较核进行形式化验证。完成了设计与仿真，其功能性已 经保证。在这里对v h d l 语言进行形式化验证，保证设计正确。首先介 绍形式化验证方法的分类，然后利用p s l 语言对其进行基于断言的模型 检验。在论述对安全比较核进行断言验证的必要性的基础上，对每个重 点功能模块提出断言方案，并且进行断言验证。对验证结果进行分析、 修改、再验证。 1 5本章小结 本章说明了论文的选题目目的和意义，介绍了安全硬件平台的相关概念和目 前的发展情况，分析了当前安全硬件平台的开发意义和现状。然后介绍了形式化 验证方法的概念，并且分类介绍了几种常见形式化验证方法。根据各种方法的功 能、效果、可行性对比，选择断言作为本论文的验证方法。通过分析各种断言的 优缺点，最后选用p s l 。最后给出了论文的研究内容以及组织结构。 9 2 安全硬件平台系统结构设计 铁路信号设备的安全性极端重要。为了确保系统安全，合理的系统结构是关 键因素。只有在结构合理的基础上，研究技术实现的细节才有意义。 2 1安全计算机结构分析 2 1 1安全苛求系统对硬件平台的要求 安全苛求系统( s a f e t yc r i t i c a ls y s t e m ) 是指对组成系统的软件、硬件安全级 别要求很高的系统，系统出现故障后可能导致人员伤亡、重大经济损失或环境破 坏等严重后果。因此用于安全苛求系统中的硬件平台，安全性是最重要的。信号 系统中所采用的计算机也称为v i t a lc o m p u t e r ，v i t a l 比f a i ls a f e 含义更广，除了包 括故障安全技术外，也要采用其他安全技术来保证安全n 朝。 安全苛求系统中的安全计算机源于容错计算机，但由于应用环境的要求，安 全计算机的安全性和可靠性等方面性能要求都高于容错计算机。容错是指对于系 统内部出错的情况下，系统功能仍然能保持正常工作。目前所有的容错技术几乎 都是利用冗余技术来实现的，所谓冗余就是当计算机系统不需要容错时就没必要 添加的组成部分。冗余有多种不同类型，如硬件冗余、软件冗余、时间冗余、信 息冗余等，冗余是设计和实现可靠计算机系统最主要的技术和要求【1 6 1 。 2 1 2常见安全硬件平台结构 常见的安全硬件平台主要使用三取二和二乘二取二两种结构。 1 ) 三取二也称三模冗余( t r i p l em o d u l a rr e d u n d a n c y ，t m r ) ，如图2 一l 所示， 三个相同的计算机接收三个相同的输入，产生的三个结果送至多数表决器，属于 被动冗余。 1 0 输入1 输入2 输入3 输出 图2 1 三模冗余( t m r ) f i g 2 - 1t r i p l em o d u l a rr e d u n d a n c y ( t m r ) 表决器的输出取决于它三个输入的多数。若有一个计算机故障，则另两个正 常计算机的输出可将故障计算机的输出掩蔽，从而不会在表决器输出产生差错。 t m r 系统的主要问题是表决器的故障将造成系统差错。最简单形式的t m r 系统 的可靠度不会高于表决器的可靠度。为了克服这一困难，可采用多级三重表决， 如图2 2 所示。图中三个重复模块的输出送至三个表决器产生三个结果。只要仅有 一个模块故障或输入差错，这三个结果都将是正确的。而如果前面一级有一个表 决器故障，后面一级可看成一个输入有差错，后面一级的三个输出仍是正确的。 因此采用三重表决的t m r 系统又成为复原部件。 输入1 输入2 输入3 输出1 输出2 输出3 图2 - 2 多级三重表决 f i g 2 - 2m u l t i - l e v e lt r i p l em o d u l a rr e d u n d a n c y 2 ) 二乘二取二容错计算机系统的是由两套双机比较系统并联实现，二取二结 构保证系统的安全性，二乘结构保证系统的可靠性，系统如图2 3 所示。 输入 图2 - 3 二乘二取二系统 f i g 2 32x 2o u to f 2s y s t e m 输出 二取二是两个相同模块并行执行相同的计算，其结果由比较器进行比较。单 二取二通道只具备故障检测能力，但不提供容错能力，所以采用两套完全相同的 通道，当其中一个通道发生故障时，进行通道切换，由另一个通道继续工作。 二取二系统的可靠性是通过双通道完成的，发生故障时通道进行切换。这种 方式的主要技术难题是双机同步和数据比较，一旦发现不一致，则需要进行自检 以确定故障的所在并进行切换。 二乘二取二系统比三取二更具有可靠性，类似c b t c 的系统需要长时间不停 机运行，在系统设计过程中需要考虑在保证安全的基础上尽可能提高可用性。二 乘二取二系统的双通道是热备关系，当一个通道出现故障无法继续工作时，另一 通道可以立即代替工作，不影响系统的运行和对外输出，这一点是三取二结构无 法实现的。 2 1 3我国铁路的计算机联锁系统结构 在国内铁路微机联锁应用中，安全计算机都是采用二乘二取二结构的。例如 e 1 3 2 一j d 型计算机联锁系统、d s 6 k 5 b 型计算机联锁系统、t y 几1 1 型计算机联 锁系统。这三种系统的基本架构大致相同，体系结构如图2 。4 所示n 7 1 8 1 。 1 2 a 操作表示机i b 操作表示机 、 一一一一一 人蕾” 一一一 i _l 久驱采机 m i ， 彳i 广1 器”一l f ，一 靶 乡 采集电路驱动电路采集电路驱动电路 么 之弓 之弓 接口配线 彳产 霉 夕 机械室组合架几继电器 图2 4 联锁系统架构 f i g 2 4i l l t e d o c ks ) ，s t e ma r c h i t c c t l l 系统中的联锁机全称是联锁计算机，两套共4 个c p u 构成二乘二取二容错系 统。联锁机接收来自操作表示其传来的操作命令、接收驱动采集机传来的室外信 号设备状态、进行联锁运算，向驱动采集机传输室外信号设备动作命令，同时向 操作表式机传输表式信息。 二乘二取二结构是铁路信号领域中广泛应用的一种系统结构。二乘二取二是 两个二取二冗余实现，所以其关键是二取二，本文将对二取二结构进行研究、设 计与验证。 2 2几种二取二安全计算机结构比较 目前已经出现了许多成熟的安全计算机结构。各种结构之间各有特点、各有 利弊。本节对一些二取二安全结构进行分析、比较。 2 2 1双通道双处理器锁步结构 双通道双处理器锁步结构由两个完全相同的双处理器锁步通道组成，两个通 道通过网络连接n 引，如图2 5 所示。 图2 5 双通道双处理器锁步结构 f i g 2 - 5d u a ll o c k - s t e pd u a lp r o c e s s o ra r c h i t e c t u r e 在锁步结构中，两个处理器分为主处理器和检测处理器，在严格同步的条件 下执行相同的代码。主处理器访问系统中的所有存储设备和输入、输出设备。检 测处理器连续执行总线上的指令操作。检测处理器的所有输出，包括数据和地址， 都储存在监测区内，需要比较主处理器和检测处理器接口的数据线、地址线、控 制线上的所有信息。监测区不能检测出由共模故障引起的总线和存储区错误，所 以需要加入其它校验技术。 当检测出系统可忽略的错误时，锁步结构是故障沉默的。当总线和存储器有 数值改变时，通常会产生瞬时的校验位错误，这种瞬时错误是可以被系统忽视的。 系统鲁棒性的要求可以通过