Paper Info
Title
Coping with Moore's law (and more): supporting arrays in state-of-the-art model checkers
Abstract
State-of-the-art hardware model checkers and equivalence checkers rely upon a diversity of synergistic algorithms to achieve adequate scalability and automation. While higher-level decision procedures have enhanced capacity for problems of amenable syntax, little prior work has addressed (1) the generalization of many critical synergistic algorithms beyond bit-blasted representations, nor (2) the issue of bridging higher-level techniques to problems of complex circuit-accurate syntax. In this paper, we extend a variety of bit-level algorithms to designs with memory arrays, and introduce techniques to rewrite arrays from circuit-accurate to verification-amenable behavioral syntax. These extensions have numerous motivations, from scaling formal methods to verify ever-growing design components, to enabling hardware model checkers to reason about software-like systems, to allowing state-of-the-art model checkers to support temporally-consistent function- and predicate-abstraction.
Year
Venue
Keywords
2010
FMCAD
complex circuit-accurate syntax,behavioral syntax,synergistic algorithm,higher-level technique,state-of-the-art hardware model checker,critical synergistic algorithm,state-of-the-art model checker,amenable syntax,higher-level decision procedure,enabling hardware model checker,formal verification,redundancy,logic gates,data models,formal method,formal methods,cognition
Field
DocType
Citations 
Data modeling,Computer science,Theoretical computer science,Automation,Equivalence (measure theory),Formal methods,Syntax,Formal verification,Scalability,Moore's law
Conference
2
PageRank 
References 
Authors
0.40
16
3
Name
Order
Citations
PageRank
Jason Baumgartner131323.36
Michael Case2446.66
Hari Mony318613.30