Patent Document ID: 9389983
Application ID: 14093112
Patent Flag: 1

Claim One:
1. A computer-implemented method of verifying a hardware design of an electronic circuit comprising control logic which controls manipulation of data, said method comprising the steps of: receiving a description of said hardware design of said electronic circuit in a computer; generating, based on said description in said computer a model of said hardware design of said electronic circuit said model comprising an initial state function defining at least one initial state, a transition function defining how said hardware design moves between consecutive states and a property function defining a property that should be met for an allowable state, said initial state function, transition function and property function each comprising at least one of data, operations and predicates; generating an abstracted model defining data defining an abstracted model of said hardware design by approximating at least some of said data, operations and predicates with uninterpreted terms, uninterpreted functions and uninterpreted predicates respectively, the abstracted model defining data comprising an abstracted initial state function defining at least one abstracted initial state, abstracted transition function and abstracted property function within said abstracted model; performing a reachability analysis in the computer on said abstracted model to determine whether when starting from said at least one abstracted initial state, said hardware design can reach an unallowable abstracted state by following said abstracted transition function; and if said hardware design cannot reach an unallowable abstracted state, said hardware design is verified as correct; and if said hardware design can reach an unallowable abstracted state, unabstracting a trace of said transitions from said at least one abstracted initial state to said unallowable abstracted state and determining using said model whether steps of said unabstracted trace are feasible; and if steps of said unabstracted trace are not feasible, updating the abstracted model defining data to refine said abstracted model to preclude any infeasible steps and repeating said reachability analysis on said refined abstracted model; and if steps of said unabstracted trace are feasible, generating an error; wherein the reachability analysis comprises: determining whether each of the at least one abstracted initial state is an allowable state, and if not, determining that said hardware design can reach an unallowable state; determining whether, when starting from said at least one abstracted initial state, said hardware design can reach an unallowable abstracted state in one transition of the abstracted transition function, and if so, determining that said hardware design can reach an unallowable state; and without determining all reachable states that can be reached from said at least one abstracted initial state by following said abstracted transition function and without unrolling the abstracted transition function, determining whether the allowable states include at least one counter example to induction (CTI) state which is an allowable state from which an unallowable state can be reached in one transition of the abstracted transition function, and if said at least one CTI state is reachable from the at least one abstracted initial state by following the abstracted transition function, then determining that said CTI state is a counter example to induction and that said hardware design can reach an unallowable state.