Formal Verification of Godson-2 Microprocessor Floating-Point Division Unit

Word level model checking based on decision diagrams can verify arithmetic circuits completely, but its bug finding is time-consuming. SAT-based bounded model checking is powerful in bug finding, but it does not support specification with mathematic formula. In this paper, the SAT-based word level model checking method is presented. This method extends CNF to E-CNF which can represent both Boolean formula and mathematic formula, and extends bounded model checking and SAT solver to word level to cooperate with E-CNF. Experiments show that SAT-based model checking is powerful in bug finding for arithmetic circuit. The verification of floating-point division unit of Godson-2 microprocessor adopts both *PHDD-based and SAT-based model checking methods. These two methods are excellently complementary to each other, giving the ability to completely verify design as well as shorten design cycle.