Verification-guided voter minimization in triple-modular redundant circuits

We present a formal approach to minimize the number of voters in triple-modular redundant sequential circuits. Our technique actually works on a single copy of the circuit and considers a user-defined fault model (under the form "at most 1 bit-flip every k clock cycles"). Verification-base...

Full description

Saved in:
Bibliographic Details
Main Authors: Burlyaev, Dmitry, Fradet, Pascal, Girault, Alain
Format: Conference Proceeding
Language:English
Subjects:
Circuit faults
Clocks
Computer architecture
Integrated circuit modeling
Microprocessors
Semantics
Tunneling magnetoresistance
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a formal approach to minimize the number of voters in triple-modular redundant sequential circuits. Our technique actually works on a single copy of the circuit and considers a user-defined fault model (under the form "at most 1 bit-flip every k clock cycles"). Verification-based voter minimization guarantees that the resulting circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial one. 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 BDDs. Experimental results on the ITC'99 benchmark suite indicate that our method significantly decreases the number of inserted voters which entails a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.
ISSN:1530-1591
1558-1101
DOI:10.7873/DATE.2014.105