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

Dmitry Burlyaev, Pascal Fradet, Alain Girault

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.

Keywords


Digital Circuits; Fault-tolerance; Optimization; Static Analysis; Triple Modular Redundancy

Full Text:

PDF

References


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.

B. Baykant Alagoz. Fault masking by probabilistic voting. OncuBilim Algorithm And Systems Labs, 9(1), 2009.

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

S. Baarir et al. Feasibility analysis for MEU robustness quantification by symbolic model checking. In Proceedings in Formal Methods of Software Design, 2011.

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.

Brendan Bridgford, Carl Carmichael, and Chen Wei Tseng. Single-event upset mitigation selection guide. Application Note XAPP987 (v1.0), Xilinx, 2008.

P. Brinkley, P. Avnet, and C. Carmichael.SEU mitigation design techniques for the XQR4000XL. Xilinx, 2000.

S. P. Buchner and M. P. Baze. Single-event transients in fast electronic circuits. IEEE NSREC Short Course, pages 1-105, 2001.

Dmitry Burlyaev. Design, optimization, and formal verification of circuit fault-tolerance techniques.PhD thesis Joseph Fourier University/INRIA, November 2015.

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.

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.

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.

Gianpiero Cabodi and Satnam Singh, editors. Complete and Effective Robustness Checking by Means of Interpolation. Formal Methods in Computer-Aided Design (FMCAD), 2012.

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

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.

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

Giovanni De Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill Higher Education, 1st edition, 1994.

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

Roger D. Do. New tool for FPGA designers mitigates soft errors within synthesis. DSP-FPGA.com Magazine, December 2011.

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.

Michael Dunn. Open source hardware IPs: OpenCores project. Logarithm Unit; Launchbird Design Systems, Inc. Floating Point Multiplier. URL: http://opencores.org.

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.

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.

Sandi Habinc. Functional triple modular redundancy FTMR. European Space Agency Contract Report, FPGA-003-01, 2002.

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.

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.

T. Heijmen. Soft-error vulnerability of sub-100-nm flip-flops. 14th IEEE Int.On-Line Testing Symposium, pages 247-252, 2008.

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.

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

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.

Jonathan M. Johnson and Michael J. Wirthlin. Voter insertion algorithms for FPGA designs using triple modular redundancy. In FPGA, pages 249-258, 2010.

R.M. Karp. Reducibility among combinatorial problems. Complexity of Computer Computations, 43:85-–103, 1972.

Steve Kilts. Advanced FPGA Design: Architecture, Implementation, and Optimization. Wiley-IEEE Press, 2007.

Microsemi Corporation. Neutron-Induced Single Event Upset SEU, 55800021-0/8.11 edition, 2011.

H. T. Nguyen and Y. Yagil. A systematic approach to SER estimation and solutions. Proc. Int. Reliability Physics Symp., pages 60-70, April 2003.

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.

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.

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.

Richard Rudell. Dynamic variable ordering for ordered binary decision diagrams. In Proc. of CAD-93, pages 42-47, 1993.

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.

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

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

F. Somenzi.CUDD: CU Decision Diagram Package, release 2.5.0.http://vlsi.colorado.edu/ fabio/CUDD. Accessed: 2014-09-01.

Angela Sutton. Creating highly reliable FPGA designs. Military&Aerospace Technical Bullentin, Issue 1:5-7, 2013.

J. von Neumann. Probabilistic logic and the synthesis of reliable organisms from unreliable components. Automata Studies, Princeton Univ. Press, pages 43-98, 1956.

Xilinx TMR Tool product brief, 2006.

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.




DOI: https://doi.org/10.4230/LITES-v005-i001-a004

URN (PDF): http://nbn-resolving.de/urn:nbn:de:0030-lites-v005-i001-a004-pdf3

Copyright (c) 2018 Dmitry Burlyaev, Pascal Fradet, and Alain Girault

Creative Commons License CC BY
This work is licensed under a Creative Commons Attribution 3.0 Germany License (CC BY 3.0 DE).

License URL: http://creativecommons.org/licenses/by/3.0/de/deed.en
To make this site work properly, we sometimes place small data files called cookies on your device. Cookies are only here to manage user sessions. Cookies aren’t required for simply visiting the site and read content.
OK




Published by the European Design and Automation Association (EDAA) \ EMbedded Systems Special Interest Group (EMSIG) and Schloss Dagstuhl -- Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing. | Imprint | Data Privacy Policy