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 ive Equality, allowing us to treat most of the abstract word-level values as distinct constants while performing complete formal verification. For EUFM formulas from correct microprocessors, the best translation was by using the eij 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-toCNF translation by encoding the unobservability of logic blocks by merging them with adjacent gates on the only path to the primary output. For...

• Type: Conference
• Year: 2004
• Where: ICCD
• Authors: Miroslav N. Velev
• Keywords: Formulas Expressing Microprocessor, Hardware, ICCD 2004, Logic Blocks, Propositional Logic