A method of detecting a circuit malfunction in a register transfer level, RTL, design stage is disclosed. The method comprises obtaining signal points of each register from a circuit model based on the RTL design stage, generating a property list according to the signal points of each register, wherein the property list includes a property to be verified for each signal point, performing a formal verification operation according to the circuit model and the property list, to determine whether the property of the property list for each signal point in the circuit model is true, and generating a circuit malfunction result according to the signal point whose property is not true.