Research On Assertion Based Verification For Design Of Digital System

As the rapid development of microelectronic technology and the market demanding on electronic products, the scale and complexity of modern integrated circuit are growing dramatically. The System on Chip (SOC) can easily use IP to compose very large integrated system, but the verification task for SOC has become the heavy burden in the design flows. We believe that verification for SOC design ought to be a mixture of simulation, semi-formal and formal methods. Assertion based verification (ABV) is an effective method which combines formal method with traditional simulation. The design intentions (assertions) are inserted into RTL design, and checked against the assertions by simulation or formal technology.This thesis studies the development in the area of assertion based verification, and presents a model checking method with three-valued atomic propositions which may appear in the abstract representation of a system. We also study the dynamic and static verification method based on Property Specification Language (PSL). The contributions of this thesis are as follows.This paper has solved the problem of three-valued logic model checking. The main problem of application on model checking is state explosion. The solution presented here is abstracting a system in order to reduce its state space. The system model is expressed by partial Kripke structure, and the semantics of a three-valued logic formula which describes the property of a system is defined under this structure. An algorithm for three-valued logic model checking is presented, as well as a prove system from which witness and counterexample can be deduced when verification result of a property is"unknown", offering the useful reference information. In the meantime, in order to apply this technology extensively, the translation from a modal transition system into a partial Kripke structure is proposed to realize a three-valued model checking based on a modal transition system.A vacuity detection method in model checking based CTL is presented. Describing a system's property, a formula is called vacuity property formula when the truth of its subformula does not affect the truth of itself during model checking. Detection on vacuity property can be accomplished by replacing atomic propositions with TRUE or FALSE, according to their polarities, to form a series of subformulae, which are then checked by model checking tool so that the result can be concluded.The application of PSL in the verification is studied. PSL gives standard means of specifying design properties of VLSI system using a concise syntax with clearly-defined semantics. Assertion based PSL can be verified through dynamic simulation and static formal verification. This thesis proposes the translation method from the subset of PSL into automata, and also gives applications on two actual design projects.