US 7,322,017 B2 | ||
Method for verification using reachability overapproximation | ||
Jason Raymond Baumgartner, Austin, Tex. (US); Hari Mony, Austin, Tex. (US); Viresh Paruthi, Austin, Tex. (US); and Jiazhao Xu, Mount Kisco, N.Y. (US) | ||
Assigned to International Business Machines Corporation, Armonk, N.Y. (US) | ||
Filed on Dec. 14, 2004, as Appl. No. 11/11,245. | ||
Prior Publication US 2006/0129958 A1, Jun. 15, 2006 | ||
Int. Cl. G06F 17/50 (2006.01); G06F 9/45 (2006.01) |
U.S. Cl. 716—5 [716/4; 716/18] | 7 Claims |
1. A method of verifying that a circuit design conforms to a desired property, said method comprising:
receiving a circuit design, a first initial state of said circuit design, and a property for verification with respect to
said circuit design, wherein said first initial state is represented as a binary decision diagram that includes a plurality
of nodes, and wherein said first initial state is further associated with an initial value that defines a value said first
initial state takes at time 0;
expanding said first initial state of said circuit design to create a superset of said first initial state containing one
or more states reachable from said first initial state of said circuit design;
synthesizing said superset to define a second initial state of said circuit design, wherein said second initial state is synthesized
as a netlist by utilizing multiplexor representation over parametric variables to enable various paths through said plurality
of nodes in said binary decision diagram and updating initial value mappings to appropriate synthesized gates represented
in said netlist;
overapproximating application of said superset and said second initial state to said circuit design through cutpoint insertion
into said superset to obtain a modified superset, wherein said cut-point insertion replaces a gate in said netlist with a
random gate; and
verifying said property by comparing said property to said modified superset.
|