Symbolic simulation techniques for verifying RTL circuits combining datapaths and controllers

Complexity of circuit designs has increased dramatically in order to meet technology demands, posing a problem for verification of these designs. Conventional validation methods have shown to be ineffective in verifying many such complex designs. Formal verification methods have been proposed as a solution to this problem; however, existing methods do not handle designs that combine datapaths and controllers very well. One such method, model checking, deals with controllers efficiently but not the datapaths, due to the large numbers of states in the datapaths. Theorem-proving methods may be effective for verifying datapath operations, but verifying controllers requires finding and proving inductive invariants that characterize the reachable states of the system. In practice, finding inductive invariants is the most difficult part of verification.; In this thesis, a new formal approach called finite state machine based symbolic simulation (FSMSS) is presented to verify systems that combine datapaths and controllers. FSMSS is very efficient in handling datapath operations. In addition, the FSMSS method only specifies invariants for a small set of FSM states, called clean states, where the invariants are relatively simple. The invariants for the unclean states are generated by symbolically simulating over all paths to find the possible next clean states. As a result, the FSMSS can verify very complex systems with much less effort in finding invariants.; Furthermore, FSMSS can be improved by the use of reductions for symbolic expressions. Expression reduction decreases the size of symbolic states, leading to lower memory requirements and faster verification.; Lastly, systems which cannot be formally verified can still be partially verified using the FSMSS method. The FSMSS method can be used as a debugging tool to find bugs in the design.; To demonstrate these findings, FSMSS is applied to two separate circuit designs. The first, an instruction fetch unit, demonstrates formal verification on a complex circuit design. The second, a memory interface, demonstrates partial verification by debugging when a formal verification is not possible. FSMSS was shown to successfully verify and debug these two applications, where conventional and existing formal methods were not practical.