Formal Verification of Fault-Tolerant Hardware Designs

Digital circuits for space applications can suffer from operation failures due to radiation effects. Error detection and mitigation techniques are widely accepted solutions to improve dependability of digital circuits under Single Event Upsets (SEUs) and Single Event Transients (SETs). These solutions imply design modifications that must be validated. This paper presents a formal verification method to prove that the applied fault tolerance techniques do actually prevent fault propagation as well as that the fault-tolerant circuit is functionally equivalent to the original version. The method has been implemented in an in-house software tool, VeriHard. It has been successfully applied to verify a wide variety of fault tolerance techniques, such as Triple Modular Redundancy (TMR), Duplication with Comparison (DwC), Safe Finite State Machines and Hamming encoding. Experimental results with benchmarks and industrial cases illustrates the capabilities of the method and its high performance.