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 present 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.
