1. A functional timing analysis method, comprising: step A: obtaining a circuit, by using a computing device; step B: selecting a target delay time from a delay time set for a node in the circuit, by using the computing device; step C: generating a timed characteristic function associated with the selected target delay time for the node as a target formula, by using the computing device; step D: recursively translating the timed characteristic function into timed characteristic function clauses of the target formula by using an implication-based conversion, by using the computing device; step E: using a Boolean satisfiability solver to check whether the target formula is satisfiable, by using the computing device; step F: if the target formula is satisfied, outputting the selected target delay time as an attainable true delay, by using the computing device; and step G: if the target formula is not satisfied, outputting the selected target delay time as an unattainable true delay or other relevant information, by using the computing device.