The Parametric Representation

Abstract

The parametric representation of Boolean predicates can dramatically increase the capacity of formal verification based on symbolic simulation. This approach is useful for restricting verification to a care set and for reducing verification complexity through input-space decomposition. Our technique is independent of the symbolic simulation algorithm, does not require any modifications to the circuit, can be used to constrain both input and internal signals, and is applicable to a wide variety of circuits. The application of the approach to the synthetic hidden-weighted-bit circuit [Bry91] is described in detail. In the next chapter, the approach is applied to the verification of two large Intel circuits: a second IA-32 instruction decoder and an IEEE-compliant floatingpoint adder/subtracter. A preliminary version of the work in this chapter appeared in [AJS99a].