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

• US 7,448,008 B2
• Filed: 08/29/2006
• Issued: 11/04/2008
• 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:
  US11/468,078
• Publication Number:
  US 20080059925A1
• Time in Patent Office: 798 Days
• Field of Search: 716/6, 703/16
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

Automated verification methodology parsing scripts auto generate testbench hardware design language, 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 testbench.

Claims

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

(I) generating the testbench hardware design language code from the design source hardware design language code by the steps as follows;

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

b. identifying 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 interfaces, registers, and latches from each component;

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

e. compiling the testbench to form a verification model; and

(II) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test for provision thereof to a design verification tool, by the steps as follows;

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 an error until the design source completes the formal verification process without any counter examples, else characterizing that the verification process is complete and all identified interfaces are concluded to be properly gated.

2. The method of claim 1, said step I 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.

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

4. The method of claim 1 comprising generating the testbench by a method comprising the steps as follows:

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.

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

6. The method of claim 1 further comprising tracking a bill of materials for a model as the model is validated.

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

(I) generating testbench hardware design language code from the design source hardware design language code by the steps as follows;

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

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

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

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

e. compiling the testbench to form a verification model; and

(II) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test for provision thereof to a design verification tool by the steps as follows;

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 an error until the design source completes the formal verification process without any counterexamples, else characterizing that the verification is complete and all identified interfaces are concluded to be properly gated.

8. The system of claim 7 further 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.

9. The system of claim 7 further adapted to extract the list of interfaces, registers and latches from each component by exploiting the register keyword in a signal declaration portion of the VHDL source.

10. The system of claim 7 further adapted to generate the testbench by a method comprising the steps as follows:

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.

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

12. The system of claim 7 further adapted to track a bill of materials for a model as the model is validated.

13. A program product comprising:

a computer program storage device for storing a computer program which when executed by a processor causes the processor to configure and control a system for testing a multi-domain microelectronic circuit with said circuit having built-in self testing circuitry,

said system being adapted to generate a testbench hardware design language code from a design source hardware design language code, and to build a formal verification model comprising the testbench hardware design language code and the hardware design language for a design under test for provision thereof to provide to a design verification tool by the method of as follows;

(I) generating testbench hardware design language code from a 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 a design source;

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

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

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

e. compiling the testbench to form a verification model; and

(II) building a formal verification model comprising the testbench hardware design language code and the hardware design language for the design under test for provision thereof to a design verification tool by the steps as follows;

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 an error until the design source completes the formal verification process without any counter examples, else characterizing that the verification process is complete and all identified interfaces are concluded to be properly gated.

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

15. The program product of claim 13 further adapted to generate the testbench by a method comprising the steps of as follows:

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.

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

17. The program product of claim 13 further adapted to track a bill of materials for a model as the model is validated.