Research And Implementation Of Semi-formal Verification Method For Godson2's Functional Units

With the development of integrate circuit(IC) design technology, chip design become more complex. How to make sure function correct, it is a hard question that verification engineers must solve. Since IC scales dramatically, the complexity of traditional simulation method used for functional verification increase exponentially, and the formal method can't deal with the large designs which exceed several million gates, all of this make the gap between design and verification bigger than ever before. For shorten this gap, the semi-formal verification method which combines simulation and formal became more popular. This paper hopes to make a try in this aspect (Semi-formal verification).Godson2 processors are self-dependent general processors in our country, the design of which is very complicated. In order to verify it adequately, we also hope to employ the semi-formal method. So we implemented a semi-formal verification prototype system which based on the two formal verification tools Cadence SMV and NuSMV. This semi-formal verification system include four main parts, they are design modeling, specification description, formal analysis algorithm, choice of initial state. First, we use Kripke structure to model the design which needs to verify, and express it in computer by SMV language. Then the specification is described in computation tree logic (CTL) or linear temporal logic (LTL) formula. Third, we use model checking based on SAT-BMC algorithm as our semi-formal verification system's formal analysis engine. And last directly initialization or simulation method can be employed for initial state transfer.In this paper, a reference float-point multiply-add fused unit which based on IEEE-754 standard was described. Then we verified the float-point multiply-add fused (FMAF)unit which is the one of most important functional units of Godson2. Besides of this, we compared the simulation and the semi-formal method by inserting bugs, it shows that the semi-formal method based on SAT-BMC is much better in time and stability. And got some significant results which can also be very useful when other members in our group doing semi-formal verification research.