Obtaining Microprocessor Vulnerability Factor Using Formal Methods

Aggressive technology down-scaling increases the vulnerability of microprocessors to runtime errors, in particular radiation-induced soft errors. In this paper, we present a technique based on Boolean satisfiability (SAT) to obtain reliability parameters of microprocessors in the presence of soft errors. We use a metric called microprocessor vulnerability factor (MVF) which captures the soft error rate of a particular implementation of the microprocessor, separating it from vulnerability factors due to the micro-codes and programs running on the microprocessor. We transform the MVF computation problem into equivalent Boolean satisfiability problem and use state-of-the-art SAT-solvers to obtain MVF. We present results for some widely used RISC processor cores and provide detailed analysis for various instructions and execution paths/resources.