Formal verification of memory interface in network processors

Abstract

In verifying the memory interface of a complex network processor, it is crucial to reduce the number of state variables in the design and the verification time. In this paper, two methods are presented for these purposes. One is to remove the temporal operator ‘NEXT’ for reducing the verification time. The other is to separate data path signals from control path signals and set data path signals as scalar set for reducing the number of state variables. The first method allowed us to reduce the verification time by the factor of 2~100 times by just adding a small number of flip-flops without changing the design. We found a bug using this method. The second method is also found out to be crucial to the success of our work as we could verify the design which could not have been verified otherwise.