Engineering a Word-Level Satisfiability Solver for RTL Design Verification
Date Issued
2009
Date
2009
Author(s)
Rau, Ruey-Shi
Abstract
Modern digital hardware design begins from register-transfer-level (RTL) description. Then, the RTL description passes through a series of design automation procedures until the physical layout is completed. Since the cost of design errors is much lower if they are found in earlier design stages, the verification on RTL is very important.he satisfiability solver is one of the essential core engines for formal verification. Therefore, this thesis proposed a word-level satisfiability solver for RTL design verification, QuteWSat. QuteWSat combines David-Putnam-Logemann-Loveland algorithm, word-level circuit description, implication procedures and conflict analysis procedures for each type of word-level logic gates. Compared with other satisfiability solvers, QuteWSat preserves the structural information about the circuit, and since it does not expand word-level logic gates into bit-level logic gates, some RTL information can be preserved and utilized in the solving process. The experimental results show that the performance of QuteWSat is comparable to that of a state-of-the-art solver.
Subjects
Verification
Satisfiability Problem
Satisfiability Solver
Register-Transfer-Level
RTL
SDGs
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-R96943067-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):1a44d32e7b63a9ef1b061ebd24c43eb6