Novel verification framework combining structural and OBDD methods in a synthesis environment
S.M. Reddy, Wolfgang Kunz, Dhiraj K. Pradhan · 1995
Abstract|This paper presents a new methodology for formal logic veri cation for combinational circuits.Speci cally, a structural approach is used, based on indirect implications derived by using Recursive Learning.This is extended to formulate a hybrid approach where this structural method is used to reduce the complexity o f a subsequent functional method based on OBDDs.It is demonstrated how OBDD-based veri cation can take great advantage of structural preprocessing in a synthesis environment.The experimental results show the eective compromise achieved between memory-ecient structural methods and functional methods.One more advantage of these methods lies in the fact that resources that go into logic synthesis can eectively be reused for verication purposes.