Computing bounds for fault tolerance using formal techniques

ABSTRACT

Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults, e.g. due to environmental radiation. Approaches to implement fault tolerance are known. But assessing the fault tolerance of a given circuit is a tough problem.

Here, we propose the use of formal methods to assess the robustness of a digital circuit with respect to transient faults. Our formal model uses a fixed bound in time to cope with the complexity of the underlying sequential equivalence check. The result is a lower and an upper bound on the robustness. The underlying algorithm and techniques to improve the efficiency are presented. In experiments the method is evaluated on circuits with different fault detection mechanisms.

REFERENCES

• 1: T. Austin and V. Bertacco. Deployment of better than worst-case design: Solutions and needs. In Int'l Conf. on Comp. Design, pages 550--558, 2005.
• 2: A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of LNCS, pages 193--207. Springer Verlag, 1999.
• 3: M. Bozzano, A. Cimatti, and F. Tapparo. Symbolic fault tree analysis for reactive systems. In Automated Technology for Verification and Analysis, volume 4762 of LNCS, pages 162--176, 2007.
• 4: R. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp., 35(8):677--691, 1986.
• 5: P. Chauhan, E. Clarke, and D. Kroening. Using SAT based image computation for reachability analysis. Technical Report CMU-CS-03-151, School of Computer Science, Carnegie Mellon University, 2003.
• 6: P. Civera, L. Macchiarulo, M. Rebaudengo, M. S. Reorda, and M. Violante. An FPGA-based approach for speeding-up fault injection campaigns on safety-critical circuits. Jour. of Electronic Testing: Theory and Applications, 18(3):261--271, 2002.
• 7: M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:506--521, 1960.
• 8: R. Drechsler, S. Eggersglüß, G. Fey, A. Glowatz, F. Hapke, J. Schlöffel, and D. Tille. On acceleration of SAT-based ATPG for industrial designs. IEEE Trans. on CAD, 27(7):1329--1333, 2008.
• 9: N. Eén and N. Sörensson. An extensible SAT solver. In SAT 2003, volume 2919 of LNCS, pages 502--518, 2004.
• 10: D. Ernst, N. S. Kim, S. Das, S. Pant, T. Pham, R. Rao, C. Ziesler, D. Blaauw, T. Austin, and T. Mudge. Razor: A low-power pipeline based on circuit-level timing speculation. In Micro Conference, 2003.
• 11: G. Fey and R. Drechsler. A basis for formal robustness checking. In Int'l Symp. on Quality Electronic Design, pages 784--789, 2008.
• 12: R. W. Hamming. Error detecting and error correcting codes. Bell System Technical Jour., 9:147--160, April 1950.
• 13: U. Krautz, M. Pflanz, C. Jacobi, H. W. Tast, K. Weber, and H. T. Vierhaus. Evaluating coverage of error detection logic for soft errors using formal methods. In Design, Automation and Test in Europe, pages 176--181, 2006.
• 14: T. Lengauer and R. E. Tarjan. A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst., 1(1):121--141, 1979.
• 15: R. Leveugle. A new approach for early dependability evaluation based on formal property checking and controlled mutations. In IEEE International On-Line Testing Symposium, pages 260--265, 2005.
• 16: M. Miskov-Zivanov and D. Marculescu. Circuit reliability analysis using symbolic techniques. IEEE Trans. on CAD, 25(12):2638--2649, 2006.
• 17: M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conf., pages 530--535, 2001.
• 18: A. Pellegrini, K. Constantinides, D. Zhang, S. Sudhakar, V. Bertacco, and T. Austin. CrashTest: A fast high-fidelity FPGA-based resiliency analysis framework. In Int'l Conf. on Comp. Design, 2008.
• 19: S. A. Seshia, W. Li, and S. Mitra. Verification-guided soft error resilience. In Design, Automation and Test in Europe, pages 1442--1447, 2007.
• 20: P. Shivakumar, M. Kistler, S. W. Keckler, D. Burger, and L. Alvis. Modeling the effect of technology trends on the soft error rate of combinational logic. In Int'l Conf on Dependable Systems and Networks, pages 389--398, 2002.
• 21: A. Smith, A. Veneris, M. Fahim Ali, and A. Viglas. Fault diagnosis and logic debugging using boolean satisfiability. IEEE Trans. on CAD, 24(10):1606--1621, 2005.
• 22: P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli. Combinational test generation using satisfiability. IEEE Trans. on CAD, 15:1167--1176, 1996.
• 23: G. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2, pages 115--125, 1968. (Reprinted in: J. Siekmann, G. Wrightson (Ed.), Automation of Reasoning, Vol. 2, Springer, Berlin, 1983, pp. 466--483.).
• 24: J. Whittemore, J. Kim, and K. Sakallah. SATIRE: A new incremental satisfiability engine. In Design Automation Conf., pages 542--545, 2001.
• 25: C. Zhao and S. Dey. Improving transient error tolerance of digital VLSI circuits using RObustness COmpiler (ROCO). In Int'l Symp. on Quality Electronic Design, pages 133--140, 2006.
• 26: Q. Zhou and K. Mohanram. Gate sizing to radiation harden combinational logic. IEEE Trans. on CAD, 25(1):155--166, 2006.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

General Terms:
Verification

Keywords:
SAT, fault tolerance, formal verification