loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2007 Eighth International Workshop on Microprocessor Test and Verification
Application of Lifting in Partial Design Analysis
December 05-December 06
ISBN: 978-0-7695-3241-7
In the past, we have investigated satisfiability-based combinational equivalence checking and bounded model checking of partial circuit designs, i.e., circuit designs where one or more components of the design are not implemented yet. Especially for satisfiability-based bounded model checking, typically a counterexample is generated in case that the specification property is violated. Minimizing the number of assigned variables in the satisfying assignment that corresponds to such a counterexample is the objective of lifting. In this work we show that lifting is also feasible and profitable for counterexamples obtained via satisfiability-based bounded model checking of partial designs. We provide first experimental results on this issue that show its feasibility. Furthermore, we present a novel application scenario for lifting in the context of automated blackbox synthesis. This is a useful concept that can be applied during combinational equivalence checking of partial circuit designs, where realizability of the missing components was already proven, but the functionality of the missing components is still unknown. As a summary, this work provides first experimental results as well as a novel concept regarding the application of lifting for the analysis of partial designs.
Index Terms:
Lifting, Counterexample, Equivalence Checking, Blackbox Design
Citation:
Marc Herbstritt, Vanessa Struve, Bernd Becker, "Application of Lifting in Partial Design Analysis," mtv, pp.33-38, 2007 Eighth International Workshop on Microprocessor Test and Verification, 2007
Usage of this product signifies your acceptance of the Terms of Use.