Improving Safety Property Checking by High-Level Design Information
Date Issued
2009
Date
2009
Author(s)
Ye, Jhen-Cheng
Abstract
Safety property checking is an important technique in design verification. It ensures the correctness of the expected design behavior, or, when the property is falsified, provides a counter example for debugging. In recent years, the problem is solved well with the help of SAT solver. Due to the nature of SAT solver, the problem input is translated into a bit-level logic formula and focused on the operation of bit-level logic like CNF minimization and abstraction and refinement technique. However, the problem is originally described in the RTL design. The high level design information such as Finite State Machine (FSM) and word-level expression might be helpful for the safety property checking problem. In this thesis, the word-level expression is used to reduce the logic representation, and the information provided by FSM is used to guide the SAT solver by path constraint. Our experimental result showed that the performance is closed to one of the safety property checker ABC. The performance with path constraint even wins the ABC. Thus, the high level design information does have a good effect on safety property checking.
Subjects
safety property checking
high level design information
word-level expression
Finite State Machine(FSM)
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-R96943069-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):4d628123de63fbfff7933c93e9b6ed1c