Modular Schemes for Constructing Equivalent Boolean Encodings of Cardinality Constraints and Application to Error Diagnosis in Formal Verification of Pipelined Microprocessors.