Document Open Access Logo

A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits

Authors Dmitry Burlyaev , Pascal Fradet , Alain Girault

PDF
Thumbnail PDF

File

LITES-v005-i001-a004.pdf
  • Filesize: 0.96 MB
  • 26 pages

Document Identifiers

Author Details

Dmitry Burlyaev
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble
Pascal Fradet
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France
Alain Girault
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France

Cite AsGet BibTex

Dmitry Burlyaev, Pascal Fradet, and Alain Girault. A Static Analysis for the Minimization of Voters in Fault-Tolerant Circuits. In LITES, Volume 5, Issue 1 (2018). Leibniz Transactions on Embedded Systems, Volume 5, Issue 1, pp. 04:1-04:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LITES-v005-i001-a004

Abstract

We present a formal approach to minimize the number of voters in triple-modular redundant (TMR) sequential circuits. Our technique actually works on a single copy of the TMR circuit and considers a large class of fault mo dels of the form “at most 1 Single-Event Upset (SEU) or Single-Event Transient (SET) every k clock cycles”. Verification-based voter minimization guarantees that the resulting TMR circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial TMR circuit. Our approach operates at the logic level and takes into account the input and output interface specifications of the circuit. Its implementation makes use of graph traversal algorithms, fixed-point iterations, and binary decision diagrams (BDD). Experimental results on the ITC’99 benchmark suite indicate that our method significantly decreases the number of inserted voters, yielding a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR. As our experiments show, if the SEU fault-model is replaced with the stricter fault-model of SET, it has a minor impact on the number of removed voters. On the other hand, BDD-based modelling of SET effects represents a more complex task than the modelling of an SEU as a bit-flip. We propose solutions for this task and explain the nature of encountered problems. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.

Subject Classification

ACM Subject Classification
  • Hardware → Model checking
  • Hardware → Redundancy
Keywords
  • Digital Circuits
  • Fault-tolerance
  • Optimization
  • Static Analysis
  • Triple Modular Redundancy

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M.D. Aagaard, R.B. Jones, and C.-J.H. Seger. Formal verification using parametric representations of boolean constraints. In Design Automation Conference (DAC), pages 402-407, 1999. Google Scholar
  2. B. Baykant Alagoz. Fault masking by probabilistic voting. OncuBilim Algorithm And Systems Labs, 9(1), 2009. Google Scholar
  3. S. Baarir, C. Braunstein, et al. Complementary formal approaches for dependability analysis. In IEEE Int.Symp. on Defect and Fault Tolerance in VLSI Systems, pages 331-339, 2009. URL: http://dx.doi.org/10.1109/DFT.2009.21
  4. S. Baarir et al. Feasibility analysis for MEU robustness quantification by symbolic model checking. In Proceedings in Formal Methods of Software Design, 2011. Google Scholar
  5. A.L. Bogorad et al. On-orbit error rates of RHBDSRAMs: Comparison of calculation techniques and space environmental models with observed performance. IEEE Trans. on Nuclear Science, pages 2804-2806, 2011. Google Scholar
  6. Brendan Bridgford, Carl Carmichael, and Chen Wei Tseng. Single-event upset mitigation selection guide. Application Note XAPP987 (v1.0), Xilinx, 2008. Google Scholar
  7. P. Brinkley, P. Avnet, and C. Carmichael.SEU mitigation design techniques for the XQR4000XL. Xilinx, 2000. Google Scholar
  8. S. P. Buchner and M. P. Baze. Single-event transients in fast electronic circuits. IEEE NSREC Short Course, pages 1-105, 2001. Google Scholar
  9. Dmitry Burlyaev. Design, optimization, and formal verification of circuit fault-tolerance techniques.PhD thesis Joseph Fourier University/INRIA, November 2015. Google Scholar
  10. Dmitry Burlyaev, Pascal Fradet, and Alain Girault. Verification-guided voter minimization in triple-modular redundant circuits. In Design, Automation & Test in Europe Conference & Exhibition, DATE 2014, Dresden, Germany, March 24-28, 2014, pages 1-6, 2014. Google Scholar
  11. Dmitry Burlyaev, Pascal Fradet, and Alain Girault. Automatic time-redundancy transformation for fault-tolerant circuits. International Symposium on Field-Programmable Gate Arrays, pages 218-227, February 2015. Google Scholar
  12. Dmitry Burlyaev, Pascal Fradet, and Alain Girault. Time-redundancy transformations for adaptive fault-tolerant circuits. In NASA/ESA Conference on Adaptive Hardware and Systems (AHS), pages 1-8, 2015. Google Scholar
  13. Gianpiero Cabodi and Satnam Singh, editors. Complete and Effective Robustness Checking by Means of Interpolation. Formal Methods in Computer-Aided Design (FMCAD), 2012. Google Scholar
  14. Albert C. L. Chiang, Irving S. Reed, and Anthony V. Banes. Path sensitization, partial boolean difference, and automated fault diagnosis.IEEE Trans. Computers, 21(2):189-195, 1972. URL: http://dx.doi.org/10.1109/TC.1972.5008925
  15. E.M. Clarke, J.R. Burch, O. Grumberg, D.E. Long, and K.L. McMillan. Automatic verification of sequential circuit designs. Phil. Trans. R. Soc. Lond, series A, 339:105-120, 1992. Google Scholar
  16. F. Corno, M.S. Reorda, and G. Squillero.RT-level ITC'99 benchmarks and first ATPG results. Design Test of Computers, pages 44-53, 2000. URL: http://dx.doi.org/10.1109/54.867894
  17. Giovanni De Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill Higher Education, 1st edition, 1994. Google Scholar
  18. Dorothy E. Denning and Peter J. Denning. Certification of programs for secure information flow. Commun. ACM, 20(7):504-513, 1977. URL: http://dx.doi.org/10.1145/359636.359712
  19. Roger D. Do. New tool for FPGA designers mitigates soft errors within synthesis. DSP-FPGA.com Magazine, December 2011. Google Scholar
  20. P.E. Dodd, M.R. Shaneyfelt, J.R. Schwank, and G.L. Hash. Neutron-induced soft errors, latchup, and comparison of SER test methods for SRAM technologies. International Electron Devices Meeting, pages 333-336, 2002. Google Scholar
  21. Michael Dunn. Open source hardware IPs: OpenCores project. Logarithm Unit; Launchbird Design Systems, Inc. Floating Point Multiplier. URL: http://opencores.org.
  22. Guy Even, Joseph (Seffi) Naor, Baruch Schieber, and Madhu Sudan. Approximating minimum feedback sets and multi-cuts in directed graphs. In Int. Conf. on Int. Prog. and Combinatorial Opt., pages 14-28, 1995. Google Scholar
  23. Görschwin Fey, André Sülflow, and Rolf Drechsler. Computing bounds for fault tolerance using formal techniques. In Proceedings of the 46th Design Automation Conference, DAC, pages 190-195, 2009. Google Scholar
  24. Sandi Habinc. Functional triple modular redundancy FTMR. European Space Agency Contract Report, FPGA-003-01, 2002. Google Scholar
  25. K.J. Hass and J.W. Ambles. Single event transients in deep submicron CMOS. In 42nd Midwest Symposium on Circuits and Systems, pages 122-125 vol. 1, 1999. Google Scholar
  26. John P. Hayes, Ilia Polian, and Bernd Becker. An analysis framework for transient-error tolerance. In 25th IEEEVLSI Test Symposium (VTS 2007), 6-10 May 2007, Berkeley, California, USA, pages 249-255, 2007. Google Scholar
  27. T. Heijmen. Soft-error vulnerability of sub-100-nm flip-flops. 14th IEEE Int.On-Line Testing Symposium, pages 247-252, 2008. Google Scholar
  28. International Test Conference, ITC'03, Breaking Test Interface Bottlenecks, Charlotte (NC), USA, 2003. IEEE Computer Society. URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8970.
  29. T. Imagawa, H. Tsutsui, H. Ochi, and T. Sato. A cost-effective selective TMR for heterogeneous coarse-grained reconfigurable architectures based on DFG-level vulnerability analysis. In Design, Automation, and Test in Europe (DATE), pages 701-706, March 2013. URL: http://dx.doi.org/10.7873/DATE.2013.151
  30. B. Jeannet.MLCUDDIDL: An OCaml interface for the CUDDBDD library.http://pop-art.inrialpes.fr/ bjeannet/mlxxxidl-forge/mlcuddidl/index.html. Accessed: 2014-09-01.
  31. Jonathan M. Johnson and Michael J. Wirthlin. Voter insertion algorithms for FPGA designs using triple modular redundancy. In FPGA, pages 249-258, 2010. Google Scholar
  32. R.M. Karp. Reducibility among combinatorial problems. Complexity of Computer Computations, 43:85-–103, 1972. Google Scholar
  33. Steve Kilts. Advanced FPGA Design: Architecture, Implementation, and Optimization. Wiley-IEEE Press, 2007. Google Scholar
  34. Microsemi Corporation. Neutron-Induced Single Event Upset SEU, 55800021-0/8.11 edition, 2011. Google Scholar
  35. H. T. Nguyen and Y. Yagil. A systematic approach to SER estimation and solutions. Proc. Int. Reliability Physics Symp., pages 60-70, April 2003. Google Scholar
  36. Ilia Polian, Bernd Becker, Masato Nakasato, Satoshi Ohtake, and Hideo Fujiwara. Low-cost hardening of image processing applications against soft errors. In 21th IEEE International Symposium on Defect and Fault-Tolerance in VLSI Systems (DFT 2006), 4-6 October 2006, Arlington, Virginia, USA, pages 274-279, 2006. Google Scholar
  37. B. Pratt, M. Caffrey, P. Graham, K. Morgan, and M. Wirthlin. Improving FPGA design robustness with partial TMR. IEEE International Reliability Physics Symposium, pages 226-232, 2006. Google Scholar
  38. O. Ruano, P. Reviriego, and J.A. Maestro. Automatic insertion of selective TMR for SEU mitigation. European Conference on Radiation and its Effects on Components and Systems, pages 284-287, 2008. Google Scholar
  39. Richard Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. of CAD-93, pages 42-47, 1993. Google Scholar
  40. P.K. Samudrala et al. Selective triple modular redundancy based single-event upset tolerant synthesis for FPGAs. IEEE Transactions on Nuclear Science, pages 284-287, October 2004. Google Scholar
  41. S.A. Seshia, Wenchao Li, and S Mitra. Verification-guided soft error resilience. In DATE '07, pages 1-6, 2007. URL: http://dx.doi.org/10.1109/DATE.2007.364501
  42. P. Shivakumar, M. Kistler, S.W. Keckler, D. Burger, and L. Alvisi. Modeling the effect of technology trends on the soft error rate of combinational logic. In Dependable Systems and Networks, 2002. DSN 2002. Proceedings. International Conference on, pages 389-398, 2002. URL: http://dx.doi.org/10.1109/DSN.2002.1028924
  43. F. Somenzi.CUDD: CU Decision Diagram Package, release 2.5.0.http://vlsi.colorado.edu/ fabio/CUDD. Accessed: 2014-09-01.
  44. Angela Sutton. Creating highly reliable FPGA designs. Military&Aerospace Technical Bullentin, Issue 1:5-7, 2013. Google Scholar
  45. J. von Neumann. Probabilistic logic and the synthesis of reliable organisms from unreliable components. Automata Studies, Princeton Univ. Press, pages 43-98, 1956. Google Scholar
  46. Xilinx TMR Tool product brief, 2006. Google Scholar
  47. J.F. Ziegler et al. IBM experiments in soft fails in computer electronics (1978-1994). IBM Journal of Research and Development, 40(1):3-18, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact