Boolean satisfiability based verification of analog circuits

摘要

A method is provided to formally verify a property of a circuit design comprising: receiving a description of at least a portion of the circuit; receiving an indication of search accuracy criteria; receiving a description of a relationship between current and voltage (I-V relationship) for one or more of devices of the circuit; converting each I-V relationship to a conservative approximation of such I-V 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 is consistent with KCL; searching for one or more combinations of current and voltage values that are within at least one region of each conservative approximation and that are consistent with the voltage labels and that are consistent with each respective defined current relationship; converting each region determined to have a searched for combination of current and voltage values to multiple respective smaller regions; and repeating the acts of searching and converting until regions are obtained that meet the received search accuracy criteria.