Symbolic cycle simulation with closure detection towards symbolic verification

We describe the algorithms for symbolic cycle simulation of sequential designs containing hierarchies of icompletely specified functions and Boolean relations. We propose the SSTG (symbolic state transition graph), which captures both the propagation of unknown input values and the effect of icomplerteness in the specification, and we develop algorithms for SSTG closure detection. Input vectors can be presented as Boolean relations, both spatial and temporal, on previous sets of input vectors, internal states and output vectors. Moreover the SSTG can be used towards verifying the correctness of the design with repect to both synthesis and redesign.Godkänd; 1996; 20080425 (ysko