Browse Prior Art Database

Method to accelerate SAT-based formal verification of RTL assertions in industrial scale VLSI designs

IP.com Disclosure Number: IPCOM000010051D
Publication Date: 2002-Oct-16
Document File: 8 page(s) / 151K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is a method to accelerate satisfiability solver (SAT) based formal verification of resister transistor logic (RTL) assertions in industrial very large scale integration (VLSI) designs. Benefits include faster verification and verification of more properties.

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 25% of the total text.

Method to accelerate SAT-based formal verification of RTL assertions in industrial scale VLSI designs

Disclosed is a method to accelerate satisfiability solver (SAT) based formal verification of resister transistor logic (RTL) assertions in industrial very large scale integration (VLSI) designs. Benefits include faster verification and verification of more properties.

Background

              During the development of the resistor transistor logic (RTL), the designer has very detailed knowledge about the intent of the design. The designer develops the hardware specification with the intent that certain conditions and behaviors occur. In the electronic design automation (EDA) industry, there is a momentum in the recent years to include RTL-assertions as a means to check whether the intent and hardware specification is correct. The RTL intent is to be verified through dynamic or formal verification tools.

              Using SAT software does not require any tuning or particular expertise. The high capacity and usability of the bounded model checker (BMC) make it especially attractive for automatic verification of RTL assertions.

              Two limitations have been identified with respect to RTL assertion verification. Only one
property is checked at a time. For multiple properties, each property is checked separately, creating processing overhead that is amplified by the requirement to repeatedly increase the bound of the verification. The impact of this problem is clear where hundreds of properties are verified on the same design.

      The second limitation of BMC is that while being especially effective as a falsification tool, it provides only a partial answer to verification. The output of a BMC tool is typically a list of properties that were successfully falsified or verified and a list of properties with an undetermined status. These properties are likely to be true as they were not falsified with a reasonable bound, but the validation method is not strong enough to verify them.

      The conventional BMC algorithm receives several input values, including (see Figure 1 and Figure 2):
•             List of properties to be checked (Props)
•             Maximum depth to check (bound)
•             Integer (step) to increment from one value of the bound to the next

      The BMC attempts verification by dividing the interval [0, bound] into smaller intervals [0, step-1] and [step 2*step-1]. The last interval ends at the bound. For each interval [min, max], the process repeats for all the properties, P, that are not falsified or verified.

      The falsification check for one property is reduced to a SAT problem (see Figure 3). For example, a formula describes a counter, P, such as a path that starts from the initial states (s0, s1, …, smax) and violates P in one of its states. Assume that the program receives a predicate Init(s), characterizing the initial states of the design, and a predicate TR(s,s’), describing the transition rel...