Method for scalable liveness verification via abstraction refinement

Patent metadata

Field	Value
Publication number	US-9483595-B2
Application number	US-201514729812-A
Country	US
Kind code	B2
Filing date	Jun 3, 2015
Priority date	Jan 19, 2015
Publication date	Nov 1, 2016
Grant date	Nov 1, 2016

Abstract

Liveness verification of a logic design is performed using various shadow abstraction refinement techniques. An initial subset of state elements are included in the shadow abstraction, and verification is performed (liveness-to-safety conversion) using this initial subset. If a liveness counterexample is detected, the shadow abstraction is refined by designating a second subset of the state elements different from the initial subset for inclusion in a refined abstraction. The initial subset can be designated by choosing all registers in a combinational fan-in of a liveness property of the design. High-performance algorithms for abstract liveness-to-safety conversion can be based upon simulation and counterexample refinement, bounded model checking and counterexample refinement, bounded model checking and proof-based refinement, proofs obtained during bounded model checking of a precise liveness checking problem, a hybrid of counterexample-based refinement and proof analysis, and proofs obtained.

First claim

What is claimed is:

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.

2. The method of claim 1 wherein the circuit description includes at least one liveness property of the logic design, and the initial subset of the state elements is designated by choosing all registers in a combinational fan-in of the liveness property.

3. The method of claim 2 wherein the second subset of the state elements is designated by adding at least one selected register not in the combinational fan-in having a value which cannot be repeated in a state loop of the logic design between a start and an end of the loop.

4. The method of claim 3 wherein the second subset of the state elements includes all state elements in the initial subset.

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.

6. The method of claim 1 wherein the liveness verification includes liveness-to-safety conversion on the initial subset of the state elements.

7. The method of claim 1 wherein the circuit description includes at least one fairness property of the logic design, and said refining includes applying the fairness property to the second subset of the state elements.

Assignees

• IBM

Inventors

• Baumgartner Jason R
• Gajavelly Raj K
• Kanzelman Robert L
• Mony Hari
• Nalla Pradeep K

Classifications

• G06F30/33

  Design verification, e.g. functional simulation or model checking · CPC title

• G06F17/5022

  Physics · mapped topic

• G06F17/5045 Primary

  Physics · mapped topic

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title

• G06F30/3308 Primary

  using simulation · CPC title