多机系统调试诊断关键技术与方法研究

多机系统规模和复杂度的增加，给测试人员带来了新的挑战。分析了多机系统调试阶段和运行阶段便于测试和诊断的软硬件技术，提出了一种基于边界扫描技术的层次化调试网络结构，给出了通过笛卡儿乘积构造（t,k）-可诊断系统的方法以及通过预处理降低诊断难度、加快诊断速度的思想。     

并行计算机系统容错设计

容错设计是提高计算机系统可靠性的有效手段。本文提出了一种分布共享主存的并行计算机系统的容错结构，着重分析了结构采用的故障诊断机制，提出了系统中备份节点机配置的优化策略。     

微处理器敏捷设计方法综述

随着登纳德缩放定律和摩尔定律几近终结,通过领域特定体系结构提升微处理器性能变得越来越重要,迫切需要提升微处理器设计生产率来应对网络、智能、安全等领域特定需求.国内外的实践表明,微处理器敏捷设计方法是一种能有效提升微处理器设计生产率的方法.通过对比软硬件设计的差异,分析出敏捷设计的本质及其应用于微处理器设计所面临的挑战.综述了微处理器敏捷设计领域近年来代表性研究实践,归纳出微处理器敏捷设计关键使能技术,探讨了该领域未来潜在的研究方向.     

一种新的基于图象的虚拟场景重建与漫游框架

本文介绍了利用图象产生虚拟场景的方法，分析了基于图象的虚拟的实的结构，提出了一种新的基于图象的虚拟场景的重建与游框架，并对其中的深度恢复这一关键２技术进行了讨论。     

基于统一资源管理的超级计算机系统节能方案

从系统级节能角度出发,结合天河一号超级计算机系统硬件架构特点,通过将计算、通信、冷却、供电等各种系统资源有机结合在一起,制订统一的资源管理架构,应用最近最少使用(LRU)等多种管理策略对系统资源进行集中管理,有效降低系统能耗。     

谓词抽象技术研究

随着软、硬件系统规模和功能的不断扩充,状态空间爆炸问题严重影响了模型检验的进一步发展与应用,成为验证大规模系统的瓶颈.谓词抽象是解决状态空间爆炸的最有效方法之一,近年来得到迅速发展.介绍了谓词抽象的基本算法并比较了不同的求解支持工具;重点分析了反例指导的抽象求精和基于插值的抽象求精原理;分析了产生新谓词的各种方法的优、缺点;最后指出了谓词抽象技术进一步发展所面临的挑战和发展方向.     

基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.     

HT总线的并行CRC-32计算原理及其实现

本文介绍了HT总线CRC-32的计算原理，推导了8位HT链路的CRC-32并行计算算法，用XilinxXCA000-5芯片实现并验证了该并行算法的正确性。     

参数化系统二维抽象的理论基础

模型之间的等价关系和抽象模型的性质保持是保证验证正确的必要条件,参数化系统二维抽象从构成系统状态空间的二维方向分别进行抽象,证明了此抽象方法的正确性和合理性,即TDA模型与原始模型存在模拟关系,而且在TDA模型中成立的只对单个变量进行全称量化的单索引ACTL*公式,在任意规模的原始模型中也成立,为简化参数化系统验证提供了理论依据。     

无穷状态系统可覆盖性分析算法

针对良序结构迁移系统可覆盖性分析计算成本高的问题,提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法.首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型;然后采用最新的模型检验技术增量式地计算不同权值下模型的可达状态空间上逼近,得到可覆盖的反例路径或证明该系统不可覆盖.实验结果表明,该算法在同等计算时间限制下能够解决更多的测试样例;在1 GB内存限制下,可以解决97.2%的测试样例,超过同类算法的2倍.