Automatic verification of dependency
AssigneeFreescale Semiconductor, Inc.
InventorsXiushan Feng, Jayanta Bhadra, Ashish Goel
Life of this patent
Estimating the term…
Abstract
An approach is provided in which a formal verification tool sends a condition signal to a first circuit instance and to a second circuit instance, which are both instances of an electric circuit design. The formal verification tool selects a common input port and sends a first input value to the common input port of the first circuit instance and sends a second input value, which is different than the first input value, to the common input port of the second circuit instance. In turn, the first circuit instance generates a first output value and the second circuit instance generates a second instance value, which are utilized to verify dependencies between the electronic circuit's input ports and output ports.
Claims20
A method comprising:
- sending a common condition signal to a first circuit instance and to a second circuit instance, wherein the first and second circuit instances are instances of a same electronic circuit design that includes one or more input ports and at least one output port;
- selecting a common input port from the one or more input ports;
- sending a first input value to the selected common input port of the first circuit instance, wherein the sending the first input value results in a first output value at the first circuit instance's output port;
- sending a second input value to the selected common input port of the second circuit instance, wherein the second input value is different than the first input value, and wherein the sending the second input value results in a second output value at the second circuit instance's output port;
- and
- verifying, by one or more processors, one or more dependencies between the one or more input ports and the at least one output port based on a comparison of the first output value and the second output value.
An information handling system comprising:
- one or more processors;
- one or more memories accessible by at least one of the processors;
- a formal verification module accessible by at least one of the processors that invokes a common condition signal on a first circuit instance and a second circuit instance, wherein the first and second circuit instances are instances of a same electronic circuit design that includes one or more input ports and at least one output port;
- selection logic included in the formal verification module that selects a common input port from the one or more input ports;
- first input generation logic included in the formal verification module that invokes a first input value on the selected common input port of the first circuit instance, wherein the invoking the first input value results in a first output value at the first circuit instance's output port;
- second input generation logic included in the formal verification module that invokes a second input value on the selected common input port of the second circuit instance, wherein the second input value is different than the first input value, and wherein the invoking the second input value results in a second output value at the second circuit instance's output port;
- and
- a dependency verification module accessible by at least one of the processors that verifies one or more dependencies between the one or more input ports and the at least one output port based on a comparison of the first output value and the second output value.
A computer program product stored in a computer readable storage medium, comprising computer program code that, when executed by an information handling system, causes the information handling system to perform actions comprising:
- sending a common condition signal to a first circuit instance and to a second circuit instance, wherein the first and second circuit instances are instances of a same electronic circuit design that includes one or more input ports and at least one output port;
- selecting a common input port from the one or more input ports;
- sending a first input value to the selected common input port of the first circuit instance, wherein the sending the first input value results in a first output value at the first circuit instance's output port;
- sending a second input value to the selected common input port of the second circuit instance, wherein the second input value is different than the first input value, and wherein the sending the second input value results in a second output value at the second circuit instance's output port;
- and
- verifying one or more dependencies between the one or more input ports and the at least one output port based on a comparison of the first output value and the second output value.
Dependencies are inferred from the claim text.