Parametric Representations of Boolean Constraints

Abstract We describe the use of parametric representations of Boolean predicates to encode data-space constraints and signi cantly extend the capacity of formal veri cation. The constraints are used to decompose veri cations by sets of case splits and to restrict veri cations by validity conditions. Our technique is applicable to any symbolic simulator. We illustrate our technique on state-of-theart Intel(R) designs, without removing latches or modifying the circuits in any way.

• Type: Conference
• Year: 1999
• Where: DAC
• Authors: Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger
• Keywords: Computer Architecture, DAC 1999, Data-space Constraints, Formal Veri Cation, Veri Cations