Assuring chip reliability with automatic generation of drivers and assertions

Patent metadata

Field	Value
Publication number	US-9600616-B1
Application number	US-201615264336-A
Country	US
Kind code	B1
Filing date	Sep 13, 2016
Priority date	Nov 27, 2015
Publication date	Mar 21, 2017
Grant date	Mar 21, 2017

Abstract

A computer-implemented method may include retrieving a design netlist with a processor, identifying, via the processor, a logic structure in the design netlist, generating, via the processor, a driver based on the logic structure, applying, via the processor, a simulation and a formal model based on the driver, and testing, via the processor, an output of the simulation and the formal model.

First claim

What is claimed is:

1. A computer-implemented method for assuring a reliability of a chip comprising:
verifying a parity with a processor;
traversing, via the processor, a netlist back from a plurality of netlist outputs;
identifying, via the processor, one or more parity protected structures and one or more gates,
wherein protected parity structures comprises a duplication protection; and
generating, via the processor, a driver based on a logic structure and an assertion indicative of a parity validity.

2. The computer-implemented method of claim 1 further comprising:
applying, via the processor, a simulation and a formal model based on the driver; and
testing, via the processor, an output of the simulation and the formal model.

3. The computer-implemented method of claim 2 wherein generating the simulation and the formal model based on the driver further comprises:
generating one of a model for formal.

4. The computer-implemented method of claim 3 , further comprising generating an assertion for formal.

5. The computer-implemented method of claim 4 , wherein either the model for formal and the assertion for simulation indicates a correctness status between two different sub-units of the chip.

6. The computer-implemented method of claim 1 , wherein identifying the one or more parity protected structures comprises:
retrieving a design netlist with a processor;
statistically analyzing the design netlist;
extracting checking logic information from the design netlist; and
extracting gating information from the design netlist by identifying a plurality of protected structures and a plurality of gating structures; and
identifying the logic structure in the design netlist based on a statistical analysis of the design netlist, the logic information, and gating information.

7. The computer-implemented method of claim 1 wherein generating the driver based on the logic structure comprises:
verifying a parity;
traversing a netlist back from a plurality of netlist outputs;
identifying one or more parity protected structures and one or more gates, wherein protected parity structures may comprise one or more of a duplication protection and a onehot protection; and
generating an assertion indicative of a parity validity.

8. A system for assuring a reliability of a chip comprising:
a processor configured to:
verify a parity;
traverse a design netlist back from a plurality of netlist outputs;
identify one or more parity protected structures and one or more gates,
wherein protected parity structures comprises a duplication protection; and
generate a driver based on a logic structure and an assertion indicative of a parity validity.

9. The system of claim 8 , wherein the processor is further configured to:
apply a simulation and a formal model based on the driver; and
testing an output of the simulation and the formal model.

10. The system of claim 8 wherein the processor is further configured to:
retrieve the design netlist;
statistically analyze the design netlist;
extract checking logic information from the design netlist;
extract gating information from the design netlist; and
identify a logic structure in the design netlist based on a statistical analysis of the design netlist, the logic information, and gating information.

11. The system of claim 8 wherein the processor is further configured to:
verify a validity of a parity;
traverse a netlist back from a plurality of netlist outputs;
identify one or more parity protected structures and one or more gates, wherein protected parity structures may comprise one or more of a duplication protection and a onehot protection; and
generate an assertion indicative of a parity validity; and
generate the driver based on the assertion.

12. The system of claim 8 wherein the processor is further configured to:
generate one of a model for formal.

13. The system of claim 12 , further comprising generating an assertion for formal.

14. The system of claim 13 , wherein either the model for formal and the assertion for simulation indicates a correctness status between two different sub-units of the chip.

15. A non-transitory computer-readable storage medium storing instructions that, when executed by a computer, cause the computer to perform a method for assuring a reliability of a chip, the method comprising:
verifying a parity with a processor;
traversing, via the processor, a netlist back from a plurality of netlist outputs;
identifying, via the processor, one or more parity protected structures and one or more gates,
wherein protected parity structures comprises a duplication protection; and

generating, via the processor, a driver based on a logic structure and an assertion indicative of a parity validity.

16. The non-transitory computer-readable storage medium of claim 15 further comprising:
applying, via the processor, a simulation and a formal model based on the driver; and
testing, via the processor, an output of the simulation and the formal model.

17. The non-transitory computer-readable storage medium of claim 16 , wherein generating the simulation and the formal model based on the driver further comprises:
generating one of a model for formal and an assertion for simulation, wherein either the model for formal and the an assertion for simulation indicates a correctness status between two different sub-units of the chip.

18. The non-transitory computer-readable storage medium of claim 17 , further comprising generating an assertion for formal.

19. The non-transitory computer-readable storage medium of claim 15 , wherein identifying the one or more parity protected structures comprises:
retrieving a design netlist with a processor;
statistically analyzing the design netlist;
extracting checking logic information from the design netlist; and
extracting gating information from the design netlist by identifying a plurality of protected structures and a plurality of gating structures; and
identifying the logic structure in the design netlist based on a statistical analysis of the design netlist, the logic information, and gating information.

20. The non-transitory computer-readable storage medium of claim 15 , wherein generating the driver based on the logic structure comprises:
verifying a validity of a parity;
traversing a netlist back from a plurality of netlist outputs;
identifying one or more parity protected structures and one or more gates, wherein protected parity structures may comprise one or more of a duplication protection and a onehot protection; and
generating an assertion indicative of a parity validity.

Assignees

• IBM

Inventors

• Arbel Eli
• Barak Erez
• Hoppe Bodo
• Krautz Udo
• Moran Shiri

Classifications

• G06F30/327

  Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist · CPC title

• G06F30/33

  Design verification, e.g. functional simulation or model checking · CPC title

• G06F30/367

  Design verification, e.g. using simulation, simulation program with integrated circuit emphasis [SPICE], direct methods or relaxation methods · CPC title

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title

• G06F17/504 Primary

  Physics · mapped topic