Static Property Checking Using ATPG v.s. BDD Technique

		  Chung-Yang (Ric) Huang, Bwolen Yang,
		 Huan-Chih Tsai, Kwang-Ting (Tim) Cheng



Abstract:

Static property checking is a technique for verifying some pre-defined
design rules such as "bus contention", "racing condition", and
"don't-care case".  It contains formal verification engines so that a
property can be completely verified and if the property is proven false,
a counterexample will be generated for debugging the design.  Among the
different static property checking approaches, ATPG-based and BDD-based
are the most powerful and successful ones.  We implement both engines
with several optimization techniques on the same framework such that
their performance can be compared.  The experimental results on some
industrial designs show that both approaches have different strength and
weakness in proving the static properties.  Furthermore, our experience
shows that they often complement each other and therefore a hybrid
approach will be the best strategy.  We combined these two approaches by
alternating them with successively increased proof effort.  The
experimental results show that this combined approach do produce the
best performance.




@INPROCEEDINGS(huang:itc00,
    key="atpg bdd study",
    author="Chung-Yang (Ric) Huang and Bwolen Yang and
            Huan-Chih Tsai and Kwang-Ting (Tim) Cheng",
    Title="Static Property Checking Using ATPG v.s. BDD Technique",
    BookTitle="Proceedings of International Testing Conference",
    pages="To Appear",
    year="2000",
    month="October")