High-Level Bounded Model Checking Using Wu's Method

A bounded model checking method for the high-level design verification using Wu's method is proposed. By modeling high-level designs and targeting properties as polynomial equations, bounded model checking is reduced to the task of theorem proving, which can be solved by Wu's method efficiently. Experimental results demonstrated the superiority in time consumption of the proposed approach compared with the property checking methods based on Boolean SAT, LP-based RTL SAT and non-linear solver.