探析基于可编程逻辑的硬件平台的设计与形式化验证

《探析基于可编程逻辑的硬件平台的设计与形式化验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、北京交通大学硕士学位论文基于可编程逻辑的硬件平台的设计与形式化验证姓名：张倩申请学位级别：硕士专业：交通信息工程及控制指导教师：马连川20090601中文摘要摘要：安全硬件平台通过先进的计算机、电子技术来现实。随着计算机、电子技术的迅猛发展，系统性能大大提高，结构也变得越来越复杂。安全硬件平台作为安全苛求系统的重要部分，其安全性是至关重要的。在设计阶段就应充分考虑安全性，以免由于潜在的设计缺陷导致整个系统存在安全隐患。由于系统逐渐向规模大、性能强、复杂性高的方向发展，单纯利用仿真、测试等方法无法对系统进行无穷验证，因此在硬件平台设计阶段，利用形式化方法对硬件平台

2、设计的正确性和完备性进行验证。论文以基于通信的列车控制(Communication-basextTrainControl，CBTC)系统为应用背景，详细分析了安全硬件平台需求。通过对比各种平台结构的优缺点，选取了二乘二取二结构为本文设计的总体结构。在分析各种安全计算机结构的基础上，结合CBTC系统对安全硬件平台的功能需求，提出一种新的二取二系统结构方案。论文设计的安全硬件平台是以安全性、通用性为重点。论文详细介绍了保证安全性、通用性和调度策略的具体功能实现方法。以微同步和硬件数据比较方式来保证平台的安全性；以处理器的约束、数据帧结构的确定和接口格式的固定来保证了

3、平台的通用性。安全硬件平台中的重要单元是安全比较核。安全比较核基于可编程逻辑设计与实现。使用可编程逻辑不仅可以缩减电路的体积，提高电路的稳定性，而且先进的开发工具使整个系统的设计调试周期大大缩短。在实现过程中，将安全比较核划分为不同的功能子模块，对每个子模块进行设计与实现，并且对仿真结果进行分析，保证其设计基本正确。仿真验证只能保证比较核的仿真结果正确，但对于复杂系统，无穷尽的仿真是不现实的。为了避免存在潜在的设计错误，论文利用基于断言的方法(PropertySpecificationLanguage，PSL)对安全比较核进行形式化验证，对其内部设计的正确性和完

4、整性进行检验。当断言失败，发现设计错误时，对检验出的设计错误进行分析、修改。再进行新的验证，直到形式化验证证明其设计没有潜在的设计缺陷为止。论文结果表明，对于基于可编程逻辑设计的安全硬件平台，利用断言对设计进行形式化验证，可以检验出仿真无法检验出的错误，保证其设计的完整性和正确性，从而得到一个无设计缺陷、通用的安全硬件平台。本文用图57幅，用表4个，参考文献32个。关键词：安全计算机；二乘二取二；FPGA：形式化验证；PSL分类号：TP309．1ABSTRACTABSTRACT：Thesafehardwareplatformisaccomplishedthrou

5、ghadvancedcomputerandelectronictechnology．Withthedevelopmentofcomputerandelectronic，thecapabilityofsystemincreasingwhilethecomplexityincreasing．Hardwareplatform勰aimportantpartofsafe-criticalsystem，safetyisvitalimportance．Thesafetyofthehardwareplatformmustbefullyconcernedatthedesignph

6、ase,forfearthedisfigurementofdesignwillberesultinthehiddensafetytroubleexistinginthesystem．Duetothesystemsdevelopingtothelargescale，highperformance，higllcomplexitydirection,itCannotaccomplishwiththesimulationalone．Sointhedesignphaseofhardwareplatform，needtou$etheformalverificationtov

7、alidateit．Itisnecessarytovalidatethecorrectandthematurityofthehardwareplatform．CBTCsystemisthebackgroundofthispaper,analysistherequirementofhardwareplatform．Troughtocomparesomedifferentkindsofplatformarchitecture,selectthe2X2-out-of-2asthedesignarchitecture．Onthebaseofanalysisarchite

8、ctureofsafec