Method, System, and Program Product for Automated Verification of Gating Logic Using Formal Verification

• US 20080059925A1
• Filed: 08/29/2006
• Published: 03/06/2008
• Est. Priority Date: 08/29/2006
• Status: Active Grant

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Van Huben, Gary A., Seigler, Adrian E.
• Granted Patent: US 7,448,008 B2
• Time in Patent Office: Days
• US Class Current: 716/5
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

As described herein the automated verification methodology parsing scripts auto generate test bench hardware design langaue, such as VHDL or Verilog, from the design source VHDL or Verilog. A formal verification model is then built comprising the testbench VHDL and the design under test. The resulting design verification tool then provides proofs and counterexamples for all of the rules, e.g., auto-generated rules, in the test bench.

Claims

1. A method of verifying gating rules comprising the steps of generating test bench hardware design language code from the design source hardware design language code, and building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool.

2. The method of claim 1 comprising providing proofs and counterexamples for auto-generated rules in the test bench.

3. A method of verifying gating rules comprising the steps of generating test bench hardware design language code from the design source hardware design language code, and building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the method of:

(1) generating test bench hardware design language code from the design source hardware design language code by;

a. identifying interface signals requiring gating verification, including denoting registers and/or latches that are asserted to remain stable from the design source;

b. identify each component to be independently verified using the design source and an assertion that registers and latches within a component will remain stable during gating,

c. extracting a list of registers and latches from each component;

d. generating a test bench, said test bench driving formal verification step utilizing the list of interfaces and registers as an input to produce the test bench, said test bench having automated rules to verify assertions regarding latch stability;

e. compiling the test bench to form a verification model; and

(2). building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the steps of;

f. executing a formal verification process to determine that all latches and registers asserted to remain stable under a gating condition are stable;

including attempting to produce a counter example illustrating how a particular latch can change state while its associated fence signal is being applied; and

g. if counter examples exist, repetitively updating the design source to fix the error until the design source completes the formal verification step without any counter examples, else characterizing that the verification is complete and all identified interfaces are concluded to be properly gated.

4. The method of claim 3 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.

5. The method of claim 3 comprising extracting the list of registers and latches from each component by exploiting the register keyword in a signal declaration portion of the VHDL source.

6. The method of claim 3 comprising generating the test bench by a method comprising 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 the 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.

7. The method of claim 3 wherein wherein gating is chosen from the group consisting of fencing, clock gating, and power gating.

8. The method of claim 3 comprising tracking a bill of materials for a model as the model is validated.

9. A system for testing a multi-domain microelectronic circuit having built in self testing circuitry, said system building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the steps of generating test bench hardware design language code from the design source hardware design language code, and building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool.

10. The system of claim 9 adapted for providing proofs and counterexamples for auto-generated rules in the test bench.

11. A system for testing a multi-domain microelectronic circuit, said circuit having built in self testing circuitry, said system adapted to generate test bench hardware design language code from the design source hardware design language code, and build a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the method of:

(1) generating test bench hardware design language code from the design source hardware design language code by;

a. identifying interface signals requiring gating verification, including denoting registers and/or latches that are asserted to remain stable from the design source;

b. 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,

c. extracting a list of registers and latches from each component;

d. generating a test bench, said test bench driving formal verification step utilizing the list of interfaces and registers as an input to produce the test bench, said test bench having automated rules to verify assertions regarding latch stability;

e. compiling the test bench to form a verification model; and

(2) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the steps of;

f. executing a formal verification process to determine that all latches and registers asserted to remain stable under a gating condition are stable;

including attempting to produce a counter example illustrating how a particular latch can change state while its associated fence signal is being applied; and

g. if counter examples exist, repetitively updating the design source to fix the error until the design source completes the formal verification step without any counter examples, else characterizing that the verification is complete and all identified interfaces are concluded to be properly gated.

12. The system of claim 11 adapted 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.

13. The system of claim 11 adapted to extract the list of registers and latches from each component by exploiting the register keyword in a signal declaration portion of the VHDL source.

14. The system of claim 11 adapted to generate the test bench by a method comprising 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 the 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.

15. The system of claim 11 wherein wherein gating is chosen from the group consisting of fencing, clock gating, and power gating.

16. The system of claim 11 adapted to track a bill of materials for a model as the model is validated.

17. A program product comprising a substrate having computer readable code thereon, said adapted to control and configure a system to testing a multi-domain microelectronic circuit having built in self testing circuitry, said system building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the steps of generating test bench hardware design language code from the design source hardware design language code, and building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool.

18. The program product of claim 17 adapted for configuring and controlling a system to provide proofs and counterexamples for auto-generated rules in the test bench.

19. A program product adapted for configuring and controlling a system for testing a multi-domain microelectronic circuit, said circuit having built in self testing circuitry, said system adapted to generate test bench hardware design language code from the design source hardware design language code, and build a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the method of:

(1) generating test bench hardware design language code from the design source hardware design language code by;

a. identifing interface signals requiring gating verification, including denoting registers and/or latches that are asserted to remain stable from the design source;

b. 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,

c. extracting a list of registers and latches from each component;

d. generating a test bench, said test bench driving formal verification step utilizing the list of interfaces and registers as an input to produce the test bench, said test bench having automated rules to verify assertions regarding latch stability;

e. compiling the test bench to form a verification model; and

(2) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test to provide a design verification tool by the steps of;

f. executing a formal verification process to determine that all latches and registers asserted to remain stable under a gating condition are stable, including attempting to produce a counter example illustrating how a particular latch can change state while its associated fence signal is being applied; and

g. if counter examples exist, repetitively updating the design source to fix the error until the design source completes the formal verification step without any counter examples, else characterizing that the verification is complete and all identified interfaces are concluded to be properly gated.

20. The program product of claim 19 adapted to extract the list of registers and latches from each component by exploiting the register keyword in a signal declaration portion of the VHDL source.

21. The program product of claim 19 adapted to generate the test bench by a method comprising 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 the 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.

22. The program product of claim 19 wherein gating is chosen from the group consisting of fencing, clock gating, and power gating.

23. The program product of claim 19 adapted to track a bill of materials for a model as the model is validated.