DocumentCode
1787744
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
fYear
2014
fDate
2-6 Nov. 2014
Firstpage
676
Lastpage
683
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer-Aided Design (ICCAD), 2014 IEEE/ACM International Conference on
Conference_Location
San Jose, CA
Type
conf
DOI
10.1109/ICCAD.2014.7001425
Filename
7001425
Link To Document