A new approach for early dependability evaluation based on formal property checking and controlled mutations

The interest for early analyses of the functional impact of faults in a circuit is growing, due to the increasing probability of transient faults. However, experiments are often very long, especially when spatial and temporal multiplicity has to be taken into account in the fault model. Formal property checking is an appealing approach to perform comprehensive functional validations but is intended to validate properties only in nominal operation, not after a fault has occurred. This paper proposes a new approach combining formal property checking and the generation of specific circuit mutants to achieve efficient early identification of unacceptable effects of multiple faults.