Comparative Study of Strategies for Formal Verification of High-Level Processors

Compared are different methods for evaluation of formulas expressing microprocessor correctness in the logic of Equality with Uninterpreted Functions and Memories (EUFM) by translation to propositional logic, given recently developed efficient Boolean-to-CNF translations, in order to identify the best overall translation strategy from EUFM to CNF. The translation from EUFM to propositional logic is done by exploiting the property word-level values as distinct constants while performing complete formal verification. For EUFM formulas from correct microprocessors, the best translation was by using the e ij encoding of g-equations (dual-polarity equations), the nested-ITE scheme for elimination of uninterpreted predicates, preserving the ITE-tree structure of equation arguments, and Boolean-to-CNF translation by encoding the unobservability of logic blocks by merging them with adjacent gates on the only path to the primary output. For EUFM formulas from buggy microprocessors, the best translation was by using the e ij encoding of g-equations, the Ackermann scheme for elimination of uninterpreted predicates, preserving the ITE-tree structure of equation arguments, and Boolean-to-CNF translation by applying optimizations to reduce the number of clauses—merging of ITE-trees with one level of their AND/OR leaves, and exploiting the polarity of gates and logic blocks to reduce the number of their clauses