Patent ID: 8341567
Filing Date: 2012-12-25
Classification: G06F

Abstract:
1. A method to formally verify a property of a circuit design comprising: receiving a description of at least a portion of the circuit that identifies one or more devices that each includes at least one terminal and that identifies at least one connection between terminals of one or more of the identified devices; receiving a description of a relationship between current values and voltage values represented as a curve (I-V curve relationship) for one or more of the identified devices; converting each respective I-V curve relationship to multiple respective conservative approximations, each representing a respective portion of such respective I-V curve relationship as an interval that includes a range of one of current values or voltage values that implies an interval that includes a range of the other of current values or voltage values and that encompasses the respective portion of the respective I-V curve relationship; assigning voltage labels to one or more terminals of one or more identified devices that indicate voltage relationships among the one or more terminals consistent with KVL; defining a respective current relationship, among one or more respective sets of currents of the one or more of the identified devices that have one or more terminals that the circuit description indicates to have a connection between them, that is consistent with KCL; and using a computer to search a search space defined by the respective conservative approximations for a region of the search space that is bounded by a range of current and a range of voltage values that intersects with a respective conservative approximation of a respective portion of each respective I-V curve relationship and that is consistent with the voltage labels and that is consistent with each respective defined current relationship.