操作系统形式化设计与安全需求的一致性验证研究

采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统的设计进行形式化建模,使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义.对象语义模型作为系统设计和形式化验证的联系.以实现和验证过的可信微内核操作系统VTOS为实例,阐述形式化设计和安全需求分析,并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证,表明VTOS达到预期的安全性.     

基于FPGA的串行多节点数据采集传输系统的应用研究

多节点分布式传感器的数据采集与传输系统有着广泛的应用,其物理层实现主要分为串行及并行两种方式。针对特定的应用场景,选用串行传输的实现方式,设计以FPGA芯片、RS485芯片及AD芯片为核心的硬件平台,使用verilog语言设计FPGA的RTL（Register Transfer Level）逻辑代码,并在Modelsim中完成了功能仿真验证。最终实现了物理层为串行传输、传输层为总线模型的数据采集传输系统,该系统RTL代码设计简单,维护性强,可靠性高,占用芯片资源少,具有一定的工程应用价值。     

基于探测目标的自适应航路规划算法产品化实现方法

为将基于探测目标的自适应航路规划算法进行产品化,采用基于模型的设计方法以及自动代码生成技术,使算法模型快速、健壮地转化为软件产品。软件产品由核心算法和外设驱动组成,核心算法采用基于模型设计思想进行设计,仿真验证后自动生成目标语言代码,考虑到IO访问方式的复杂性,外设驱动模块采用代码自动生成与手动编码相结合的方式实现,核心代码与外设驱动模块组成的完整工程下载到硬件板卡,通过试验验证软件产品与初始设计模型的一致性,实现算法的产品化。经过实践,所提出的算法产品化实现方法能够提高设算法设计效率和各阶段中间产品继承性,降低各阶段调试复杂性,实现产品开发的敏捷性和健壮性,可作为复杂算法工程实现的参考。     

软件辅助FPGA实现安全监控系统的方法研究

核电站的安全级监控系统除了实现人机交互式的监控功能外,还需满足系统安全性的要求。目前,现场可编程门阵列(FPGA)芯片以其功能的独立性、响应的快速性以及更好的安全性,越来越广泛地应用在核电站系统中。探索一种方法——采用FPGA芯片"纯硬件"的技术代替CPU芯片,同时去除操作系统,以实现安全监控系统,从而提高系统整体的可靠性和安全性。但为了降低FPGA程序的复杂度,增加系统的灵活度,需要具有友好交互界面的组态软件来辅助FPGA实现监控系统功能。因为安全监控系统运行环境的限制,以及出于安全性的考虑,将组态软件作为离线的组态工具来设计。从安全监控系统的画面显示层组态、系统数据层组态和组态信息下装三个方面进行了详细描述,给出了组态软件辅助FPGA芯片实现安全监控系统的实现方法。该方法已完成设计开发,进一步测试与验证后,即可推广到实际应用。     

无源高频RFID芯片的FPGA原型验证平台设计

利用Xilinx的FPGA设计了一个FPGA原型验证平台,用于无源高频电子标签芯片的功能验证。主要描述了验证平台的硬件设计,解决了由分立元件实现模拟射频前端电路时存在的问题,提出了FPGA器件选型原则和天线设计的理论模型。同时,给出了验证平台的测试结果,通过实际的测试证明了验证平台设计的正确性和可靠性。该验证平台有力地支撑了RFID芯片的功能验证,大大提高了标签芯片的投片成功率。     

一种高速ZBT SRAM控制器设计

FPGA已经在雷达领域得到了广泛应用,然而其内部存储容量通常无法达到系统需求,因此必须为FPGA配置外部高速存储器.本设计采用两片高性能ZBT SRAM作为乒乓缓冲区交替工作,最高访问速率可达133MHz,使FPGA片外总存储容量达到32Mbit,满足设计要求.由于ZBT SRAM具有特殊的访问时序,必须使用FPGA的内部数字时钟管理模块DCM对时钟的相位进行精确控制,同时还要使用时序约束高级设计技术调整控制器的输入输出延时特性,使该控制器能够顺利地在FPGA内部信号处理系统和ZBT芯片之间完成高速数据交换.经过上述优化设计,采用VHDL代码编写可综合代码完成布线,目前该控制器已经成功地在某雷达导引头信号处理机中获得应用,验证了其有效性.     

基于TestCenter的仪表转接机制设计与实现

随着包处理芯片设计的需求不断扩大,芯片验证环节的复杂性和难度的提高。一个完整芯片的验证过程会涉及到虚拟功能模型,寄存器传输级RTL,FPGA原型验证不同类型。在进行虚拟功能模型和RTL的验证时会以虚拟仪表的方式进行数据包收发的驱动,FPGA原型验证则以真实仪表的方式进行数据包收发驱动。一旦测试场景发生改变,需要重新编写测试用例,降低测试效率。本文针对验证的重用性差,效率低下等缺点设计了一种虚拟测试仪表,利用TCL语言实现测试脚本和转接脚本,结合网络测试仪表TestCenter实现设计虚拟仪表和真实仪表的转换机制,使得测试用例的可重用性提高,易回归,缩短不同验证阶段的时间。     

基于FPGA中NIOS Ⅱ内核设计的TFT_LCD显示驱动

本文基于FPGA中NIOS Ⅱ内核设计驱动真彩液晶显示模块,可根据材料成本、研发时间等任意选择FPGA芯片,增强了产品的可靠性和设计灵活性。     

从1394 VHDL代码移植看FPGA设计

通过从基于FPGA设计的1394物理层芯片与链路层芯片合并为一个FPGA芯片且由双端口升为三端口的VHDL代码移植过程，介绍1394芯片基本原理和移植中所产生的问题解决办法，阐述FPGA芯片设计的代码规范化的重要性以及一些基本技巧。     

一款多核处理器FPGA验证平台的设计与实现

高性能处理器设计日趋复杂,为了缩短验证周期,降低研制风险通常需要在流片之前进行基于现场可编程门阵列(field programmable gate-array,FPGA)原型验证平台的软硬件协同验证.随着处理器多核化的发展,FPGA原型验证平台的实现变得越来越具有挑战性.介绍了一款高性能多核微处理器FPGA验证平台的设计与实现方法,详细阐述了该FPGA验证平台采用的母板/子板总体架构、分片策略、时分复用实现技术及I/O接口实现方法.该平台具有良好的可扩展性,能够方便灵活地实现目标芯片在各种规模和配置下的FPGA验证,用于在流片前对目标芯片进行功能正确性验证和性能评估.经过该FPGA平台验证的目标芯片,首次流片返回的芯片能成功运行操作系统和各种应用程序,实现了一次流片成功的目标.最后对该FPGA验证平台的应用前景进行了分析总结.     

Model driven code checking

Model checkers were originally developed to support the formal verification of high-level design models of distributed system designs. Over the years, they have become unmatched in precision and performance in this domain. Research in model checking has meanwhile moved towards methods that allow us to reason also about implementation level artifacts (e.g., software code) directly, instead of hand-crafted representations of those artifacts. This does not mean that there is no longer a place for the use of high-level models, but it does mean that such models are used in a different way today. In the approach that we describe here, high-level models are used to represent the environment for which the code is to be verified, but not the application itself. The code of the application is now executed as is by the model checker, while using powerful forms of abstraction on-the-fly to build the abstract state space that guides the verification process. This model-driven code checking method allows us to verify implementation level code efficiently for high-level safety and liveness properties. In this paper, we give an overview of the methodology that supports this new paradigm of code verification.     

SoC芯片FPGA原型的软硬件协同验证

在IC设计中,验证占据着举足轻重的地位.为了达到高效率、高可靠性的验证结果,保证芯片在流片的成功率,引入了FPGA原型验证技术.本文以一款低功耗报警器SoC为对象,首先简单介绍了低功耗报警器SoC芯片的系统架构,然后详细说明了报警器SoC芯片FPGA原型验证的具体实现.利用软硬件协同验证方法,验证了报警器SoC芯片模块的功能以及系统验证.     

包含协议和语义的构件一致性验证方法

在基于构件的系统设计中,需要对构件的一致性进行验证。构件的一致性包括语义一致性和协议一致性,已有的一致性验证方法仅支持构件的协议一致性验证。而在实际应用中除了要进行构件的协议一致性验证外,还需要进行其语义一致性验证。为此提出了一种包含协议和语义的构件一致性验证方法。所提方法将方法语义与基于场景的需求规约相结合,使用语义扩展接口自动机模型(SIA)来建模构件的语义和协议信息,使用带有语义约束的UML交互概观图来表示基于场景的需求规约。通过对SIA和带语义约束的UML交互概观图的行为的理论分析,进一步形成了一种一致性验证算法,并用实例来说明其过程。该算法不仅能够检验系统中构件的协议一致性,而且能够检验其语义一致性。该算法中的方法语义包括了该方法参数的类型和详细语义信息,更符合实际应用情形。     

基于FPGA的AVS视频解码芯片验证平台设计

针对AVS视频解码芯片仿真和验证的要求,提出了基于FPGA的验证平台框架。该验证平台主要用于对AVS解码芯片进行硬件模块的验证,从而为整个视频解码芯片的开发提供可靠的依据。该平台基于Nios II软核处理器,可使软件模块和硬件模块在一个平台下真正实现软硬件协同工作。基于该平台实现了多个硬件模块和AVS视频解码芯片的验证,其结果证明了该验证平台的正确性和可靠性。     

A generic framework: from modeling to code

Model-driven development (MDD) is a very popular technique in the area of software development, but this technique is criticized due to lack of a formal semantics. MDD is used for large-scale system development using semi-formal techniques like UML (Unified Modeling Language), which are not amenable to formal analysis and consistency checking. Formal methods with MDD may provide an assurance of correctness of the system. This paper advocates an approach to building generic framework for rigorous MDD that is based on combining semi-formal notations with formal modeling languages, correctness of the system using model checker and automatic code generation from the verified formal specification. The main objective of this work is to apply model-driven techniques and tools with formal verification and its code generation for designing critical systems. An assessment of the proposed framework is given through a case study, relative to the development of a cardiac pacemaker system.     

基于xMAS模型的SpaceWire信誉逻辑的形式化验证

空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议, 保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。     

FPGA的验证平台及有效的SoC验证方法

设计了一种基于FPGA的验证平台及有效的SoC验证方法,介绍了此FPGA验证软硬件平台及软硬件协同验证架构,讨论和分析了利用FPGA软硬件协同系统验证SoC系统的过程和方法.利用此软硬件协同验证技术方法,验证了SoC系统、DSP指令、硬件IP等.实验证明,此FPGA验证平台能够验证SoC设计,提高了设计效率.     

一种1750A指令集仿真软核设计与验证

MIL-STD-1750A指令集是星载弹载计算机常用指令集之一,为实现该类指令集CPU+FPGA的通用性验证,实现安全性、强度、单粒子翻转等异常测试,满足测试覆盖率要求,保证星载弹载计算机系统可靠性,提出了一种CPU+FPGA的仿真模型搭建方法,利用如中断和故障处理机制的实现、浮点运算单元设计方式、异常注入机制设计以及图形控制界面等关键技术,实现了一种精简1750A仿真软核。实验证明,利用该仿真软核设计的CPU+FPGA的仿真模型平台,可极大提高1750系列CPU相关接口的FPGA产品的验证效率和可靠性,也为后续星载弹载软件的测试提供了一套故障注入方便、故障定位清晰的测试平台。