A Novel Approach to High-Level Property Checking Using Wu´s Method

High-level property checking has attracted tremendous research effort in recent years, for traditional formal verification technologies become hard to satisfy the verification requirement which turns more and more complex gradually. In this paper, we present a novel approach to verify properties for the high-level design using Wu´s method. In the approach, the high-level design and target properties are modelled at a high abstraction level as polynomial equations and property checking is reduced to the task of theorem proving which can be solved by Wu´s method efficiently. Experimental results show that the new approach gives considerable better results then the techniques based on Boolean SAT and LP solver for the high-level design verification.