Abstract: Logic verification continues to be considered one of CAD's most difficult problems, highlighted with the discovery of the Pentium bug dilemma. This talk reviews certain current innovations addressing such problems. A new method will be discussed, based on what has become known as 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 come bugs in the process. This work has won the 1996 IEEE Transactions on CAD I Best Paper A ward, & was patented the same year. Several CAD companies currently implement this technique in their tool.