Title :
ATLAS: Automatic Term-level abstraction of RTL designs
Author :
Brady, Bryan A. ; Bryant, Randal E. ; Seshia, Sanjit A. ; O´leary, John W.
Author_Institution :
UC Berkeley, Berkeley, CA, USA
Abstract :
Abstraction plays a central role in formal verification. Term-level abstraction is a technique for abstracting word-level designs in a formal logic, wherein data is modeled with abstract terms, functional blocks with uninterpreted functions, and memories with a suitable theory of memories. A major challenge for any abstraction technique is to determine what components can be safely abstracted. We present an automatic technique for term-level abstraction of hardware designs, in the context of equivalence and refinement checking problems. Our approach is hybrid, involving a combination of random simulation and static analysis. We use random simulation to identify functional blocks that are suitable for abstraction with uninterpreted functions. Static analysis is then used to compute conditions under which such function abstraction is performed. The generated term-level abstractions are verified using techniques based on Boolean satisfiability (SAT) and satisfiability modulo theories (SMT). We demonstrate our approach for verifying processor designs, interface logic, and low-power designs. We present experimental evidence that our approach is efficient and that the resulting term-level models are easier to verify even when the abstracted designs generate larger SAT problems.
Keywords :
computability; data structures; formal verification; integrated circuit design; microprocessor chips; Boolean satisfiability; RTL designs; SAT problems; automatic term-level abstraction; formal logic; formal verification; function abstraction; interface logic; low-power designs; microprocessor design verification; processor design verification; random simulation; refinement checking problems; register-transfer-level descriptions; satisfiability modulo theories; static analysis; word-level design abstraction; Analytical models; Computational modeling; Data models; Hardware design languages; Integrated circuit modeling; Nickel; Syntactics;
Conference_Titel :
Formal Methods and Models for Codesign (MEMOCODE), 2010 8th IEEE/ACM International Conference on
Conference_Location :
Grenoble
Print_ISBN :
978-1-4244-7885-9
Electronic_ISBN :
978-1-4244-7886-6
DOI :
10.1109/MEMCOD.2010.5558624