Logic insertion to speed-up logic verification: a recent development

Logic verification continues to be considered one of CAD´s most difficult problems, highlighted with the discovery of the Pentium bug dilemma. This paper reviews certain current innovations addressing such problems. A new method is discussed, based on what has become known as the Recursive Learning Technique. This proposed technique has its cornerstone in Boolean implication techniques - proven most powerful when traditional approaches, such as OBDD, fail. In fact, Recursive Learning was the first to verify the ISCAS benchmark circuits - discovering some bugs in the process