Method, system, and program product for automated verification of gating logic using formal verification

• US 7,971,166 B2
• Filed: 06/15/2008
• Issued: 06/28/2011
• Est. Priority Date: 08/29/2006
• Status: Expired due to Fees

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Van Huben, Gary A., Seigler, Adrian E.
• Primary Examiner(s): Kik; Phallaka
• Application Number:
  US12/139,483
• Publication Number:
  US 20090183129A1
• Time in Patent Office: 1,108 Days
• Field of Search: 716/21, 716/8, 716/5, 700/120, 430/5, 378/35, 703/16
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

Gating rules for a device design containing microelectronic devices are tested using formal verification. Testbench design code is generated for a device design from a design source containing hardware design language code. A formal verification process on the testbench device code determines whether the devices within the device design will be stable or unstable under a gating condition. If the test shows a design is unstable under the gating condition; it is indicated that a hardware design fix for the device design is required. If not, the test ends.

Claims

1. A method performed by a computer of testing to verify gating rules for a device design containing microelectronic circuits, latches and/or registers by employing a formal verification process, said method comprising:

generating testbench design code for a device design from a design source containing hardware design language code;

performing, by said computer, a formal verification process on the testbench device code to determine whether the microelectronic circuits, latches, and/or registers within the device design will be stable or unstable under a gating condition;

then indicating that a hardware design fix for the device design is required if the formal verification process shows that the device design is unstable under the gating condition;

or

then ending the test with respect to said device design if the formal verification process shows that the device design is stable under the gating condition.

2. The method of claim 1, further comprising providing proofs and counterexamples for auto-generated rules in a testbench.

3. The method of claim 1, further comprising identifying each component to be independently verified using the design source and an overall assertion that all registers and latches within a component will remain stable during gating.

4. The method of claim 1 further comprising extracting a list of interfaces, registers and latches from each component by exploiting a register keyword in a signal declaration portion of a VHDL source.

5. The method of claim 1 wherein generating the testbench design code comprises:

a. enumerating inputs and outputs into an entity declaration section;

b. creating a unique fail event for each identified latch and declaring fail events in a fail section;

c. creating an assignment statement to drive each identified gating signal to a constant active state;

d. creating an assignment statement to drive each identified ungated input to a constant inactive state; and

e. creating a rule for each identified latch wherein the fail event will positively trigger if a latch facility deviates from a corresponding identified setting signal.

6. The method of claim 1 wherein the gating condition is chosen from the group consisting of fencing, clock gating, and power gating;

and the method further comprising tracking a bill of materials for a model as the model is validated.

7. The method of claim 1 including a series of steps as follows:

further identifying interface signals, registers and/or latches from a design source;

automatically generating a testbench;

compiling said testbench;

executing a formal verification step;

determining whether counter examples were produced by said formal verification step;

if counter examples were produced, fixing said verification step and updating said design source; and

if counter examples were not produced, then ending said series of steps.

8. The method of claim 1 further comprising the steps of:

automatically generating a testbench that generates testbench files;

supplying said testbench files for compiling said testbench;

generating a bill of materials listing after performing said formal verification process and compiling said testbench; and

comparing said bill of materials with updates from a Data Design Manager (DDM).

9. A system for testing a multi-domain microelectronic circuit to verify gating rules for a device design containing microelectronic circuits, latches, and/or registers by employing a formal verification process, said system comprising:

means for generating testbench design code for a device design from a design source containing hardware design language code;

means for performing a formal verification process on the testbench design code to determine whether latches and/or registers within a device design will be stable or unstable under a gating condition;

means for indicating that a hardware design fix for the device design is required if the formal verification process shows that the device design is unstable under the gating condition;

or

means for ending the test with respect to said device design if the formal verification process shows that the device design is stable under the gating condition.

10. The system of claim 9 further including a series of means for:

identifying interface signals, registers and/or latches from a design source;

automatically generating a testbench;

compiling said testbench;

executing a formal verification step;

determining whether counter examples were produced by said formal verification step;

if said formal verification step produced counter examples, then, fixing said verification step and updating said design source; and

if said formal verification step did not produce counter examples, then ending said series of identifying, automatically generating, compiling, executing, fixing and updating.

11. The system of claim 10, further comprising means to identify each component to be independently verified using the design source and an overall assertion that all registers and latches within a component will remain stable during gating.

12. The system of claim 10, further comprising means for extracting a list of interfaces, registers and latches from each component by exploiting a register keyword in a signal declaration portion of a VHDL source.

13. The system of claim 10, wherein means for automatically generating the testbench further comprises means for:

a. enumerating inputs and outputs into an entity declaration section;

b. creating a unique fail event for each identified latch and declaring fail events in a fails section;

c. creating an assignment statement to drive each identified gating signal to a constant active state;

d. creating an assignment statement to drive each identified ungated input to a constant inactive state; and

e. creating a rule for each identified latch wherein the fail event will positively trigger if the latch facility deviates from its corresponding identified setting signal.

14. The system of claim 10 wherein the gating condition is chosen from the group consisting of fencing, clock gating, and power gating, and said system further comprising means for tracking a bill of materials for a model as the model is validated.

15. The system of claim 10 further comprising means for tracking a bill of materials for a model as the model is validated.

16. The system of claim 9 further including means for:

automatically generates testbench files;

supplying said testbench files for compiling said testbench;

generating a bill of materials listing after said formal verification process and compiling said testbench; and

comparing said bill of materials with updates from a Data Design Manager (DDM).

17. A computer program product comprising a non-transitory computer useable storage medium including a computer readable program, the computer readable program when executed on a computer causes the computer to implement a method of testing to verify gating rules for a device design containing microelectronic circuits, latches and/or registers by employing a formal verification process, said method comprising the steps of:

generating testbench design code for a device design from a design source containing hardware design language code;

performing a formal verification process on the testbench device code to determine whether the microelectronic circuits, latches and/or registers within the device design will be stable or unstable under a gating condition;

then indicating that a hardware design fix for the device design is required if the formal verification process shows that the device design is unstable under the gating condition;

or

then ending the test with respect to said device design if the formal verification process shows that the device design is stable under the gating condition.

18. The program product of claim 17, said method further including a series of steps as follows:

identifying interface signals, registers and/or latches from a design source;

automatically generating a testbench;

compiling said testbench;

executing a formal verification step;

determining whether counter examples were produced by said formal verification step;

if counter examples were produced, then fixing said verification step and updating said design source; and

if no counter examples were produced, then ending said series of steps.

19. The program product of claim 18, said method further comprising providing proofs and counterexamples for auto-generated rules in the testbench.

20. The program product of claim 18 said method further comprising a step for extracting a list of interfaces, registers and latches from each component by exploiting a register keyword in a signal declaration portion of a VHDL source.

21. The program product of claim 18, wherein said step for automatically generating a testbench further comprises the steps of:

a. enumerating inputs and outputs into an entity declaration section,

b. creating a unique fail event for each identified latch and declaring these fail events in a fails section;

c. creating an assignment statement to drive each identified gating signal to a constant active state;

d. creating an assignment statement to drive each identified ungated input to a constant inactive state; and

e. creating a rule for each identified latch wherein the fail event will positively trigger if a latch facility deviates from its corresponding identified setting signal.

22. The program product of claim 18 wherein:

the gating condition is chosen from the group consisting of fencing, clock gating, and power gating; and

said method further comprising a step of tracking a bill of materials for a model as the model is validated.

23. The program product of claim 18 wherein said method further comprises:

automatically generating a testbench which generates testbench files;

supplying said testbench files for compiling said testbench;

generating a bill of materials listing after said formal verification step and compiling said testbench; and

comparing said bill of materials with updates from a Data Design Manager (DDM).