Patent Document ID: 9483595
Application ID: 14729812

Base Claim:
1. A method of verifying liveness of a logic design comprising: receiving a circuit description for the logic design which includes vertices representing gates and edges representing interconnections between the gates, wherein portions of the gates represent different state elements which are evaluated to determine a state of the logic design, by executing first instructions in a computer system; designating an initial subset of the state elements for inclusion in an abstraction of the logic design, by executing second instructions in the computer system; performing liveness verification on the abstraction based on the initial subset of the state elements, by executing third instructions in the computer system; detecting a liveness counterexample in response to said performing the liveness verification, by executing fourth instructions in the computer system; and refining the abstraction by designating a second subset of the state elements different from the initial subset for inclusion in a refined abstraction, by executing fifth instructions in the computer system.

---

Claim 5:
5. The method of claim 1 further comprising subsequently performing a liveness verification on the refined abstraction, again detecting a liveness counterexample in response to the subsequent performing, and further refining the abstraction designating a subsequent subset of state elements different from previous subsets for inclusion in a further refined abstraction, wherein said subsequently performing, again detecting, and further refining are repeated iteratively.