RTL design verification by making use of datapath information

An RTL (register level) design verification method that first separates a given design into a datapath and a control circuit and fully utilizes information obtained from the datapath when verifying the control circuit is presented. The method has been successfully applied to the verification of a real 20K-gate chip that performs interface control between processors and networks in a parallel machine. So far, one fifth of the functions of the chip have been verified, in less than a 1 min on SPARC2