An approach to verify a large scale system-on-a-chip using symbolic model checking

For system-level verification of a large-scale design, logic simulation is widely used. When a simulation trace exposes a design error a designer may rectify the design inadequately because the trace shows only one particular erroneous path. This is one of the essential problems of simulation based verification. On the other hand, model checkers are becoming widely used in industry but cannot verify large designs. We propose a new verification methodology based on a “navigated” model checking in order to overcome the above problems. We first generalize the trace and generate a property. We then verify the rectified design against the property by navigating state traversal in model checking. With navigation, we can verify designs without ad-hoc simplification and also can check various possible paths relating the error, instead of concentrating on a particular path of the trace. We have successfully verified bus transactions of a system-on-a-chip having two million transistors with our methodology. For one case, we found that the rectification was inadequate, and we fixed it successfully