Formal verification of embedded SoC

SoC (System on a Chip) are becoming more and more popular due to their widespread applications and the improved techniques. In many cases, the safety is very important. For SoC, the traditional validation techniques, such as simulation and testing, are not viable. Formal methods are becoming a practical alternative to ensure the correctness of the design. In this paper, we investigate the modeling and formal verification of a SoC using Cadence SMV. We use a hierarchical approach to model and formally verify a complete system at different levels