Checking Safety Properties Using Induction and a SAT-Solver

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.

• Type: Conference
• Year: 2000
• Where: FMCAD
• Authors: Mary Sheeran, Satnam Singh, Gunnar Stålmarck
• Keywords: Finite State Machines, FMCAD 2000, Formal Methods, Safety Properties, Safety Property Checking