Complete SEU Vulnerable Register Enumeration using Property Directed Reachability

From bibtex.

Abstract

Single-event upsets are a major dependability concern in safety- and security-critical hardware. Identifying which registers are vulnerable to them is increasingly tackled by formal fault injection, i.e., driving a fault-injection campaign through a model checker. In industrial practice, this analysis is often built on top of commercial model checkers used as black boxes, which prevents algorithm-level optimization and limits scalability. As a result, several dedicated algorithms have been proposed; they rely on engines such as Binary Decision Diagrams (BDD), bounded model checking, or interpolation. However, none of them is based on Property Directed Reachability (PDR), the dominant algorithm for hardware model checking. In this paper, we present CVRE-IPDR, an algorithm for complete vulnerable register enumeration based on an incremental use of PDR. The key observation is that each enumeration step only constrains the transition relation, so the reachable state space can only shrink and previously computed PDR frames remain sound and reusable from one step to the next. On 779 circuits drawn from the Hardware Model Checking Competition, we show that CVRE-IPDR outperforms the same non-incremental baseline, whether instantiated with a PDR back-end or, on instances with more than 20 vulnerable registers, with a leading commercial model checking back-end.