SEU-X: a SEu Un-eXcitability prover for SRAM-FPGAs

We propose an untestability prover for Single Event Upset (SEU) faults affecting the configuration memory of logic resources of SRAM-FPGA systems. In particular we focus on the subset of untestable faults that can neither be excited, and for this reason we called the tool SEU-X: a SEu Un-eXcitability prover for SRAM-FPGAs. SEUs in any configuration bit of the logic resources actually used by the system are addressed. This makes our fault model much more accurate than the classical stuck-at fault model. The tool relies on the SAL specification language for the description of netlists, and on the SAL model checker for the proof of the untestability of faults. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported