Checking safety properties using induction and a SAT-solver

Mary Sheeran, Satnam Singh and Gunnar Staalmarck

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems