Abstract: Transaction based formal verification (TBFV) methodology for verification of circuit system is presented. With this method, the validation engineer can verify the system at behavior level, needn't understand the detailed implementation. To illustrate this method, we verified the RTL implementation of 8051. We gave the set of TBFV models for the instructions set of 8051. With the help of these models, the validation engineer can improve their work efficiency.