Improving Safety Property Checking on RTL Design with Abstraction and Refinement Techniques
Date Issued
2010
Date
2010
Author(s)
Wu, Cheng-Yin
Abstract
Verification on modern VLSI designs has encountered a tremendous challenge for large design complexity issue, especially for verifying expected behavior from designer’s intent. Safety property checking is one of the most important problems to ensure that the hardware system will never fall into a state that is unexpected by designers. However, traditional assertion checking is conducted on gate-level Boolean circuits. The drawback is that the designer’s original intent is lost in this level. Therefore, it will be more efficient to perform safety property checking directly on high-level design abstraction.
In this thesis, we proposed a purely SAT-based safety property checking algorithm in dealing with word-level RTL designs and properties. Our approach is based on abstraction and refinement techniques to solve the problem more efficiently. Experimental results have shown that our approach has great performance improvement in runtime and convergence ability in proving difficult properties.
Subjects
Verification
Safety Property Checking
Satisfiability
Register-Transfer-Level
RTL
Abstraction and Refinement
File(s)![Thumbnail Image]()
Loading...
Name
ntu-99-R97943067-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):957eacc66c8aee78df7ed1b6c6e72fc9