OpenSEA: Semi-Formal Methods for Soft Error Analysis

TL;DR

OpenSEA is a semi-formal tool that analyzes soft error vulnerabilities in chips by combining formal methods with designer tests, enabling scalable fault detection and protection verification.

Contribution

It introduces a novel semi-formal approach that analyzes soft error protection in chips using formal methods on input tests while keeping time-location open.

Findings

Successfully identified vulnerable and protected latches in industrial designs.

Detected tests causing false alarms in error checkers.

Validated effectiveness on real-world chip designs.

Abstract

Alpha-particles and cosmic rays cause bit flips in chips. Protection circuits ease the problem, but cost chip area and power, and so designers try hard to optimize them. This leads to bugs: an undetected fault can bring miscalculations, the checker that alarms about harmless faults incurs performance penalty. Such bugs are hard to find: circuit simulation with tests is inefficient since it enumerates the huge fault time-location space, and formal methods do not scale since they explore the whole inputs. In this paper, we use formal methods on designer's input tests, while keeping time-location open. This idea is at the core of the tool OpenSEA. OpenSEA can (i) find latches vulnerable to and protected against faults, (ii) find tests that exhibit checker false alarms, (iii) use fixed and open inputs, and (iv) use environment assumptions. Evaluation on a number of industrial designs shows that OpenSEA produces valuable results.