基于时序等价性检查的电路软错误系统级可靠性分析方法研究
|
摘要
随着集成电路设计与制造工艺的飞速发展,空间辐射和噪声干扰等环境因素引发的软错误严重威胁设计可靠性。为了同时满足性能、功耗、面积以及可靠性等多种设计目标需求,通常只能对电路进行有选择性的软错误保护。软错误可靠性分析是决定有选择性保护效果的关键。电路系统级软错误可靠性分析在设计的早期展开,不仅可以获得更高的分析效率,而且能够更早地为容错设计提供指导,避免设计返工,是工业界和学术界共同关注的研究热点。
已有的适用于数字电路系统级可靠性分析的方法主要有两类,即基于故障模拟的方法和基于形式化技术的方法。基于故障模拟的方法应用最广泛,但是,这类方法很难实现输入空间和故障空间的完全覆盖,是不完备的。基于形式化技术的方法虽然可以保证分析结果的完备性,但是已有的方法主要基于模型检验和定理证明,都需要较多的经验和专家支持,而且定理证明还需要手工干预。
与其他的形式化验证技术相比,时序等价性检查具有原理简单、易于理解和使用的优点。因此,本文将时序等价性检查技术引入到系统级软错误可靠性分析领域,深入研究了基于时序等价性检查的电路软错误系统级可靠性分析理论和方法,取得了如下创新成果:
1.提出一种基于错误传播模型和时序等价性检查的软错误敏感点筛选方法。该方法首先从电路中提取软错误的传播行为模型,然后基于该模型对故障电路与原电路进行等价性检查,识别对软错误敏感的时序单元。实验结果表明,提出的方法不仅可以精确筛选出电路中所有的软错误敏感点,还可以检测容错逻辑的有效性。
2.首次证明了一般电路的软错误免疫力主要来源于对软错误部分免疫的结点;并证明了电路及其组件的可靠性不仅随电路的输入分布变化而变化,而且随时间动态变化。从而为研究能够充分利用电路自身免疫力有效指导软错误保护的可靠性分析新方法提供理论依据。
3.提出一种运行时时序单元软错误可靠性排序方法和一种近似的时序单元软错误可靠性排序方法。其中,运行时可靠性排序方法能够根据输入分布和初始状态分布精确地离线预测电路中时序单元的运行时软错误可靠性排序。而近似的可靠性排序方法能够在输入分布未知的情况下,为工程师提供关于容错设计方面的初步指导。实验结果表明,两种方法都能够为电路的有选择性保护提供有效指导;且在相同的容错代价下,基于运行时方法的指导可以获得更高的可靠性;而近似的方法可以分析规模更大的电路。
4.提出一种基于二维分解的高层时序等价性检查方法。二维是指空间维与时间维。首先利用切片技术对验证对象进行空间维分解,然后在对切片进行等价性检查的过程中动态插入逻辑割点,实现时间维分解。实验表明,该方法能够有效地缓解存储空间爆炸问题。
5.设计实现了一个基于时序等价性检查的电路系统级软错误可靠性分析框架SEC-HSERA(Sequential Equivalence Checking based Hybrid Soft Error Reliability Analyzer)。该框架集成了本文提出的软错误敏感点筛选方法、运行时可靠性分析方法、近似的可靠性分析方法以及面向时序等价性检查的二维分解指导模块。将SEC-HSERA原型系统应用于32位嵌入式微处理器Estar2中译码器电路的软错误可靠性分析,并基于分析结果,对译码器的时序单元进行有选择性的软错误保护,最终以22.5%的功耗损失和0.59%的面积损失获得90.4%的错误覆盖率。
As technology scales, soft errors induced by various environment problems, such as cosmic radiation and random noise, threaten the system reliability severely. To reach the design goals of reliability, performance, power consumption and area simultaneously, the design can only be protected selectively. For selective protection, reliability evaluation is critical. Circuit’s system-level soft error reliability analysis is carried out early in design process, which is more efficient and can provide earlier guidance for soft error tolerance design to avoid reworking. System-level soft error reliability analysis has been the common research focus of the industrial circle and the academy circle.
Most of the existing approaches for system-level reliability evaluation of circuits can be classified into two categories: simulation based approaches and formal techniques based approaches. Though simulation based approaches are used most widely, they are incomplete since they cannot cover the input space and fault space completely. Formal techniques based approaches are complete, but most of the conventional approaches based on formal techniques are based on property checking and theorem proving, which both require experience and support from experts. Moreover, theorem proving needs manual intervention.
With the advantages in simplicity, ease-of-understanding and ease-of-use out of other formal verification techniques, sequential equivalence checking (SEC) is introduced into the area of circuit’s system-level reliability evaluation in this thesis, which focuses on the theory and approaches of SEC-based system-level reliability evaluation. The major innovative achievements are listed as follows:
1. A fault propagation characteristics and SEC guided soft error reliability evaluation approach is proposed. For scalability, fault propagation sequential dependence graph (SDG) is advanced to extract the soft error propagation characteristics. In this approach, equivalence checking is localized in the circuit parts affected by soft error propagation. Experimental results indicate that the propose approach not only can locate all the soft error vulnerable spots, but also can check the effectiveness of the protection logics in circuits.
2. It is theoretically proved that the circuit’s intrinsic immunity to soft errors mainly stems from the circuit components with partial immunity, and that the soft error reliability of a circuit at runtime varies with the input distribution as well as time. These conclusions provide theoretical basis for the research on reliability evaluation approaches which can make full use of circuits’intrinsic immunity to guide selective soft error hardening.
3. A run-time soft error reliability sorting approach and an approximated soft error reliability sorting approach are proposed. According to the input distribution and the initial state distribution, the run-time approach can exactly predict the runtime reliability sorting of sequential units by offline analysis, while the approximate approach can help engineers make preliminary vulnerability estimation to make necessary tradeoff between reliability and other design targets even when a good workload estimation of the design is unavailable. Experimental results show that both of the two approaches can guide the deployment of soft error protection mechanisms efficiently, and the runtime approach can achieve higher reliability than the approximate one at the same cost while the approximate approach can analyze lager-scale circuits.
4. A two dimensional (2D) decomposition SEC approach is advanced. Here,“2D”means the space dimension and the time dimension. The approach builds verification model for the slice of a single output variable every time first. And during the equivalence checking of the corresponding slices, logic cutpoints are dynamically inserted to split the verification problem in the time dimension. Promising experimental results demonstrate that this approach can reduce the storage explosion of SEC.
5. A SEC based Hybrid Soft Error Reliability Analyzer (SEC-SERA) is designed and developed, which integrates all the proposed soft error reliability evaluation approaches including the soft error vulnerable spots selection approach, the runtime soft error reliability sorting approach, the approximate reliability sorting approach, as well as the 2D decomposition SEC approach. The prototype system of SEC-HSERA is applied to analyze the reliability of the decoder in a 32bit embedded microprocessor. Guided by the result from SEC-HSERA, 90.4% error coverage was achieved with extra 22.5% power consumption and 0.59% area.
已有的适用于数字电路系统级可靠性分析的方法主要有两类,即基于故障模拟的方法和基于形式化技术的方法。基于故障模拟的方法应用最广泛,但是,这类方法很难实现输入空间和故障空间的完全覆盖,是不完备的。基于形式化技术的方法虽然可以保证分析结果的完备性,但是已有的方法主要基于模型检验和定理证明,都需要较多的经验和专家支持,而且定理证明还需要手工干预。
与其他的形式化验证技术相比,时序等价性检查具有原理简单、易于理解和使用的优点。因此,本文将时序等价性检查技术引入到系统级软错误可靠性分析领域,深入研究了基于时序等价性检查的电路软错误系统级可靠性分析理论和方法,取得了如下创新成果:
1.提出一种基于错误传播模型和时序等价性检查的软错误敏感点筛选方法。该方法首先从电路中提取软错误的传播行为模型,然后基于该模型对故障电路与原电路进行等价性检查,识别对软错误敏感的时序单元。实验结果表明,提出的方法不仅可以精确筛选出电路中所有的软错误敏感点,还可以检测容错逻辑的有效性。
2.首次证明了一般电路的软错误免疫力主要来源于对软错误部分免疫的结点;并证明了电路及其组件的可靠性不仅随电路的输入分布变化而变化,而且随时间动态变化。从而为研究能够充分利用电路自身免疫力有效指导软错误保护的可靠性分析新方法提供理论依据。
3.提出一种运行时时序单元软错误可靠性排序方法和一种近似的时序单元软错误可靠性排序方法。其中,运行时可靠性排序方法能够根据输入分布和初始状态分布精确地离线预测电路中时序单元的运行时软错误可靠性排序。而近似的可靠性排序方法能够在输入分布未知的情况下,为工程师提供关于容错设计方面的初步指导。实验结果表明,两种方法都能够为电路的有选择性保护提供有效指导;且在相同的容错代价下,基于运行时方法的指导可以获得更高的可靠性;而近似的方法可以分析规模更大的电路。
4.提出一种基于二维分解的高层时序等价性检查方法。二维是指空间维与时间维。首先利用切片技术对验证对象进行空间维分解,然后在对切片进行等价性检查的过程中动态插入逻辑割点,实现时间维分解。实验表明,该方法能够有效地缓解存储空间爆炸问题。
5.设计实现了一个基于时序等价性检查的电路系统级软错误可靠性分析框架SEC-HSERA(Sequential Equivalence Checking based Hybrid Soft Error Reliability Analyzer)。该框架集成了本文提出的软错误敏感点筛选方法、运行时可靠性分析方法、近似的可靠性分析方法以及面向时序等价性检查的二维分解指导模块。将SEC-HSERA原型系统应用于32位嵌入式微处理器Estar2中译码器电路的软错误可靠性分析,并基于分析结果,对译码器的时序单元进行有选择性的软错误保护,最终以22.5%的功耗损失和0.59%的面积损失获得90.4%的错误覆盖率。
As technology scales, soft errors induced by various environment problems, such as cosmic radiation and random noise, threaten the system reliability severely. To reach the design goals of reliability, performance, power consumption and area simultaneously, the design can only be protected selectively. For selective protection, reliability evaluation is critical. Circuit’s system-level soft error reliability analysis is carried out early in design process, which is more efficient and can provide earlier guidance for soft error tolerance design to avoid reworking. System-level soft error reliability analysis has been the common research focus of the industrial circle and the academy circle.
Most of the existing approaches for system-level reliability evaluation of circuits can be classified into two categories: simulation based approaches and formal techniques based approaches. Though simulation based approaches are used most widely, they are incomplete since they cannot cover the input space and fault space completely. Formal techniques based approaches are complete, but most of the conventional approaches based on formal techniques are based on property checking and theorem proving, which both require experience and support from experts. Moreover, theorem proving needs manual intervention.
With the advantages in simplicity, ease-of-understanding and ease-of-use out of other formal verification techniques, sequential equivalence checking (SEC) is introduced into the area of circuit’s system-level reliability evaluation in this thesis, which focuses on the theory and approaches of SEC-based system-level reliability evaluation. The major innovative achievements are listed as follows:
1. A fault propagation characteristics and SEC guided soft error reliability evaluation approach is proposed. For scalability, fault propagation sequential dependence graph (SDG) is advanced to extract the soft error propagation characteristics. In this approach, equivalence checking is localized in the circuit parts affected by soft error propagation. Experimental results indicate that the propose approach not only can locate all the soft error vulnerable spots, but also can check the effectiveness of the protection logics in circuits.
2. It is theoretically proved that the circuit’s intrinsic immunity to soft errors mainly stems from the circuit components with partial immunity, and that the soft error reliability of a circuit at runtime varies with the input distribution as well as time. These conclusions provide theoretical basis for the research on reliability evaluation approaches which can make full use of circuits’intrinsic immunity to guide selective soft error hardening.
3. A run-time soft error reliability sorting approach and an approximated soft error reliability sorting approach are proposed. According to the input distribution and the initial state distribution, the run-time approach can exactly predict the runtime reliability sorting of sequential units by offline analysis, while the approximate approach can help engineers make preliminary vulnerability estimation to make necessary tradeoff between reliability and other design targets even when a good workload estimation of the design is unavailable. Experimental results show that both of the two approaches can guide the deployment of soft error protection mechanisms efficiently, and the runtime approach can achieve higher reliability than the approximate one at the same cost while the approximate approach can analyze lager-scale circuits.
4. A two dimensional (2D) decomposition SEC approach is advanced. Here,“2D”means the space dimension and the time dimension. The approach builds verification model for the slice of a single output variable every time first. And during the equivalence checking of the corresponding slices, logic cutpoints are dynamically inserted to split the verification problem in the time dimension. Promising experimental results demonstrate that this approach can reduce the storage explosion of SEC.
5. A SEC based Hybrid Soft Error Reliability Analyzer (SEC-SERA) is designed and developed, which integrates all the proposed soft error reliability evaluation approaches including the soft error vulnerable spots selection approach, the runtime soft error reliability sorting approach, the approximate reliability sorting approach, as well as the 2D decomposition SEC approach. The prototype system of SEC-HSERA is applied to analyze the reliability of the decoder in a 32bit embedded microprocessor. Guided by the result from SEC-HSERA, 90.4% error coverage was achieved with extra 22.5% power consumption and 0.59% area.
引文
[1] Baumann R C. Soft Errors in Advanced Computer Systems [J]. IEEE Design and Test of Computer, Washington: IEEE Computer Society, 2005, 22(3): 258~266.
[2] Borkar S. Designing Reliable Systems from Unreliable Components: The Challenges of Transistor Variability and Degradation [J]. IEEE Micro, Washington: IEEE Computer Society, 2005, 25(6): 10~16.
[3] Borkar S. Thousand Core Chips-A Technology Perspective [C]. Design Automation Conference, New York: ACM, 2007: 746~749.
[4] Galivanche R, Narayanan V, Raina R, Sanda P. Soft Error: Is the Concern for Soft Errors Overblown? [C] IEEE International Test Conference, Washington: IEEE Computer Society, 2005: 1271.
[5] Mitra S, Karnik T, Seifert N, Zhang M. Logic soft errors in sub-65nm technologies design and CAD challenges [C]. Design Automation Conference. New York: ACM, 2005:2~4.
[6] Saggese G P, Wang N J, Kalbarczyk, Patel S J, Iyer R K. An Experimental Study of Soft Errors in Mricroprocessors [J]. IEEE Micro, 2005, 25(6): 30~39.
[7] Benso A, Prinetto P. Fault Injection Techniques and Tools for Embedded Systems Reliability Evaluation [M]. Boston: Kluwer Academic Publishers, 2003.
[8] Ravishankar K I, David J R. A Measurement-based Model for Workload Dependence of CPU Errors [J]. IEEE Trans. On Computer, 1986, 35(6):511-519.
[9] Siewiorek D P, Swarz R S. Reliable computer systems: Design and evaluation [M]. 2nd Edition. Bedford Mass: Digital Press, 1992.
[10] Hazucha P, Svensson C, Impact of CMOS technology Scaling on the Atmospheric Neutron Soft Error Rate [J]. IEEE Trans. on Nuclear Science, 2000, 47(6): 2586 ~ 2594.
[11] Robert B. Soft Error in Advanced Computer Systems [J]. IEEE Design and Test of Computer. Washington: IEEE Computer Society, 2005: 258~266.
[12] Chen C L, Hsiao M Y. Error-Correcting Codes for Semiconductor Memory Applications: A State-of-the-Art Review [J]. IBM Journal of Research and Development, Riverton, NJ, USA : IBM Corporation, 1984, 28(2):124~134.
[13]唐明,张国平,张焕国.基于汉明纠错编码的AES硬件容错设计与实现[J].电子学报,北京:科技出版社,2005(11):2013~2016.
[14] KleinOsowski A, Cannon E H, Oldiges P, Wissel L. Circuit Design and Modeling for Soft Errors [J]. IBM Journal of Research and Development, 2008, 52(3): 255~263.
[15] Mukherjee S, Kontz M, Reinhardt S. Detailed Design and Evaluation ofRedundant Multithreading Alternatives [C]. International Symposium on Computer Architecture, 2002: 99~110.
[16] Leveugle R. Early Analysis of Fault-based Attack Effects in Secure Circuits [J]. IEEE Transactions on Computers, 2007, 56(10): 1431~1434.
[17] Kogal R, Pinkerton S D, Lie T J, Crawford K B. Single-word Multiple-bit Upsets in Static Random Access Devices [J]. IEEE Transactions on Nuclear Science, 1993, 40(6): 1941~1946.
[18] Shivakumar P, Kistler M, Keckler, S W, Burger D, Alvisi L. Modeling the Effect of Technology Trends on the Soft Error Rate of Combinational Logic [C]. International Conference on Dependable Systems and Networks. Washington: IEEE Computer Society, 2002: 389~398.
[19] Leveugle R. A New Approach for Early Dependability Evaluation based on Formal Property Checking and Controlled Mutation [C]. IEEE International On-Line Testing symposium, Washington: IEEE Computer Society, 2005: 260~265.
[20] Hadjiat K, Leveugle R. Early Dependability Evaluation: Injection of Multiple Bit-flips [C]. Latin-American Test Workshop, Washington: IEEE Computer Society, 2005: 109~114.
[21] Leveugle R, Hadjiat K. Multi-level Fault Injections in VHDL Descriptions: Alternative Approaches and Experiments [J]. Journal of Electronic Testing: Theory and Applications (JETTA), Kluwer, 2003, 19(5):559~575.
[22] Wang N, Quek J, Rafacz T M, Patel S J. Characterizing the Effects of Transient Faults on a High-Performance Processor Pipeline [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2004:61~72.
[23] Goswami K, Iyer R, Young L. DEPEND: A Simulation-based Environment for System-level Dependability Analysis [J]. IEEE Transactions on Computers, Washington: IEEE Computer Society, 1997, 46(1):60~74.
[24] Holcomb D, Li W, Seshia S A. Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits [C]. Design, Automation & Test in Europe Conference & Exhibition, Washington: IEEE Computer Society, 2009: 785~790.
[25] Clarke E M, Wing J. Formal methods: state of the art and future directions [J]. ACM Computing Surveys, New York: ACM Press, 1996, 28(4): 626~643.
[26] Leveugle R. Behavior modeling of faulty complex VLSIs: why and how? [C] Baltic Electronics Conference, Tallinn, Estonia, 1998: 191~194.
[27] Leveugle R. Towards modeling for dependability of complex integrated circuits [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1999: 194~198.
[28] Abke J, B?hl E, Henno C. Emulation based real time testing of automotiveapplications [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1998: 28~31.
[29] B?hl E., Harter W, Trunzer M. Real time effect testing of processor faults [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1999: 39~43.
[30] Civera P, Macchiarulo L, Rebaudengo, M., Reorda, S., Violante, M. Exploiting FPGA for accelerating fault injection experiments [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 2001: 9~13.
[31] Valderas M G, Garcia M P, Cardenal R F, Ongil C L, Entrena L. Advanced Simulation and Emulation Techniques for Fault Injection [C]. IEEE International Symposium on Industrial Electronics (ISIE), Washington: IEEE Computer Society, 2007: 3339~3344.
[32] Antoni L, Leveugle R, Fehér B, Using Run-time Reconfiguration for Fault Injection in Hardware Prototypes [C]. IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Washington: IEEE Computer Society, 2000: 405~413.
[33] Andres D de, Ruiz J C, Gil D, Gil P. Run-time Reconfiguration for Emulating Transient Faults in VLSI Systems [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2006: 291~300.
[34] Sterpone L, Violante M, A New Partial Reconfiguration-Based Fault-Injection System to Evaluate SEU Effects in SRAM-Based FPGAs [J]. IEEE Transactions on Nuclear Science, 2007, 54(4): 965~970.
[35] Leveugle R, Calvez A, Maistri P. Vanhauwaert, P. Statistical fault injection: how much is sufficient? [C] Design, Automation and Test in Europe, Washington: IEEE Computer Society, 2009: 502~506.
[36] Benso A, Rebaudengo M, Impagliazzo L, Marmo P. Fault-list collapsing for fault-injection experiments [C]. IEEE Reliability and Maintainability Symposium, Washington: IEEE Computer Society, 1998: 383 ~388.
[37] Berrojo L, González I., Corno F, Reorda M S, Squillero G, Entrena L, Ongil C L. An Industrial Environment for High-Level Fault-Tolerant Structures Insertion and Validation [C]. IEEE VLSI Test Symposium, Washington: IEEE Computer Society, 2002: 229~236.
[38] Pierre L, Clavel R, Leveugle R. Soft Error Effect and Register Criticality Evaluations: Past, Present and Future [C]. IEEE Workshop on Silicon Errors in Logic - System Effects, Washington: IEEE Computer Society, 2009.
[39]黄海林,唐志敏,许彤.龙芯1号处理器的故障注入方法与软错误敏感性分析[J].计算机研究与发展.2006,43(10):1820~1827.
[40]张英武,袁国顺.微处理器故障注入工具与故障敏感度分析[J].半导体技术,2008,33(7):589~599.
[41] Mukherjee S, Weaver C, Emer J, Reinhardt S K, Austin T. A Systematic Methodology to Compute the Architectural Vulnerability Factors for a High-Performance Microprocessor [C]. IEEE/ACM International Symposium on Microarchitecture, Washington: IEEE Computer Society, 2003: 29~40.
[42] Li X, Adve S V, Bose P, Rivers J A. SoftArch: An Architecture-Level Tool for Modeling and Analyzing Soft Errors [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2005: 496~505.
[43] Fu X, Poe J, Li T, Fortes J. Sim-SODA: A Unified Framework for Architectural Level Software Reliability Analysis [C]. Workshop on Modeling, Benchmarking and Simulation (Held in conjunction with International Symposium on Computer Achitecture), 2006.
[44] Li X, Adve S V, Bose P, Rivers J A. Architecture-Level Soft Error Analysis: Examining the Limits of Common Assumptions [R].Computer Science Technical Report UIUCDCS-R-2007-2833, University of Illinois at Urbana-Champaign, 2007: 266~275.
[45] Fu X, Poe J, Li T, Fortes J. Characterizing Microarchitecture Soft Error Vulnerability Phase Behavior. International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems [C]. Washington: IEEE Computer Society, 2006: 147~155.
[46] Soundararajan N, Parashar A, Sivasubramaniam A. Mechanisms for Bounding Vulnerabilities of Processor Structures [C]. International Symposium on Computer Architecture, New York: ACM, 2007: 506~515.
[47] Walcott K R, Humphreys G, Gurumurthi S. Dynamic Prediction of Architectural Vulnerability from Microarchitectural State [C]. International Symposium on Computer Architecture, New York: ACM, 2007: 516~527.
[48] Li X, Adve S V, Bose P, Rivers J A. Online Estimation of Architectural Vulnerability Factor for Soft Errors [C]. International Symposium on Computer Architecture, New York: ACM, 2008: 341~352.
[49]余洁.专用指令集处理器可靠性评估技术研究[D].北京:中国科学技术大学,2007.
[50] Krautz U, Pflanz M, Jacobi C, Tast H W, Weber K, Vierhaus H T. Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods [C]. Design, Automation and Test in Europe Conference (DATE), San Jose: EDA Consortium, 2006: 176~181.
[51] Clarke E M, Emerson E A. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic [C]. Logic of Programs: Workshop, New York:Springer-Verlag, 1981(131): 52~71.
[52] Clarke E M, Emerson E A, Sistla A P. Automatic Verification of Finite-state Concurrent Systems using Temporal Logic Specification [J]. ACM Trans. on Program Language Systems, 1986(8): 244~263.
[53] Pnueli A. A Temporal Logic of Concurrent Programs [J]. Theoretical Computer Science, 1981(13): 45~60.
[54] Seshia S, Li W, Mitra S, Verification-guided Soft Error Resilience [C]. Design, Automation and Test in Europe Conference, San Jose: EDA Consortium, 2007: 1442~1447.
[55] Darbari A, Al-Hashimi B, Harrod P, Bradley D. A New Approach for Transient Fault Injection using Symbolic Simulation [C]. International On-Line Testing Symposium, Washington: IEEE Computer Society, 2008: 93~98.
[56] Bryant R E, Seger C H. Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation [C]. Design Automation Conference, New York: ACM Press, 1991: 397~402.
[57] Pierre L, Clavel R, Leveugle R. ACL2 for the Verification of Fault-tolerance Properties: First Results [C]. International Workshop on the ACL2 Theorem Prover and its Applications. New York: ACM Press, 2009: 90~99.
[58] Huang S Y, Cheng K-T. Formal equivalence checking and design debugging [M]. Dordrecht: Kluwer Academic Publishers, 1998: 99.
[59] Mneimneh N. M, Sakallah K A. Principles of Sequential-Equivalence Verification [J]. IEEE Design Test, Washington: IEEE Computer Society, 2005: 248~257.
[60] Somenzi F. Binary Decision Diagrams [J]. Calculational System Design, NATO Science Series F, IOS Press, 1999(173): 303~366.
[61] Jain J, Narayan A, Fujita M, Sangiovanni-Vincenlli A. A Survey of Techniques for Formal Verification of Combinational Circuits [C]. IEEE International Conference on Computer Design: VLSI in Computers and Processors, Washington: IEEE Computer Society, 1997: 445~454.
[62] Burch J R, Singhal V. Tight integration of combinational verification methods [C]. IEEE/ACM International Conference on Computer-Aided Design, Washington: IEEE Computer Society, 1998: 570~576.
[63] Prasad M, Biere A, Gupta A. A Survey of Revent Advances in SAT-based Formal Verification [J]. Software Tools for Technology Transfer, 2005, 7(2): 156~173.
[64] Cook S A. The Complexity of Theorem Proving Procedure [C]. ACM SIGACT, New York: ACM Press, 1971: 151~158.
[65] Coudert O, Madre J C. A Unified Framework for the Formal Verification of Sequential Circuits [C]. International Conference Computer-Aided Design,Washington: IEEE Computer Society, 1990: 126~129.
[66] C. Pixley, A Theory and Implementation of Sequential Hardware Equivalence [J]. IEEE Transactions on Computer-Aided Design, Washington: IEEE Computer Society, 1992(11): 1469~1478.
[67] P. Ashar, A. Gupta, and S. Malik, Using Complete-1-Distinguishability for FSM Equivalence Checking [C]. International Conference Computer-Aided Design, Washington: IEEE Computer Society, 1996: 346~353.
[68] Jiang J H, Brayton R K, On the Verification of Sequential Equivalence [J]. IEEE Trans. Computer-Aided Design, Washington: IEEE Computer Society, 2003, 22(6): 686~697.
[69] Sheeran M, Singh S, Stalmarck G. Checking Safety Properties Using Induction and a SAT Solver [C]. International Conference on Formal Methods in Computer-Aided Design. LNCS 1954, New York: Springer-Verlag, 2000: 108~125.
[70] Van Eijk C A J. Sequential Equivalence Checking Based on Structural Similarities [J]. IEEE Transactions on Computer-Aided Design, Washington: IEEE Computer Society, 2000(19): 814~819.
[71] Kemeny J G, Snell J L. Finite Markov Chains [M]. London: D. Van Nostrand Company, 1960.
[72] Trivedi K S. Probability and Statistics with Reliability, Queuing, and Computer Science Applications [M]. New York: John Wiley & Sons, 2001.
[73]林元烈.应用随机过程[M].北京:清华大学出版社,2001:65~103.
[74] Feller W. An Introduction to Probability Theory and its Applications [M]. New York: John Wiley & Sons, 1968.
[75] M. Zhang, S. Mitra, T. M. Mak, N. Seifert, Q. Shi, K. Kim, N. Shanbhag, N. Wang, and S. Patel. Sequential Element Design with Built-in Soft Error Resilience [J]. IEEE Transactions on VLSI, Washington: IEEE Computer Society, 2006: 1368~1378.
[76] http://www.cs.nyu.edu/acsys/cvc3 [DB/OL].
[77] SpaceWire Verilog [EB/OL]. http://www.opencores.org/projects.cgi/web/ SpaceWire/overview, 2005.
[78] X. Li and D. Yeung. Application-level correctness and its impact on fault tolerance [C]. International Symposium on High Performance Computer Architecture, Washington: IEEE Computer Society, 2007: 181~192.
[79] Polian I, Becker B, Nakasato M, Ohtake S, Fujiwara H. Low-cost Hardening of Image Processing Applications against Soft Errors, International Symposium on Defect and Fault tolerance in VLSI Systems [C]. Washington: IEEE Computer Society, 2006: 274~279.
[80] Polian I, Reddy S M, Pomeranz I, et al. On Reducing Circuit Malfunctions Caused by Soft Errors. International Symposium on Defect and Fault tolerance in VLSI Systems [C]. Washington: IEEE Computer Society, 2008: 245~258.
[81] Polian I, Reddy S M, Pomeranz I, et al. No Free Lunch in Soft Error Protection? [C] IEEE/IFIP Workshop on Dependable and Secure Nanocomputing, 2008.
[82] Asadi G, Tahoori M B. Soft Error Modeling and Protection for Sequential Elements [C]. IEEE Symposium on Defect and Fault Tolerance in VLSI Systems, Washington: IEEE Computer Society, 2005: 463~471.
[83] Hachtel G D, Macii E, Pardo E, Somenzi F. Markovian Analysis of Large Finite State Machines [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Washington: IEEE Computer Society, 1996, 15(12): 1479~1493.
[84] D. Marculescu, R. Marculescu, and M. Pedram. Trace-Driven Steady-State Probability Estimation in FSMs with Application to Power Estimation[C]. IEEE Design, Automation and Test in Europe Conference, Washington: IEEE Computer Society, 1998: 774~779.
[85] Meyer C D. Stochastic Complementation, Uncoupling Markov Chains and the Theory of Nearly Reducible Systems [J]. SIAM Reviews, Philadelphia: Society for Industrial and Applied Mathematics, 1989, 31(2): 240~272.
[86] FMcMillan K L. Symbolic Model Checking [M]. Norwell: Kluwer Academic Publishers, 1994: 216.
[87] http://Javabdd.soureceforge.net [DB/OL].
[88] Pixley C. Formal Verification of Commercial Integrated Circuits, IEEE Design and Test of Computers [J]. Washington: IEEE Computer Society, 2001(18): 4~5.
[89] Mathur A, Balakrishnan M, Mitra R, Fujita M. Full-day Tutorial: Sequential Equivalence Checking [C]. International Conference on VLSI Design(VLSID), 2006: 2.
[90] Semeria L, Seawright A, Mehra R, Ng D, Ekanayake A, Pangrle B. RTL C-based Methodology for Designing and Verifying a Multi-threaded Processor [C]. Design Automation Conference, New York: ACM Press, 2002: 123-128.
[91] Feng X, Hu A J. Early Cutpoint Insertion for SLM Software vs. RTL Formal Combinational Equivalence Verification [C]. Design Automation Conference, New York: ACM Press, 2006: 1063~1068.
[92] Kroening D, Clarke E, Yorav K, Behavioral consistency of C and Verilog programs using bounded model checking [C]. Design Automation Conference, New York: ACM Press, 2003: 368~371.
[93] Biere A, Cimatti A, Clarke E M, Strichman O, Zhu Y. Bounded Model Checking [J]. Advances in Computers, College Park: Academic Press, 2003(58): 117~148.
[94] Kroening D, Clarke E. Checking Consistency of C and Verilog using PredicateAbstraction and Induction [C]. International Conference on Computer-Aided Design. Washington: IEEE Computer Society, 2004: 66~72.
[95] Matsumoto T, Saito H, Fujita M, Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs [C]. International Symposium on Quality Electronic Design, Washington: IEEE Computer Society, 2006: 370~375.
[96] Vasudevan S, Viswanath V, Abraham J A, Tu J. Automatic Decomposition for Sequential Equivalence Checking of System Level and RTL Descriptions [C]. International Conference on Formal Methods and Models for Co-Design, Washington: IEEE Computer Society, 2006: 71~80.
[97] Weiser M. Programmers Use Slices when Debugging [J]. Communication. New York: ACM, 1982, 25(7): 446~452.
[98] Weiser M. Program Slicing [J]. IEEE Transactions on Software Engineering, Washington: IEEE Computer Society, 1984, 10(4): 352~357.
[99]李必信等.程序切片技术及其应用[M].北京:科学出版社,2006.
[100] Berman C L, Trevillyan L H. Functional Comparison of Logic Designs for VLSI Circuits [C]. Computer-Aided Design, Washington: IEEE Computer Society, 1989: 456~459.
[101] Stump A, Barret C, Dill D. CVC: a Cooperating Validity Checker[C]. International Conference on Computer-Aided Verification, 2002: 500~504.
[102] Tu J, Viterbi Decoder Coprocessor in the DRM Application Soc [DB/OL]. http://www.cerc.utexas.edu/ shobha/masterreport.pdf.
[103] Texas 97 benchmarks. http://vlsi.colorado.edu/vis/texas-97/ [DB/OL].
[104] Hennessy J L, Patterson D A. Computer Architecture: A Quantitative Approach [M]. San Fransisco: Morgan Kaufmann Publishers, INC, 1990.
[105] http://www.antlr.org/ [DB/OL].
[106] ANTLR Reference Manual [DB/OL]. http://www.antlr.org/share/ 1084743321127/ANTLR_Reference_Manual.pdf, 2004.
[2] Borkar S. Designing Reliable Systems from Unreliable Components: The Challenges of Transistor Variability and Degradation [J]. IEEE Micro, Washington: IEEE Computer Society, 2005, 25(6): 10~16.
[3] Borkar S. Thousand Core Chips-A Technology Perspective [C]. Design Automation Conference, New York: ACM, 2007: 746~749.
[4] Galivanche R, Narayanan V, Raina R, Sanda P. Soft Error: Is the Concern for Soft Errors Overblown? [C] IEEE International Test Conference, Washington: IEEE Computer Society, 2005: 1271.
[5] Mitra S, Karnik T, Seifert N, Zhang M. Logic soft errors in sub-65nm technologies design and CAD challenges [C]. Design Automation Conference. New York: ACM, 2005:2~4.
[6] Saggese G P, Wang N J, Kalbarczyk, Patel S J, Iyer R K. An Experimental Study of Soft Errors in Mricroprocessors [J]. IEEE Micro, 2005, 25(6): 30~39.
[7] Benso A, Prinetto P. Fault Injection Techniques and Tools for Embedded Systems Reliability Evaluation [M]. Boston: Kluwer Academic Publishers, 2003.
[8] Ravishankar K I, David J R. A Measurement-based Model for Workload Dependence of CPU Errors [J]. IEEE Trans. On Computer, 1986, 35(6):511-519.
[9] Siewiorek D P, Swarz R S. Reliable computer systems: Design and evaluation [M]. 2nd Edition. Bedford Mass: Digital Press, 1992.
[10] Hazucha P, Svensson C, Impact of CMOS technology Scaling on the Atmospheric Neutron Soft Error Rate [J]. IEEE Trans. on Nuclear Science, 2000, 47(6): 2586 ~ 2594.
[11] Robert B. Soft Error in Advanced Computer Systems [J]. IEEE Design and Test of Computer. Washington: IEEE Computer Society, 2005: 258~266.
[12] Chen C L, Hsiao M Y. Error-Correcting Codes for Semiconductor Memory Applications: A State-of-the-Art Review [J]. IBM Journal of Research and Development, Riverton, NJ, USA : IBM Corporation, 1984, 28(2):124~134.
[13]唐明,张国平,张焕国.基于汉明纠错编码的AES硬件容错设计与实现[J].电子学报,北京:科技出版社,2005(11):2013~2016.
[14] KleinOsowski A, Cannon E H, Oldiges P, Wissel L. Circuit Design and Modeling for Soft Errors [J]. IBM Journal of Research and Development, 2008, 52(3): 255~263.
[15] Mukherjee S, Kontz M, Reinhardt S. Detailed Design and Evaluation ofRedundant Multithreading Alternatives [C]. International Symposium on Computer Architecture, 2002: 99~110.
[16] Leveugle R. Early Analysis of Fault-based Attack Effects in Secure Circuits [J]. IEEE Transactions on Computers, 2007, 56(10): 1431~1434.
[17] Kogal R, Pinkerton S D, Lie T J, Crawford K B. Single-word Multiple-bit Upsets in Static Random Access Devices [J]. IEEE Transactions on Nuclear Science, 1993, 40(6): 1941~1946.
[18] Shivakumar P, Kistler M, Keckler, S W, Burger D, Alvisi L. Modeling the Effect of Technology Trends on the Soft Error Rate of Combinational Logic [C]. International Conference on Dependable Systems and Networks. Washington: IEEE Computer Society, 2002: 389~398.
[19] Leveugle R. A New Approach for Early Dependability Evaluation based on Formal Property Checking and Controlled Mutation [C]. IEEE International On-Line Testing symposium, Washington: IEEE Computer Society, 2005: 260~265.
[20] Hadjiat K, Leveugle R. Early Dependability Evaluation: Injection of Multiple Bit-flips [C]. Latin-American Test Workshop, Washington: IEEE Computer Society, 2005: 109~114.
[21] Leveugle R, Hadjiat K. Multi-level Fault Injections in VHDL Descriptions: Alternative Approaches and Experiments [J]. Journal of Electronic Testing: Theory and Applications (JETTA), Kluwer, 2003, 19(5):559~575.
[22] Wang N, Quek J, Rafacz T M, Patel S J. Characterizing the Effects of Transient Faults on a High-Performance Processor Pipeline [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2004:61~72.
[23] Goswami K, Iyer R, Young L. DEPEND: A Simulation-based Environment for System-level Dependability Analysis [J]. IEEE Transactions on Computers, Washington: IEEE Computer Society, 1997, 46(1):60~74.
[24] Holcomb D, Li W, Seshia S A. Design as You See FIT: System-Level Soft Error Analysis of Sequential Circuits [C]. Design, Automation & Test in Europe Conference & Exhibition, Washington: IEEE Computer Society, 2009: 785~790.
[25] Clarke E M, Wing J. Formal methods: state of the art and future directions [J]. ACM Computing Surveys, New York: ACM Press, 1996, 28(4): 626~643.
[26] Leveugle R. Behavior modeling of faulty complex VLSIs: why and how? [C] Baltic Electronics Conference, Tallinn, Estonia, 1998: 191~194.
[27] Leveugle R. Towards modeling for dependability of complex integrated circuits [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1999: 194~198.
[28] Abke J, B?hl E, Henno C. Emulation based real time testing of automotiveapplications [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1998: 28~31.
[29] B?hl E., Harter W, Trunzer M. Real time effect testing of processor faults [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 1999: 39~43.
[30] Civera P, Macchiarulo L, Rebaudengo, M., Reorda, S., Violante, M. Exploiting FPGA for accelerating fault injection experiments [C]. IEEE International On-Line Testing workshop, Washington: IEEE Computer Society, 2001: 9~13.
[31] Valderas M G, Garcia M P, Cardenal R F, Ongil C L, Entrena L. Advanced Simulation and Emulation Techniques for Fault Injection [C]. IEEE International Symposium on Industrial Electronics (ISIE), Washington: IEEE Computer Society, 2007: 3339~3344.
[32] Antoni L, Leveugle R, Fehér B, Using Run-time Reconfiguration for Fault Injection in Hardware Prototypes [C]. IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Washington: IEEE Computer Society, 2000: 405~413.
[33] Andres D de, Ruiz J C, Gil D, Gil P. Run-time Reconfiguration for Emulating Transient Faults in VLSI Systems [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2006: 291~300.
[34] Sterpone L, Violante M, A New Partial Reconfiguration-Based Fault-Injection System to Evaluate SEU Effects in SRAM-Based FPGAs [J]. IEEE Transactions on Nuclear Science, 2007, 54(4): 965~970.
[35] Leveugle R, Calvez A, Maistri P. Vanhauwaert, P. Statistical fault injection: how much is sufficient? [C] Design, Automation and Test in Europe, Washington: IEEE Computer Society, 2009: 502~506.
[36] Benso A, Rebaudengo M, Impagliazzo L, Marmo P. Fault-list collapsing for fault-injection experiments [C]. IEEE Reliability and Maintainability Symposium, Washington: IEEE Computer Society, 1998: 383 ~388.
[37] Berrojo L, González I., Corno F, Reorda M S, Squillero G, Entrena L, Ongil C L. An Industrial Environment for High-Level Fault-Tolerant Structures Insertion and Validation [C]. IEEE VLSI Test Symposium, Washington: IEEE Computer Society, 2002: 229~236.
[38] Pierre L, Clavel R, Leveugle R. Soft Error Effect and Register Criticality Evaluations: Past, Present and Future [C]. IEEE Workshop on Silicon Errors in Logic - System Effects, Washington: IEEE Computer Society, 2009.
[39]黄海林,唐志敏,许彤.龙芯1号处理器的故障注入方法与软错误敏感性分析[J].计算机研究与发展.2006,43(10):1820~1827.
[40]张英武,袁国顺.微处理器故障注入工具与故障敏感度分析[J].半导体技术,2008,33(7):589~599.
[41] Mukherjee S, Weaver C, Emer J, Reinhardt S K, Austin T. A Systematic Methodology to Compute the Architectural Vulnerability Factors for a High-Performance Microprocessor [C]. IEEE/ACM International Symposium on Microarchitecture, Washington: IEEE Computer Society, 2003: 29~40.
[42] Li X, Adve S V, Bose P, Rivers J A. SoftArch: An Architecture-Level Tool for Modeling and Analyzing Soft Errors [C]. International Conference on Dependable Systems and Networks, Washington: IEEE Computer Society, 2005: 496~505.
[43] Fu X, Poe J, Li T, Fortes J. Sim-SODA: A Unified Framework for Architectural Level Software Reliability Analysis [C]. Workshop on Modeling, Benchmarking and Simulation (Held in conjunction with International Symposium on Computer Achitecture), 2006.
[44] Li X, Adve S V, Bose P, Rivers J A. Architecture-Level Soft Error Analysis: Examining the Limits of Common Assumptions [R].Computer Science Technical Report UIUCDCS-R-2007-2833, University of Illinois at Urbana-Champaign, 2007: 266~275.
[45] Fu X, Poe J, Li T, Fortes J. Characterizing Microarchitecture Soft Error Vulnerability Phase Behavior. International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems [C]. Washington: IEEE Computer Society, 2006: 147~155.
[46] Soundararajan N, Parashar A, Sivasubramaniam A. Mechanisms for Bounding Vulnerabilities of Processor Structures [C]. International Symposium on Computer Architecture, New York: ACM, 2007: 506~515.
[47] Walcott K R, Humphreys G, Gurumurthi S. Dynamic Prediction of Architectural Vulnerability from Microarchitectural State [C]. International Symposium on Computer Architecture, New York: ACM, 2007: 516~527.
[48] Li X, Adve S V, Bose P, Rivers J A. Online Estimation of Architectural Vulnerability Factor for Soft Errors [C]. International Symposium on Computer Architecture, New York: ACM, 2008: 341~352.
[49]余洁.专用指令集处理器可靠性评估技术研究[D].北京:中国科学技术大学,2007.
[50] Krautz U, Pflanz M, Jacobi C, Tast H W, Weber K, Vierhaus H T. Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods [C]. Design, Automation and Test in Europe Conference (DATE), San Jose: EDA Consortium, 2006: 176~181.
[51] Clarke E M, Emerson E A. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic [C]. Logic of Programs: Workshop, New York:Springer-Verlag, 1981(131): 52~71.
[52] Clarke E M, Emerson E A, Sistla A P. Automatic Verification of Finite-state Concurrent Systems using Temporal Logic Specification [J]. ACM Trans. on Program Language Systems, 1986(8): 244~263.
[53] Pnueli A. A Temporal Logic of Concurrent Programs [J]. Theoretical Computer Science, 1981(13): 45~60.
[54] Seshia S, Li W, Mitra S, Verification-guided Soft Error Resilience [C]. Design, Automation and Test in Europe Conference, San Jose: EDA Consortium, 2007: 1442~1447.
[55] Darbari A, Al-Hashimi B, Harrod P, Bradley D. A New Approach for Transient Fault Injection using Symbolic Simulation [C]. International On-Line Testing Symposium, Washington: IEEE Computer Society, 2008: 93~98.
[56] Bryant R E, Seger C H. Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation [C]. Design Automation Conference, New York: ACM Press, 1991: 397~402.
[57] Pierre L, Clavel R, Leveugle R. ACL2 for the Verification of Fault-tolerance Properties: First Results [C]. International Workshop on the ACL2 Theorem Prover and its Applications. New York: ACM Press, 2009: 90~99.
[58] Huang S Y, Cheng K-T. Formal equivalence checking and design debugging [M]. Dordrecht: Kluwer Academic Publishers, 1998: 99.
[59] Mneimneh N. M, Sakallah K A. Principles of Sequential-Equivalence Verification [J]. IEEE Design Test, Washington: IEEE Computer Society, 2005: 248~257.
[60] Somenzi F. Binary Decision Diagrams [J]. Calculational System Design, NATO Science Series F, IOS Press, 1999(173): 303~366.
[61] Jain J, Narayan A, Fujita M, Sangiovanni-Vincenlli A. A Survey of Techniques for Formal Verification of Combinational Circuits [C]. IEEE International Conference on Computer Design: VLSI in Computers and Processors, Washington: IEEE Computer Society, 1997: 445~454.
[62] Burch J R, Singhal V. Tight integration of combinational verification methods [C]. IEEE/ACM International Conference on Computer-Aided Design, Washington: IEEE Computer Society, 1998: 570~576.
[63] Prasad M, Biere A, Gupta A. A Survey of Revent Advances in SAT-based Formal Verification [J]. Software Tools for Technology Transfer, 2005, 7(2): 156~173.
[64] Cook S A. The Complexity of Theorem Proving Procedure [C]. ACM SIGACT, New York: ACM Press, 1971: 151~158.
[65] Coudert O, Madre J C. A Unified Framework for the Formal Verification of Sequential Circuits [C]. International Conference Computer-Aided Design,Washington: IEEE Computer Society, 1990: 126~129.
[66] C. Pixley, A Theory and Implementation of Sequential Hardware Equivalence [J]. IEEE Transactions on Computer-Aided Design, Washington: IEEE Computer Society, 1992(11): 1469~1478.
[67] P. Ashar, A. Gupta, and S. Malik, Using Complete-1-Distinguishability for FSM Equivalence Checking [C]. International Conference Computer-Aided Design, Washington: IEEE Computer Society, 1996: 346~353.
[68] Jiang J H, Brayton R K, On the Verification of Sequential Equivalence [J]. IEEE Trans. Computer-Aided Design, Washington: IEEE Computer Society, 2003, 22(6): 686~697.
[69] Sheeran M, Singh S, Stalmarck G. Checking Safety Properties Using Induction and a SAT Solver [C]. International Conference on Formal Methods in Computer-Aided Design. LNCS 1954, New York: Springer-Verlag, 2000: 108~125.
[70] Van Eijk C A J. Sequential Equivalence Checking Based on Structural Similarities [J]. IEEE Transactions on Computer-Aided Design, Washington: IEEE Computer Society, 2000(19): 814~819.
[71] Kemeny J G, Snell J L. Finite Markov Chains [M]. London: D. Van Nostrand Company, 1960.
[72] Trivedi K S. Probability and Statistics with Reliability, Queuing, and Computer Science Applications [M]. New York: John Wiley & Sons, 2001.
[73]林元烈.应用随机过程[M].北京:清华大学出版社,2001:65~103.
[74] Feller W. An Introduction to Probability Theory and its Applications [M]. New York: John Wiley & Sons, 1968.
[75] M. Zhang, S. Mitra, T. M. Mak, N. Seifert, Q. Shi, K. Kim, N. Shanbhag, N. Wang, and S. Patel. Sequential Element Design with Built-in Soft Error Resilience [J]. IEEE Transactions on VLSI, Washington: IEEE Computer Society, 2006: 1368~1378.
[76] http://www.cs.nyu.edu/acsys/cvc3 [DB/OL].
[77] SpaceWire Verilog [EB/OL]. http://www.opencores.org/projects.cgi/web/ SpaceWire/overview, 2005.
[78] X. Li and D. Yeung. Application-level correctness and its impact on fault tolerance [C]. International Symposium on High Performance Computer Architecture, Washington: IEEE Computer Society, 2007: 181~192.
[79] Polian I, Becker B, Nakasato M, Ohtake S, Fujiwara H. Low-cost Hardening of Image Processing Applications against Soft Errors, International Symposium on Defect and Fault tolerance in VLSI Systems [C]. Washington: IEEE Computer Society, 2006: 274~279.
[80] Polian I, Reddy S M, Pomeranz I, et al. On Reducing Circuit Malfunctions Caused by Soft Errors. International Symposium on Defect and Fault tolerance in VLSI Systems [C]. Washington: IEEE Computer Society, 2008: 245~258.
[81] Polian I, Reddy S M, Pomeranz I, et al. No Free Lunch in Soft Error Protection? [C] IEEE/IFIP Workshop on Dependable and Secure Nanocomputing, 2008.
[82] Asadi G, Tahoori M B. Soft Error Modeling and Protection for Sequential Elements [C]. IEEE Symposium on Defect and Fault Tolerance in VLSI Systems, Washington: IEEE Computer Society, 2005: 463~471.
[83] Hachtel G D, Macii E, Pardo E, Somenzi F. Markovian Analysis of Large Finite State Machines [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Washington: IEEE Computer Society, 1996, 15(12): 1479~1493.
[84] D. Marculescu, R. Marculescu, and M. Pedram. Trace-Driven Steady-State Probability Estimation in FSMs with Application to Power Estimation[C]. IEEE Design, Automation and Test in Europe Conference, Washington: IEEE Computer Society, 1998: 774~779.
[85] Meyer C D. Stochastic Complementation, Uncoupling Markov Chains and the Theory of Nearly Reducible Systems [J]. SIAM Reviews, Philadelphia: Society for Industrial and Applied Mathematics, 1989, 31(2): 240~272.
[86] FMcMillan K L. Symbolic Model Checking [M]. Norwell: Kluwer Academic Publishers, 1994: 216.
[87] http://Javabdd.soureceforge.net [DB/OL].
[88] Pixley C. Formal Verification of Commercial Integrated Circuits, IEEE Design and Test of Computers [J]. Washington: IEEE Computer Society, 2001(18): 4~5.
[89] Mathur A, Balakrishnan M, Mitra R, Fujita M. Full-day Tutorial: Sequential Equivalence Checking [C]. International Conference on VLSI Design(VLSID), 2006: 2.
[90] Semeria L, Seawright A, Mehra R, Ng D, Ekanayake A, Pangrle B. RTL C-based Methodology for Designing and Verifying a Multi-threaded Processor [C]. Design Automation Conference, New York: ACM Press, 2002: 123-128.
[91] Feng X, Hu A J. Early Cutpoint Insertion for SLM Software vs. RTL Formal Combinational Equivalence Verification [C]. Design Automation Conference, New York: ACM Press, 2006: 1063~1068.
[92] Kroening D, Clarke E, Yorav K, Behavioral consistency of C and Verilog programs using bounded model checking [C]. Design Automation Conference, New York: ACM Press, 2003: 368~371.
[93] Biere A, Cimatti A, Clarke E M, Strichman O, Zhu Y. Bounded Model Checking [J]. Advances in Computers, College Park: Academic Press, 2003(58): 117~148.
[94] Kroening D, Clarke E. Checking Consistency of C and Verilog using PredicateAbstraction and Induction [C]. International Conference on Computer-Aided Design. Washington: IEEE Computer Society, 2004: 66~72.
[95] Matsumoto T, Saito H, Fujita M, Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs [C]. International Symposium on Quality Electronic Design, Washington: IEEE Computer Society, 2006: 370~375.
[96] Vasudevan S, Viswanath V, Abraham J A, Tu J. Automatic Decomposition for Sequential Equivalence Checking of System Level and RTL Descriptions [C]. International Conference on Formal Methods and Models for Co-Design, Washington: IEEE Computer Society, 2006: 71~80.
[97] Weiser M. Programmers Use Slices when Debugging [J]. Communication. New York: ACM, 1982, 25(7): 446~452.
[98] Weiser M. Program Slicing [J]. IEEE Transactions on Software Engineering, Washington: IEEE Computer Society, 1984, 10(4): 352~357.
[99]李必信等.程序切片技术及其应用[M].北京:科学出版社,2006.
[100] Berman C L, Trevillyan L H. Functional Comparison of Logic Designs for VLSI Circuits [C]. Computer-Aided Design, Washington: IEEE Computer Society, 1989: 456~459.
[101] Stump A, Barret C, Dill D. CVC: a Cooperating Validity Checker[C]. International Conference on Computer-Aided Verification, 2002: 500~504.
[102] Tu J, Viterbi Decoder Coprocessor in the DRM Application Soc [DB/OL]. http://www.cerc.utexas.edu/ shobha/masterreport.pdf.
[103] Texas 97 benchmarks. http://vlsi.colorado.edu/vis/texas-97/ [DB/OL].
[104] Hennessy J L, Patterson D A. Computer Architecture: A Quantitative Approach [M]. San Fransisco: Morgan Kaufmann Publishers, INC, 1990.
[105] http://www.antlr.org/ [DB/OL].
[106] ANTLR Reference Manual [DB/OL]. http://www.antlr.org/share/ 1084743321127/ANTLR_Reference_Manual.pdf, 2004.