A PARTIAL SOLUTION TO THE STE SPECIFICATION COMPLETENESS PROBLEM
Original Publication Date: 1997-Jun-01
Included in the Prior Art Database: 2002-May-22
Since arrays are critical components of processors, it is necessary to verify them rigorously. simulation falls short of this requirement because of the huge number of simulation patterns required for adequate coverage. The formal verification tech- nique of Symbolic Trajectory Evaluation (STE) [3,1] has shown considerable promise in solving the array verification problem. The technique of STE, given user specifications for a hardware unit, veri- fies that the unit satisfies the specifications. The specification consists of a set of assertions. Each assertion specifies an aspect of the behavior of the system being verified. While using STE, a concern often faced by the user is whether the set of assertions constituting the system specification adequately describe the functionality of the unit, and if there are aspects of the system behavior which have not been covered by any assertion. We term this problem, the STE speczjkztion complete- ness problem, and in this document we have outlined a solution to it.