Sciweavers

Share
ICCD
2004
IEEE

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

9 years 7 months ago
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...
Miroslav N. Velev
Added 16 Mar 2010
Updated 16 Mar 2010
Type Conference
Year 2004
Where ICCD
Authors Miroslav N. Velev
Comments (0)
books