Using formal techniques for identifying uninitialized registers in SoC designs

SoC designs today comprise IP blocks from different design teams and vendors. Because of differing design styles being used on IPs, integrating them and verifying them is a challenge for design teams. One of the problems that we have found while integrating is the way reset or initialisation circuitry is implemented. Lack of knowledge of IPs often cause problems late in the design flow when we perform gate level simulations with backannotated delays, thus uncovering a bug due to either incorrect integration or incorrect assumed behaviour. Transition relation of registers can be modeled using binary decision diagrams (BDD). Using constant propagation techniques in formal verification the BDDs can be reduced to constant values. This paper describes how formal verification techniques are used in identifying uninitialized registers in SoC designs.