AAAI Publications, Ninth Symposium of Abstraction, Reformulation, and Approximation

Font Size: 
Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors
Miroslav N. Velev, Ping Gao

Last modified: 2011-12-14


We present a novel method for generating a wide range of equivalent Boolean encodings of cardinality, while in contrast all previous Boolean encodings of cardinality have only one form. Experiments for applying this method to automated error diagnosis in formal verification of buggy variants of a complex reconfigurable VLIW processor indicate speedup of up to two orders of magnitude, relative to previous encodings of cardinality. Besides automated debugging of hardware and software, the presented Boolean encodings of cardinality have applications to many other problems.

Full Text: PDF