基于ECC校验码的存储器可扩展自修复算法设计

随着微电子工艺的不断进步,SoC芯片设计中SRAM所占面积越来越大,SRAM的缺陷率成为影响芯片成品率的重要因素。提出了一种可扩展的存储器自修复算法(S-MBISR),在对冗余的SRAM进行修复时,可扩展利用存储器访问通路中校验码的纠错能力,在不改变SRAM结构的前提下能够进一步提高存储器的容错能力,进而提高芯片成品率。最后对该算法进行了RTL设计实现。后端设计评估表明,该算法能够工作在1GHz频率,面积开销仅增加1.5%。     

Efficient dynamic priority based soft error mitigation techniques for configuration memory of FPGA hardware

Radiation-induced single bit upsets (SBUs) and multi-bit upsets (MBUs) are more prominent in Field Programmable Gate Arrays (FPGAs) due to the presence of a large number of latches in the configuration memory (CM) of FPGAs. At the same time, SBUs and MBUs in the CM can permanently or temporarily affect the hardware circuit implemented on FPGA. Hence, error mitigation and recovery techniques are necessary to protect the FPGA hardware from permanent faults arising due to such SBUs and MBUs. Different existing techniques used to mitigate the effect of soft errors in FPGA have high overhead and their implementations are also quite complex. In this paper, we have proposed efficient single bit as well as multi-bit error correcting methods to correct errors in the CM of FPGAs using simple parity equations and Erasure code. These codes are easy to implement, and the needed decoding circuits are also simple. Use of Dynamic Partial Reconfiguration (DPR) along with a simple hardware scheduling algorithm based download manager helps to perform the error correction in the CM without suspending the operations of the other hardware blocks. We propose a first of its kind methodology for novel transient fault correction using efficient error correcting codes with hardware scheduling for FPGAs. To validate the design we have tested the proposed methodology with Kintex FPGA. We have also measured different parameters like fault recovery time, power consumption, resource overhead and error correction efficiency to estimate the performance of our proposed methods.     

面向安全关键内存管理系统分层验证方法

安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.     

Systematic formal verification for fault-tolerant time-triggeredalgorithms

Many critical real-time applications are implemented as time-triggered systems. We present a systematic way to derive such time-triggered implementations from algorithms specified as functional programs (in which form their correctness and fault-tolerance properties can be formally and mechanically verified with relative ease). The functional program is first transformed into an untimed synchronous system and, then, to its time-triggered implementation. The first step is specific to the algorithm concerned, but the second is generic and we prove its correctness. This proof has been formalized and mechanically checked with the PVS verification system. The approach provides a methodology that can ease the formal specification and assurance of critical fault-tolerant systems     

Automated Verification of Functional Correctness of Race-Free GPU Programs

We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop invariants, and passes them to off-the-shelf SMT solvers. It is often impossible, however, to solve naively generated VCs in reasonable time. A main difficulty stems from quantifiers over threads due to the parallel nature of GPU programs. To overcome this difficulty, we additionally apply several transformations to simplify VCs before calling SMT solvers. Our implementation successfully verifies correctness of several GPU programs, including matrix multiplication optimized by using shared memory. In contrast to many existing verification tools for GPU programs, our verifier succeeds in verifying fully parameterized programs: parameters such as the number of threads and the sizes of matrices are all symbolic. We empirically confirm that our simplification heuristics is highly effective for improving efficiency of the verification procedure.     

Proof rules for flush channels

Flush channels generalize conventional asynchronous communication constructs such as virtual circuits and datagrams. They permit the programmer to specify receipt-order restrictions on a message-by-message basis, providing an opportunity for more concurrency in a distributed program. A Hoare-style partial correctness verification methodology for distributed systems which use flush channel communication is developed, and it is shown that it it possible to reason about such systems in a relatively natural way     

Concerned with the unprivileged: user programs in kernel refinement

It is a great verification challenge to prove properties of complete computer systems on the source code level. The L4.verified project achieved a major step towards this goal by mechanising a proof of functional correctness of the seL4 kernel. They expressed correctness in terms of data refinement with a coarse-grained specification of the kernel’s execution environment. In this paper, we strengthen the original correctness theorem in two ways. First, we convert the previous abstraction relations into projection functions from concrete to abstract states. Second, we revisit the specification of the kernel’s execution environment: we introduce the notion of virtual memory based on the kernel data structures, we distinguish individual user programs that run on top of the kernel and we restrict the memory access of each of these programs to its virtual memory. Through our work, properties like the separation of user programs gain meaning. This paves the way for proving security properties like non-interference of user programs. Furthermore, our extension of L4.verified’s proof facilitates the verification of properties about complete software systems based on the seL4 kernel. Besides the seL4-specific results, we report on our work from an engineering perspective to exemplify general challenges that similar projects are likely to encounter. Moreover, we point out the advantages of using projection functions in L4.verified’s verification approach and for stepwise refinement in general.     

基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具.这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测.但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全.为了解决这些问题,文中提出...     

一个基于纠错码和DCT变换的盲水印算法

提出了一个基于纠错码和DCT变换的图像盲水印算法,该算法利用图像置乱技术和纠错码方法生成水印序列。对不用纠错码、用汉明码和用BCH码的三种水印方案进行了仿真,结果表明利用纠错码的水印方案具有更好的鲁棒性。     

Generating Scenarios by Multi-Object Checking

These days, many systems are developed applying various UML notations to represent the structure and behavior of (technical) systems. In addition, for safety critical systems like Railway Interlocking Systems (RIS) the fulfillment of safety requirements is demanded. UML-based Railway Interlocking (UML-based RI) is proposed as a methodology in designing and developing RIS. It consists of infrastructure objects and UML is used to model the system behavior. This design is validated and demonstrated by using simulation with Rhapsody. Automated verification techniques like model checking have become a standard for proving the correctness of state-based systems. Unfortunately, one major problem of model checking is the state space explosion if too many objects have to be taken into account. Multi-object checking circumvents the state space explosion by checking one object at a time. We present an approach to enhance multi-object checking by generating counterexamples in a sequence diagram fashion providing scenarios for model-based testing.     

A computer checked algebraic verification of a distributed summation algorithm

We present an algebraic verification of Segalls propagation of information with feedback algorithm and we report on the verification of the proof using the PVS system. This algorithm serves as a nice benchmark for verification exercises (see [2, 8, 17]). The verification is based on the methodology presented in [7] and demonstrates its suitability to deliver mechanically verifiable correctness proofs of highly nondeterministic distributed algorithms.The research of the second author was supported by Human Capital Mobility (HCM). The research of the third author was supported by the Netherlands Organization for Scientific Research (NWO) under contract SION 612-33-006.Received October 1988 by J. RushbyRevised July 2004Accepted September 2004 by C. B. Jones     

Reducing Data Cache Susceptibility to Soft Errors

Data caches are a fundamental component of most modern microprocessors. They provide for efficient read/write access to data memory. Errors occurring in the data cache can corrupt data values or state, and can easily propagate throughout the memory hierarchy. One of the main threats to data cache reliability is soft (transient, nonreproducible) errors. These errors can occur more often than hard (permanent) errors, and most often arise from single event upsets (SEUs) caused by strikes from energetic particles such as neutrons and alpha particles. Many protection techniques exist for data caches; the most common are ECC (error correcting codes) and parity. These protection techniques detect all single bit errors and, in the case of ECC, correct them. To make proper design decisions about which protection technique to use, accurate design-time modeling of cache reliability is crucial. In addition, as caches increase in storage capacity, another important goal is to reduce the failure rate of a cache, to limit disruption to normal system operation. In this paper, we present our modeling approach for assessing the impact of soft errors using architectural simulators. We also describe a new technique for reducing the vulnerability of data caches: refetching. By selectively refetching cache lines from the ECC-protected L2 cache, we can significantly reduce the vulnerability of the L1 data cache. We discuss and present results for two different algorithms that perform selective refetch. Experimental results show that we can obtain an 85 percent decrease in vulnerability when running the SPEC2K benchmark suite while only experiencing a slight decrease in performance. Our results demonstrate that selective refetch can cost-effectivety decrease the error rate of an L1 data cache     

Variables Bounding Based Retiming Algorithm

Retiming is a technique for optimizing sequential circuits.In this paper,we discuss this problem and propose an improved retiming algorithm based on varialbes bounding.Through the computation of the lower and upper bounds on variables,the algorithm can significantly reduce the number of constratints and speed up the execution of retiming.Furthermore,the elements of matrixes D and W are computed in a demand-driven way,which can reduce the capacity of memory,It is shown through the experimental results on ISCAS89 benchmarks that our algorithm is very effective for large-scale seuqential circuits.     

Application of an optimization methodology for multidisciplinary system design of microgyroscopes

Microgyroscopes integrated with micro-transducers, readout and control circuits in a common board normally form complex microsystems. Optimization of the design of such systems requires thorough understanding of the coupling effects of their working environments, their physical structural parameters, their construction of electronics, and their fabrication processes, etc. prior to any design verification by costly and time-consuming prototyping. A tuning fork gyroscope was taken as an example to demonstrate the principle for optimizing the necessary multidisciplinary design procedures in designing MEMS, typically including: the environmental quality factors, structural properties, readout circuits, and fabrication factors. It then used genetic algorithm (GA) to optimize the global sensitivity by a specifically designed searching methodology. The so obtained optimal results were further verified by a FEM modal analysis and by an experiment with an acceptable resolution.     

Designing a multiway synchronization protocol

A multiway synchronization protocol makes it possible for several processes to synchronize in an environment where communication is asynchronous. We present the design of such a protocol. The design methodology is based on formulating the behaviour of the entities as transition systems. This admits a correctness proof: we show that the protocol is correct relatively an ‘ideal’ non-distributed algorithm, in the sense that the protocol and the ideal algorithm cannot be separated by any amount of testing. The proof method is based on cs-equivalence.     

基于布尔可满足性的电路设计错误诊断算法

提出了一种组合电路设计错误诊断算法,该算法结合传统基于模拟的方法和可满足性问题求解技术,在不依赖于故障模型的条件下实现对电路逻辑错误的诊断定位．提出了基于布尔可满足性的增量式电路诊断方法,通过对可满足解依据电路结构信息筛选分级,提高了多错误诊断定位的分辨率和准确性;并提出多项启发式方法,避免了大量不必要的操作,使算法在时间和内存上保持有效性．实验结果表明,利用形式验证的技术来导向模拟的过程,抓住了高复杂度的多错误定位问题的特征,提高了电路错误诊断的效率．     

Computer Modeling and Simulation: Increasing Reliability by Disentangling Verification and Validation

Verification and validation (V&V) of computer codes and models used in simulations are two aspects of the scientific practice of high importance that recently have been discussed widely by philosophers of science. While verification is predominantly associated with the correctness of the way a model is represented by a computer code or algorithm, validation more often refers to the model’s relation to the real world and its intended use. Because complex simulations are generally opaque to a practitioner, the Duhem problem can arise with verification and validation due to their entanglement; such an entanglement makes it impossible to distinguish whether a coding error or the model’s general inadequacy to its target should be blamed in the case of a failure. I argue that a clear distinction between computer modeling and simulation has to be made to disentangle verification and validation. Drawing on that distinction, I suggest to associate modeling with verification and simulation, which shares common epistemic strategies with experimentation, with validation. To explain the reasons for their entanglement in practice, I propose a Weberian ideal–typical model of modeling and simulation as roles in practice. I examine an approach to mitigate the Duhem problem for verification and validation that is generally applicable in practice and is based on differences in epistemic strategies and scopes. Based on this analysis, I suggest two strategies to increase the reliability of simulation results, namely, avoiding alterations of verified models at the validation stage as well as performing simulations of the same target system using two or more different models. In response to Winsberg’s claim that verification and validation are entangled I argue that deploying the methodology proposed in this work it is possible to mitigate inseparability of V&V in many if not all domains where modeling and simulation are used.