Jason A Raymond

US Patent:

20060129958, Jun 15, 2006

Filed:

Dec 14, 2004

Appl. No.:

11/011245

Inventors:

Jason Raymond - Austin TX, US
Hari Mony - Austin TX, US
Viresh Paruthi - Austin TX, US
Jiazhao Xu - Mount Kisco NY, US

International Classification:

G06F 17/50
G06F 9/45

US Classification:

716005000

Abstract:

A method, system and computer program product for verifying that a design conforms to a desired property is disclosed. The method comprises receiving a design, a first initial state of the design, and a property for verification with respect to the design. The first initial state of the design is expanded to create a superset of the first initial state containing one or more states reachable from the first initial state of the design. A superset is synthesized to define a second initial state of the design. Application of the superset to the design is overapproximated through cutpoint insertion into the superset to obtain a modified superset, and the property is verified with reference to the modified superset.