Representation and Manipulation of Inductive Boolean Functions.

摘要

TV high level of complexity of current hardware systems has led to an interest in formal methods for proving their correctness. Reasoning by induction is a powerful formal proof method with the advantages the a single proof establishes the correctness of an entire family of circuits varying according to some size parameter, and the size of this proof is independent of the size of the circuit. Tautology-checking of symbolic Boolean functions is another method that has been successfully used in formal verification, both for checking equivalence/satisfaction with respect to a functional specification and as a basis for modelchocking. In this paper we present a representation and algorithms for symbolic manipulation of inductive Boolean functions, based on extensions of Binary Decision Diagrams. Our approach allows us to combine reasoning by induction with efficient tautology-checking in an automatic way.