Title :
Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for Boolean encoding of cardinality
Author :
Velev, Miroslav N. ; Ping Gao
Abstract :
We present a method for exploiting symmetry-breaking constraints in modular schemes for constructing equivalent Boolean encodings of cardinality constraints. These techniques result in speedup in automated debugging of complex VLIW processors in formal verification by Correspondence Checking and efficient translation to Boolean Satisfiability (SAT).
Keywords :
computability; formal verification; pipeline processing; program debugging; Boolean satisfiability; SAT; automated debugging; cardinality constraints; complex VLIW processors; correspondence checking; equivalent Boolean encodings; formal verification; modular schemes; pipelined microprocessors; symmetry breaking; symmetry-breaking constraints; Debugging; Encoding; Formal verification; Indexing; Maintenance engineering; Microprocessors; Program processors; Correspondence Checking; Logic of Equality with Uninterpreted Functions and Memories (EUFM); Positive Equality; SAT; SMT; abstraction; cardinality constraints; decision procedures; formal verification; pipelined microprocessors;
Conference_Titel :
Computer-Aided Design (ICCAD), 2014 IEEE/ACM International Conference on
Conference_Location :
San Jose, CA
DOI :
10.1109/ICCAD.2014.7001425
