Checking Safety Properties Using Induction and a SAT-Solver

Some novel induction-based methods are described, and it is shown how they are related to more standard fixpoint algorithms for invariance checking and preliminary experimental results in the verification of FPGA cores are presented.

Abstract

We take a fresh look at the problem of how to check safety properties of finite state machines. We are particularly interested in checking safety properties with the help of a SAT-solver. We describe some novel induction-based methods, and show how they are related to more standard fixpoint algorithms for invariance checking. We also present preliminary experimental results in the verification of FPGA cores. This demonstrates the practicality of combining a SAT-solver with induction for safety property checking of hardware in a real design flow.