Unreachable code identification for improved line coverage

It is shown that line coverage during verification is significantly enhanced when applying efficient methods to remove unreachable code so that time is not spent developing a set of test vectors to cover unexecutable code. Identification of unreachable code through examination of arithmetic operations and branch constraints has previously only been achieved through local examination of surrounding instructions. In this paper a method for unreachable code identification is presented. The method models software arithmetic operations and conditions as a set of Boolean constraints for which reachability is determined using a satisfiability solver, and unreachable code can identified by considering all relevant instructions preceding it.