Exploiting hierarchical encodings of equality to design independent strategies in parallel SMT decision procedures for a logic of equality

With the number of processor cores in modern CPUs growing exponentially, it is expected that CPUs will have on the order of a hundred cores in the next 5 - 7 years. Thus, the need to implement parallel SMT decision procedures to utilize the increasing number of cores. We study a method to design independent strategies for a portfolio of parallel independent strategies in an SMT decision procedure for the logic of Equality with Uninterpreted Functions and Memories (EUFM). Particularly, our goal is to complement the previously used relative encoding (also called e_ij encoding) and logarithmic encoding of equations by exploiting hierarchical encodings of equations. Hierarchical encodings can have a wide variety of structures, where each level of the hierarchy uses a different simple encoding, and thus the potential for many possible translations to SAT with such encodings. Hierarchical encodings produced a speedup of at least an order of magnitude for an out-of-order superscalar processor with issue/retire width of 14 instructions per clock cycle, such that the speedup increases with the complexity of the microprocessor under formal verification.