Word-level symbolic simulation in processor verification

Formal verification of RT-level digital systems has attracted attention due to its efficiency over traditional simulation methods. This technology is still at its infancy and faces problems of property checking efficiency, memory explosion, and simultaneously the handling of data and control modules of hardware to be verified. Various methods of representing hardware and/or algorithms for property checking have been proposed to overcome these problems. One such method is symbolic simulation, which is attracting increasing interest in the area of digital circuit validation. It allows the verification engineer to explore all, or a major portion, of the circuitʹs state space without the need for designing time-consuming test stimuli. However, the complexity and unpredictable run-time behaviour of symbolic simulation have limited its scope to small-to-medium size circuits. A proposed solution for formal verification of digital systems is the use of symbolic simulation of a word-level representation. For this purpose a high-level model is described for digital circuits in the form of a distributed table-based representation that is suitable for application of formal verification property checking. The distributed table-based representation means that the next-state, output and intermediate signals are represented in a table that retains the hierarchy of signal assignments without flattening them. In the model a design is represented by an hierarchical structure of integer equations, instead of a binary decision diagram. A subset of PSL (property specification language) can be directly applied to circuits described in the proposed representation. In addition, a set of integer equations are symbolically simulated based on the specified property in a predictable time. The word-level representation is a canonical form of the linear Taylor expansion diagram.