Use of random simulation in formal verification

Abstract

In this paper we present the application of random simulation in formal verification of functional equivalence of hardware designs. We demonstrate that random simulation can effectively complement BDD-based verification approaches in three areas: (1) quick generation of counter example pattern for miscomparing designs, (2) exhaustive comparison of small functions, and (3) providing meaningful signatures for design partitioning based on functionally equivalent cut-points. The presentation describes a smooth and efficient integration of a simulation algorithm into a general verification framework. In this framework the simulator can be applied as one of various engines for Boolean reasoning the outcome of which might be undecided.