RTL Property Checking Based On Linear Programming

Verification of VLSI has become the main obstacle from researching anddevelopment of VLSI. Simulation method cannot meet with the tremendousverification demand of SOC (System-On-Chip). Thus, formal verification is placedemphasis on as an important assistant. Model Checking is one of formalverification and the hot because of the trait of high automatism andwide application level such as switch level and Register Transfer level.With the scale increasing of system, State Space Explosion obstructsfrom its further application. Bound Model Checking (BMC) emerges asthe times require and is based on BDD or Boolean SAT. But RTL(Register Transfer Level) design is the main stream of VLSI and hasbit-word hybrid constraints which lead to low verification efficiency ofBMC.One novel method is presented in this dissertation. This methodfirstly extends circuits by timeframe, models RTL circuits in LinearProgramming (LP) constraints to generate implicit FSM, thentransforms property into LP constraints and lastly gets verificationresult by LP solver. Experimental result shows that our method hasmore advantage in CPU time and memory consumption compared withtraditional BMC.Meanwhile, when researching the above method, we find that ifhierarchical module structure of RTL designs would be added intoverification process, the high performance must be obtained. Wedevelop further H-LPSAT using this strategy and deal with hierarchicalRTL designs. Experimental result supports our expectation thatH-LPSAT is more effective than the above method, especially in factorof CPU time consumption.