Veryifing low power functionality through RTL transformation

• US 8,954,904 B1
• Filed: 04/30/2013
• Issued: 02/10/2015
• Est. Priority Date: 04/30/2013
• Status: Active Grant

• Current Assignee: Jasper Design Automation, Inc. (Cadence Group)
• Original Assignee: Jasper Design Automation, Inc. (Cadence Group)
• Inventors: Loh, Lawrence, Jobstmann, Barbara, Caldeira, Antonio Celso Jr., Mazzawi, Jamil R.
• Primary Examiner(s): Chiang, Jack
• Assistant Examiner(s): Alam, Mohammed
• Application Number:
  US13/874,388
• Time in Patent Office: 651 Days
• Field of Search: 716/103
• US Class Current: 716/103
• CPC Class Codes: G06F 2119/06 Power analysis or power optimisation
• CPC Class Codes: G06F 2119/16 Equivalence checking
• CPC Class Codes: G06F 30/327 Logic synthesis; Behaviour synthesis, e.g. mapping logic, HDL to netlist, high-level language to RTL or netlist
• CPC Class Codes: G06F 30/33 Design verification, e.g. functional simulation or model checking
• CPC Class Codes: G06F 30/3308 using simulation
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A register transfer level (RTL) design is received which models a digital circuit in terms of the flow of digital signals. A power intent description is received which may include a description of power domains, identification of retention flops for each power domain, a list of isolation signals, and power switch definitions. A transformed RTL is produced accounting for functionality described in the power intent description. The transformed RTL includes flops designated as retention flops and non-retention flops. A retention flop module analyzes the flops to ensure that flops are properly designated as retention or non-retention flops. A verification module performs power aware sequential equivalence checking on various RTL and power intent descriptions to verify that RTL and power intent description outputs behave the same when accounting for power states.

Claims

1. A computer-implemented method for power aware sequential equivalence checking, the method comprising:

receiving a first register transfer level (RTL) circuit model of a circuit design;

receiving a first power intent description of the circuit design;

generating a second RTL circuit model by modifying the first RTL circuit model based on the first power intent description;

receiving a third RTL circuit model of the circuit design;

receiving a second power intent description of the circuit design;

generating a fourth RTL circuit model by modifying the third RTL circuit model based on the second power intent description; and

performing, by a computer, power aware sequential equivalence checking on the second RTL circuit model and fourth RTL circuit model by verifying that a set of outputs of the second RTL circuit model and fourth RTL circuit model behave the same during a power on state of one or more power domains corresponding to the outputs while excluding behavior of the outputs during a power off state of the one or more power domains corresponding to the outputs.

2. The method of claim 1, wherein the first RTL circuit model and the third RTL circuit model are the same.

3. The method of claim 2, wherein performing power aware sequential equivalence checking further comprises verifying that the first power intent description and the second power intent description have the same functional effect when considering the state of the power domains corresponding to the set of outputs.

4. The method of claim 1, wherein the first power intent description and the second power intent description are the same.

5. The method of claim 4, wherein performing power aware sequential equivalence checking further comprises verifying that the second RTL circuit model and the fourth RTL circuit model have the same functional effect when considering the state of power domains corresponding to the set of outputs.

6. The method of claim 1, wherein performing power aware sequential equivalence checking further comprises verifying that the third RTL circuit model behaves the same as the first RTL circuit model based on the power aware sequential equivalence checking of the second circuit model and the fourth circuit model.

7. The method of claim 1, wherein the set of outputs are designated by a user.

8. The method of claim 1, wherein the third RTL circuit model is an optimized version of the first RTL circuit model.

9. The method of claim 8, wherein the first RTL circuit model is optimized by performing unknown binary number propagation analysis.

10. The method of claim 8, wherein the first RTL circuit model is optimized by introducing a power delay and converting a set of flops from retention flops to non-retention flops.

11. A non-transitory computer-readable storage medium containing computer program code for power aware sequential equivalence checking, the code comprising code for:

receiving a first register transfer level (RTL) circuit model of a circuit design;

receiving a first power intent description of the circuit design;

generating a second RTL circuit model by modifying the first RTL circuit model based on the first power intent description;

receiving a third RTL circuit model of the circuit design;

receiving a second power intent description of the circuit design;

generating a fourth RTL circuit model by modifying the third RTL circuit model based on the second power intent description; and

performing power aware sequential equivalence checking on the second RTL circuit model and fourth RTL circuit model by verifying that a set of outputs of the second RTL circuit model and fourth RTL circuit model behave the same during a power on state of one or more power domains corresponding to the outputs while excluding behavior of the outputs during a power off state of the one or more power domains corresponding to the outputs.

12. The computer-readable storage medium of claim 11, wherein the first RTL circuit model and the third RTL circuit model are the same.

13. The computer-readable storage medium of claim 12, wherein performing power aware sequential equivalence checking further comprises verifying that the first power intent description and the second power intent description have the same functional effect when considering the state of the power domains corresponding to the set of outputs.

14. The computer-readable storage medium of claim 11, wherein the first power intent description and the second power intent description are the same.

15. The computer-readable storage medium of claim 14, wherein performing power aware sequential equivalence checking further comprises verifying that the second RTL circuit model and the fourth RTL circuit model have the same functional effect when considering the state of power domains corresponding to the set of outputs.

16. The computer-readable storage medium of claim 11, wherein performing power aware sequential equivalence checking further comprises verifying that the third RTL circuit model behaves the same as the first RTL circuit model based on the power aware sequential equivalence checking of the second circuit model and the fourth circuit model.

17. The computer-readable storage medium of claim 11, wherein the set of outputs are designated by a user.

18. The computer-readable storage medium of claim 11, wherein the third RTL circuit model is an optimized version of the first RTL circuit model.

19. The computer-readable storage medium of claim 18, wherein the first RTL circuit model is optimized by performing unknown binary number propagation analysis.

20. The computer-readable storage medium of claim 18, wherein the first RTL circuit model is optimized by introducing a power delay and converting a set of flops from retention flops to non-retention flops.