Research On Formal Methods In Arithmetic Circuit Verification

Arithmetic circuit is one of the key components of modern microprocessor. The verification of microprocessor design must ensure the correctness of arithmetic circuit. As the increase of circuit complexity, traditional simulation method has been unable to cover the total state space and the correctness of microprocessor arithmetic circuit cannot be ensured. Thus, using formal verification, especially model checking method (an completely automated method), to verify arithmetic circuits effectively becomes a hot spot concerned by world wide R&D institutes and EDA vendors.Based on the work in design and verfication of floating-point arithmetic circuit in Godson-I microprocessor, this dissertation gives a systematic research on the specification language, decision diagram based model checking method and verification methodologies as well as SAT based model checking method in the verification of arithmetic circuit. The detailed research improvements are as follows.1. The syntax and semantics of CTL formula in arithmetic circuit is defined. Based on the semantics of CTL formula in arithmetic circuit, model checking method for CTL formula is presented and the model checking method is implemented using *PHDD.2. The general optimization principle of arithmetic operation algorithms on *PHDD is presented. Moreover, for division and modulus operation with radix of power-of-2 integer, which is common in arithmetic circuit verification, four theories are introduced to simplify the algorithm running process. These optimization techniques improve the efficiency of arithmetic operation algorithms on *PHDD greatly.3. An upper bound and lower bound calculation algorithm on *PHDD is introduced, which makes the upper bound and lower bound of function closer to the maximum value and minimum value of function. In this case, it is more possible to satisfy reduction conditions for upper bound and lower bound of function. Thus, there are more operations reduced.4. A new conditional restriction algorithm with condition preprocessing is brought forward to reduce the run time of conditional restriction algorithm. Besides, multi-level conditional restriction mechanism and conditional filtering mechanism are given to decrease the size of condition and eliminate useless restriction function calls.5. SAT algorithm is extended to verify arithmetic circuit. Experiments illustrate that SAT based verification method is high efficient in verifying wrong arithmetic circuits or strictly...