龙芯2号微处理器的功能验证

开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务．龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍，如何保证设计的正确性是一个重大挑战．简单的系统级测试已经不能满足设计的需要，这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误．主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法．模拟仿真是主要的验证手段，新的形式化验证方法也应用到了验证流程当中．     

一种基于贝叶斯网络的随机测试方法在Cache一致性验证中的设计与实现

随着集成电路设计复杂度指数级增长,功能验证已经越来越成为大规模芯片设计的瓶颈,而在多核处理器中,Cache一致性协议十分复杂,验证难度大。针对Cache一致性协议验证提出基于模拟验证的一种基于贝叶斯网络的随机测试生成方法,解决Cache一致性协议状态空间爆炸的问题。首先分析了Cache一致性协议及基于贝叶斯网络推理的CDG方法,并将CDG方法应用于Cache一致性的验证。以FT处理器中的Cache一致性协议验证为例,对比伪随机测试,使用CDG方法将覆盖率提高近30%。     

Linux下基于ARM的工业控制终端与PLC通信技术的研究与应用

结合自动切纸机的嵌入式工业控制终端的开发,分析了Linux下以ARM9为处理器的工业控制终端与三菱F×系列PLC通信的过程.详细介绍了ARM与PLC之间的通信协议、通信命令、通信机制,可以实现ARM与PLC之间实时数据交换和控制功能.     

针对流水冲突的微处理器功能验证程序的自动生成

功能验证是处理器设计中的关键问题，而基于激励向量仿真的方法是功能验证的主流技术，其难点在于如何产生高效的测试程序。研究了针对流水冲突的测试程序的自动生成方法。与常规技术相比，该方法适用于深度流水、指令系统复杂的处理器，具有自动化程度高、针对性强等优点。本文方法已应用于32位RISC处理器的验证中，取得了良好的效果。     

The anatomy study of server-initial agreement for general hierarchy wired/wireless networks

The Byzantine Agreement (BA) plays a key role in fault-tolerant distributed system design. A number of solutions to the BA problem based on various network model assumptions have been proposed. However, most existing BA protocols are designed for pure wired or pure wireless networks. In practice, most current networks are combined wired and wireless environments. In this paper, we extend the BA problem over a combined wired/wireless network, consisting of both powerful computing stationary processor and low-power mobile processor. The communication overhead of BA protocol is inherently large and secure group communications are important. The protocols proposed in this paper use the hierarchical model concept to reduce the communication overhead and provide secure group communications well suited for combined wired/wireless networks.     

无线射频RFID识别协议自动验证方法研究

Population Protocols是一种受生物启发的计算模型,能够表示无线网络中数量庞大但计算能力弱的多组件间的交互,它为无线传感器网络提供了一种可计算推理的理论框架。将Population Protocol理论引入到RFID识别协议中,提出了RFID识别协议系统模型验证框架;构建了标签与阅读器交互产生的状态变迁模型;最后用spin模型检测工具和LTL线性时序逻辑验证了弱公平条件下该模型的自稳定性,为分析与验证无线传感器网络中协议的正确性提供了一种行之有效的方法。     

Formal models of communication services: a case study

Formal methods can play an important role in exploring new communication systems services. The telecommunications and data communications communities have long accepted the need for formally describing protocols, but only recently have they considered formally describing a service by abstracting specifications from a particular protocol that provides that service. Specifying a service at an abstract level meets two important needs: standardization and customization. The author presents a simplified atomic multicast as an example service and input/output automata for the formal model. He shows how to represent the service specification, a protocol, and implementations of that protocol. He also sketches how to prove the correctness of the protocol and implementation, that is, how to show that the specified service is actually provided     

模型检测MESIF Cache一致性协议

在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂。Cache一致性协议的验证一直是模型检测在工业界主要应用之一,被工业界和学术界关注。相对传统方法而言,微结构级的模型检测能够描述和验证更多的协议细节。利用NuSMV工具对Intel公司的MESIF Cache一致性协议进行模型检测在微结构层次上进行了建模,并对该协议进行模型检测,试验结果证明了此方法的有效性。     

Formal Verification of a Complex Pipelined Processor

This paper addresses the problem of formally verifying the correctness of a complex pipelined microprocessor at the micro-architectural level of abstraction. The design verified is an example out-of-order execution processor with a reorder buffer, a store buffer, branch prediction, speculative execution and exceptions. We propose a systematic approach called the Completion Functions Approach to decompose and incrementally build its proof of correctness. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect on the programmer visible state components of completing the instruction. This construction of the abstraction function leads to a very natural decomposition of the proof into proving a series of verification conditions. The approach prescribes a systematic way to generate these verification conditions which can then be discharged with a high degree of automation using techniques based on decision procedures and rewriting. The verification was completed in 34 person days, which we believe, is a modest investment in return for the significant benefits of formal verification.     

税控器通信软件的设计与实现

税控器(fiscal processor)是国家解决税收电子化的产品之一,它能很好地实现税控功能.详细论述了税控器与宿主机之间的通信软件的设计,该方案优于国标,经实验表明功能完善,性能稳定可靠.     

Using hybrid MPI and OpenMP programming to?optimize communications in parallel loop self-scheduling schemes for multicore PC clusters

Recently, a series of parallel loop self-scheduling schemes have been proposed, especially for heterogeneous cluster systems. However, they employed the MPI programming model to construct the applications without considering whether the computing node is multicore architecture or not. As a result, every processor core has to communicate directly with the master node for requesting new tasks no matter the fact that the processor cores on the same node can communicate with each other through the underlying shared memory. To address the problem of higher communication overhead, in this paper we propose to adopt hybrid MPI and OpenMP programming model to design two-level parallel loop self-scheduling schemes. In the first level, each computing node runs an MPI process for inter-node communications. In the second level, each processor core runs an OpenMP thread to execute the iterations assigned for its resident node. Experimental results show that our method outperforms the previous works.     

多核处理器Cache一致性协议关键技术研究

多核处理器规模的不断扩大和核间通信机制的日益复杂,使得Cache一致性维护变得更加困难。本文从多核处理器Cache一致性问题的产生背景出发,分析监听协议、目录协议、Token协议和Hammer协议的实现机制以及在多核环境中的优缺点,分别从一致性协议与片上互连结构协同设计、面向低功耗应用的协议优化策略、Cache一致性协议验证及容错机制等角度考虑,对未来多核处理器Cache一致性协议设计的发展趋势和技术挑战进行详细分析与讨论。     

高效能ESCA协处理器验证技术研究

处理器结构的日益复杂使得对处理器功能进行有效验证变得越来越重要和关键。基于一款高效能计算协处理器ESCA,讨论了边界值验证、等价类验证和决策表验证等三类验证方法在ESCA处理器功能验证中的具体实现,并针对ESCA处理器中不同功能模块的基本特性提出了一种综合验证方法。实验结果表明,采用综合验证方法进行的ESCA处理器功能验证,不仅高效保证了验证案例集的生成,而且以较少的验证工作量实现了100%功能覆盖率,有效减少了ESCA处理器功能验证时间,提高了验证效率。     

一个基于身份的非交互可否认源认证协议

可否认源认证方案能够让接收方确认消息发送方的身份,但不能向第三方证明发送方的身份,在电子商务和电子政务中有广泛的应用。在假定计算Diffie-Hellman问题是困难的前提下,利用双线性对,构造了一个基于身份的非交互可否认源认证协议,并在随机预言模型下证明了方案的安全性。分析结果表明新提出的协议可以抵抗伪造攻击、假冒攻击、中间人攻击以及重放攻击等。该协议基于身份,不需要证书,可简化密钥管理;其通信和计算效率较高,实现简单,可用于计算能力受限的设备。     

“龙腾R2”微处理器模块级验证

针对"龙腾R2"微处理器验证过程中的存在验证规模大,人力资源不足的问题,采用流水线模型构建随机的指令序列生成器,搭建以功能覆盖率为导向的自动化验证平台;该平台在仿真验证过程中能根据处理器的运行状态及覆盖率实时地调整指令流以侧重当前验证不充分的功能模块,实现自动化验证;通过仿真,与传统方法相比,在达到同等验证程度的情况下,使用该平台验证周期明显缩短,同时验证覆盖率也有所提高。     

Distributed Job Scheduling in Rings

We give a distributed approximation algorithm for job scheduling in a ring architecture. In contrast to many other parallel scheduling models, the model we consider captures the influence of the underlying communications network by specifying that task migration from one processor to another takes time proportional to the distance between those two processors in the network. As a result, our algorithm must balance computational load and communication time. The algorithm is simple, requires no global control, and yields schedules of length at most 4.22 times optimal. We also give a lower bound on the performance of any distributed algorithm and the results of simulation experiments which suggest better performance than does our worst-case analysis.     

Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm

The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.     

On the design of communication-aware fault-tolerant scheduling algorithms for precedence constrained tasks in grid computing systems with dedicated communication devices

Fault-tolerant scheduling is an imperative step for large-scale computational Grid systems, as often geographically distributed nodes co-operate to execute a task. By and large, primary-backup approach is a common methodology used for fault tolerance wherein each task has a primary and a backup on two different processors. In this paper, we address the problem of how to schedule DAGs in Grids with communication delays so that service failures can be avoided in the presence of processors faults. The challenge is, that as tasks in a DAG have dependence on each other, a task must be scheduled to make sure that it will succeed when any of its predecessors fails due to a processor failure. We first propose a communication model and determine when communications between a backup and backups of its successors are necessary. Then we determine when a backup can start and its eligible processors so as to guarantee that every DAG can complete upon any processor failure. We develop two algorithms to schedule backups, which minimize response time and replication cost, respectively. We also develop a suboptimal algorithm which targets minimizing replication cost while not affecting response time. We conduct extensive simulation experiments to quantify the performance of the proposed algorithms.     

新型触摸屏与DSP通信的研究与实现

介绍了一种新型触摸屏PWS1711的功能特点以及软件设计方法等。数字信号处理器DSP已经被非常广泛地应用于各个领域，DSP与PWS1711实现基于串口的通信，包括制定通信协议，硬件设置，以及通信软件的编写。谊通信方案经实验验证，切实可行、效率高、性能稳定。