RTL formal verification of embedded processors

Presents a technique for formal verification of processors. The verification process is performed at the RTL level of implementation, which has the advantage of being synthesizable by a synthesis tool. Cadence SMV is used as the verification tool. It employs the symbolic model checking technique. A stepwise verification method is proposed where the details of design are increased in each step. This method facilitates the error finding process. The proposed technique can reduce the complexity of the verification process and enables it to be completed in a reasonable time. The technique is illustrated on a simple processor used in an embedded Web server. The design is verified successfully.