loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Design, Automation and Test in Europe Conference and Exhibition (DATE'03)
Munich, Germany
March 03-March 07
ISBN: 0-7695-1870-2
Shuo Sheng, Rutgers University
Michael Hsiao, Virginia Tech.
Preimage computation is a key step in formal verification. Pure OBDD-based symbolic method is vulnerable to the space-explosion problem. On the other hand, conventional ATPG/SAT-based method can handle large designs but can suffer from time explosion. Unlike methods that combine ATPG/SAT and OBDD, we present a novel success-driven learning algorithm which significantly accelerates a ATPG engine for enumerating all solutions (preimages). The algorithm effectively prunes redundant search space due to overlapped solutions and constructs a free BDD on the fly so that it becomes the representation of the preimage set at the end. Experimental results have demonstrated the effectiveness of the approach, in which we are able to compute preimages for large sequential circuits, where OBDD-based method fail.
Citation:
Shuo Sheng, Michael Hsiao, "Efficient Preimage Computation Using A Novel Success-Driven ATPG," date, vol. 1, pp.10822, Design, Automation and Test in Europe Conference and Exhibition (DATE'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.