SAT-based Induction for Temporal Safety Properties

The work presented in this paper addresses the challenge of fully verifying complex temporal properties on large RTL designs. Windowed induction has been proposed by Sheeran, Singh, and Stalmarck as a technique augmenting Bounded Model Checking for unbounded verification of safety properties. While induction proved to be quite effective for combinational properties, the case of temporal properties was not handled by previously known methods. We introduce explicit induction, a new induction scheme targeted to temporal properties, and to interactive development of inductive proofs. The innovative idea in explicit induction is to make the induction scheme an explicit part of the specification, where it can be easily controlled, using a highly expressive language like ForSpec. We show how explicit induction was implemented with minor modifications in the ForSpec compiler and in Thunder, a bounded model checker. Finally, we describe how explicit induction was used for verifying large control circuits with extensive feedback in the PentiumTM4 processor. The circuits verified by explicit induction are orders of magnitude larger than those verifiable by traditional model checking approaches.