Automatic test pattern generation-based circuit verification method and apparatus

An apparatus comprising:

• at least one memory configured to store instructions;
• and
• at least one processor coupled to at least one memory and configured to execute the instructions to cause the apparatus to:
• select a first logic cone from a fan-out logic cone corresponding to a target line in a circuit, wherein the fan-out logic cone comprises a first gate circuit that extends from the target line to an output end of the circuit;
• identify, based on the first logic cone, a second logic cone in a fan-in logic cone corresponding to the target line, wherein the fan-in logic cone comprises a second gate circuit that extends from an input end of the circuit to the target line, and wherein the second logic cone comprises a third gate circuit that affects a first output value of the first logic cone;
• generate a first conjunctive normal form (CNF) based on the first logic cone and the second logic cone;
• detect the target line using the first CNF to obtain a first detection result, wherein the first detection result indicates a fault type of the target line;
• and
• obtain, when the first logic cone is a partial region in the fan-out logic cone and the first detection result meets a first specified condition corresponding to the first logic cone, a first verification result of the target line based on the first detection result.

A computer program product comprising computer-executable instructions stored on a non-transitory computer readable medium that, when executed by at least one processor, cause an apparatus to:

• select a first logic cone from a fan-out logic cone corresponding to a target line in a circuit, wherein the fan-out logic cone comprises a first gate circuit that extends from the target line to an output end of the circuit;
• identify, based on the first logic cone, a second logic cone in a fan-in logic cone corresponding to the target line, wherein the fan-in logic cone comprises a second gate circuit that extends from an input end of the circuit to the target line, and wherein the second logic cone comprises a third gate circuit that affects a first output value of the first logic cone;
• generate a first conjunctive normal form (CNF) based on the first logic cone and the second logic cone;
• detect the target line using the first CNF to obtain a first detection result, wherein the first detection result indicates a fault type of the target line;
• and
• obtain, when the first logic cone is a partial region in the fan-out logic cone and the first detection result meets a first specified condition corresponding to the first logic cone, a first verification result of the target line based on the first detection result.