Methods, systems, and articles of manufacture for X-behavior verification of an electronic design

A system for verifying X-behavior in an electronic design, comprising:

• one or more modules, at least one of which is stored in part or in whole in memory and comprises at least one processor including one or more processor cores executing one or more threads in a computing system;
• a non-transitory computer accessible storage medium storing thereupon program code that includes a sequence of instructions that, when executed by the at least one processor, causes the at least one processor at least to:
• identify, by the at least one processor, at least a portion of an electronic design, the at least the portion including an input node, an output node, and an internal node located between the input node and the output node;
• a formal verification module that is stored at least partially in memory and includes or functions in tandem with the at least one processor and is configured to generate internal X-propagation verification results for the internal node based in part or in whole upon an internal precondition and an internal harmless condition for the internal node;
• and
• perform, by the at least one processor, X-propagation verification for the output node based in part upon one or more assumed properties that are assumed at the internal node.

An article of manufacture comprising a non-transitory computer accessible storage medium having stored thereupon a sequence of instructions which, when executed by at least one processor or at least one processor core executing one or more threads, causes the at least one processor or the at least one processor core to perform a set of acts for verifying X-behavior in an electronic design, the set of acts comprising:

• identifying, by at least one processor, at least a portion of an electronic design, the at least the portion including an input node, an output node, and an internal node located between the input node and the output node;
• generating, at one or more modules including a formal verification module that is stored at least partially in memory and includes or functions in tandem with the at least one processor, internal X-propagation verification results for the internal node based in part or in whole upon an internal precondition and an internal harmless condition for the internal node;
• and
• performing, by the at least one processor, X-propagation verification for the output node based in part upon one or more assumed properties that are assumed at the internal node.

A computer implemented method for verifying X-behavior in an electronic design, comprising:

• identifying, by at least one processor of a computing system, at least a portion of an electronic design, the at least the portion of the electronic design including a first node;
• determining, at one or more modules including a condition extraction module that is stored at least partially in memory and includes or functions in tandem with the at least one processor, at least one first precondition and at least one first harmless condition for the first node;
• and
• generating, by the at least one processor, one or more first X-behavior properties for the first node at least by combining the at least one first precondition and the at least one first harmless condition.