Browse Prior Art Database

Method for a satisfiability solver to improve the debugging of logical defects in industrial-scale VLSI design verification

IP.com Disclosure Number: IPCOM000008838D
Publication Date: 2002-Jul-17
Document File: 3 page(s) / 117K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is a method for a satisfiability solver to improve the debugging of logical defects in industrial scale VLSI design verification. Benefits include improved functionality and an improved development environment.

This text was extracted from a Microsoft Word document.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 50% of the total text.

Method for a satisfiability solver to improve the debugging of logical defects in industrial-scale VLSI design verification

Disclosed is a method for a satisfiability solver to improve the debugging of logical defects in industrial scale VLSI design verification. Benefits include improved functionality and an improved development environment.

Background

              Validation teams spend a lot of CPU-time and manpower debugging logical defects in industrial-scale VLSI design verification. The debug process consists of two main stages:

1.      Failure analysis

2.      Defect rectification

      The conventional debugging of logical defects is even more challenging when the design has been verified using formal methods. Formal verification based on symbolic model checking, while a very valuable method for verifying commercial sequential designs, is still limited with respect to the size of the verifiable designs. This capacity problem affects productivity. An extensive manual effort is required to decompose the proofs into simpler proof obligations even when automatic methods are used to prune the model. The abstractions and assumptions required to obtain a verification case increase the chance of false failure reports. Spurious failures cause the verifier to loop between model checking and specification modification, hindering productivity.

              For valid failure reports, back-tracing to the root cause and debugging are difficult. As the counter-example is abstract, extending it to the full model’s input is difficult. To determine if a bug is spurious or not, the effects of pruning and environmental assumptions made to verify the design under test must be understood in detail. The difficulty to debug counter-examples generated by formal verification tools endangers the potential of formal verification as a valid verification tool for the designers.

Description

      The disclosed method addresses the debug challenge in formal verification by introducing a satisfiability (SAT) solver technology. When given a failure, the method can detect automatically whether the failure is spurious or not. Additionally, the method enriches the trace that demonstrates the failure with additional information that facilitates the rectification of the failure.

              Counter-example analysis (CexAn) determines whether an abstract counter-example holds true in the full model. If so, the counter-example is extended to the full model's inputs. The deployment of the new counter-example analysis and extension method in practice on real-life industrial formal verification has been proven to be very beneficial. It addresses the shortcomings of analysi...