| 摘要 |
Disclosed below are representative embodiments of methods, apparatus, and systems for performing formal verification. For example, certain embodiments can be used to formally verify a Booth multiplier. For instance, in one example embodiment, a specification of a Booth multiplier circuit is received; an initial model checking operation is performed for a smaller version of the Booth multiplier circuit; a series of subsequent model checking operations are performed for versions of the Booth multiplier circuit that are incrementally larger than the smaller version of the Booth multiplier circuit, wherein, for each incrementally larger Booth multiplier circuit, two or more model checking operations are performed, the two or more model checking operations representing decomposed proof obligations for showing; and a verification result of the Booth multiplier circuit is output. |
