DocumentCode :
435225
Title :
On using a 2-domain partitioned OBDD data structure in verification
Author :
Feng, Tao ; Wang, Li.-C. ; Cheng, Kwang-Ting ; Lin, A.C.-C.
Author_Institution :
Cadence Design Syst. Inc., San Jose, CA, USA
fYear :
2004
fDate :
10-12 Nov. 2004
Firstpage :
49
Lastpage :
54
Abstract :
In this paper, we propose a symbolic simulation method where Boolean functions can be efficiently manipulated through a 2-domain partitioned OBDD data structure. The functional partition is applied based on the key decision points in a circuit. We demonstrate that key decision points in an RTL model can be extracted automatically to facilitate verification at the gate level. The experiments show that the decision points can help to significantly reduce the OBDD size in both RTL and gate level circuit, solving problems that could not be solved with monolithic OBDD data structure. The performance of 2-domain partitioned OBDD approach is shown through the verification of several benchmark circuits.
Keywords :
Boolean functions; binary decision diagrams; data structures; formal verification; Boolean functions; RTL model; gate level circuit; monolithic OBDD data structure; symbolic simulation method; verification tool; Binary decision diagrams; Boolean functions; Buildings; Circuit simulation; Data mining; Data structures; Polynomials; Robustness;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
High-Level Design Validation and Test Workshop, 2004. Ninth IEEE International
ISSN :
1552-6674
Print_ISBN :
0-7803-8714-7
Type :
conf
DOI :
10.1109/HLDVT.2004.1431234
Filename :
1431234
Link To Document :
بازگشت