Non-assignable signal support during formal verification of circuit designs

Abstract

A method for supporting non-assignable signals during formal verification of a circuit design includes providing a propagation logic for non-assignable signals and identifying a relevant cone in a circuit design, where the relevant cone determined by a property to verify. The method also includes designating one or more signals in the circuit design as non-assignable signals and propagating within the relevant cone any of the designated one or more non-assignable signals using the propagation logic for non-assignable signals. The method further includes ensuring, if a counter-example disproving the property exists, that the counter-example does not comprise any of the one or more designated non-assignable signals. A formal verification system that supports the designation of non-assignable signals comprises a non-assignable signal truth table and a proof engine. The non-assignable signal truth table specifies a propagation logic for non-assignable signals. The proof engine is coupled to the non-assignable truth table, and is operable to determine a property to verify in a circuit. The proof engine is also operable to identify a relevant cone in the design circuit based on the property, where the relevant cone comprises a plurality of signals. The proof engine is further operable to designate one or more signals as non-assignable and propagate the non-assignable signals using the propagation logic from the non-assignable signal truth table, and ignore the non-assignable signals in generating any counter-example.