System, methods and apparatus for generation of simulation stimulus

• US 8,020,125 B1
• Filed: 09/10/2008
• Issued: 09/13/2011
• Est. Priority Date: 09/10/2008
• Status: Expired due to Fees

• Current Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Original Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Inventors: Kitchen, Nathan, Kuehlmann, Andreas
• Primary Examiner(s): Levin; Naum
• Application Number:
  US12/208,234
• Time in Patent Office: 1,098 Days
• Field of Search: 716/106, 703/14, 706/19
• US Class Current: 716/106
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method and apparatus for producing a verification of digital circuits is provided. In an exemplary embodiment, a set of Boolean and Integer constraints are derived, and a set of Boolean and Integer stimuli are generated that meet the constraints. These stimuli are then used to verify a digital design, and a verification report is generated. In other example embodiments, a computing apparatus and computer software product are provided. The computer software product containing a set of executable instructions that, when executed, configure the computing apparatus to produce a verification report by the provided methods.

Claims

1. A computer-implemented method of producing a verification report of a digital design comprising:

generating a description of a digital design;

generating a set of Boolean constraints and a set of integer constraints describing a valid set of input stimuli for the design description, including;

randomly selecting a Boolean or an Integer sample variable;

randomly changing the state of the selected sample variable; and

determining a change in the number of satisfied clauses in combined set of Boolean and Integer constraints;

generating a mixed Boolean-Integer input stimuli set for the digital design description, the input stimuli satisfying the set of Boolean constraints and the set of integer constraints;

performing, on a computing apparatus, a verification on the design description utilizing the input stimuli; and

producing a verification report from the verification.

2. The method of claim 1, wherein the input stimuli set comprises samples from non-connected solution spaces.

3. The method of claim 1, wherein the changed sample is accepted as part of the input stimuli set if the change in number of satisfied clauses exceeds a threshold and probabilistically rejected if the change does not exceed the threshold.

4. The method of claim 3, wherein the random selection of a sample variable, the random change of state, the determining the number of satisfied clauses and the addition of the change to the stimuli set is iterated until a predetermined number of stimuli are generated.

5. The method of claim 1, wherein if the random sample variable is a Boolean variable the random change is complementing the value of a Boolean sample variable, the method further comprising determining the validity of the random sample as an input stimulus.

6. The method of claim 1, wherein if the random sample variable is an Integer variable the random change comprises determining a probability density function for the variable and randomly selecting a value from the density function, the method further comprising determining the validity of the random sample as an input stimulus.

7. The method of claim 6, wherein the selecting a value follows an algorithm selected from a group consisting of a Metropolis Move, a WalkSat Move and a Davis Putnam Logemann Loveland (DPLL) Move.

8. The method of claim 1, wherein the generation of a mixed Boolean-Integer stimuli set is iteratively performed until a predetermined number of stimuli are generated in the set.

9. A computing apparatus comprising:

a processor;

a memory;

a storage wherein the storage contains a set of processor executable instructions that, when executed by the processor will configure the computing apparatus to;

generate a description of a digital design;

generate a set of Boolean constraints and a set of integer constraints describing a valid set of input stimuli for the design description, including;

randomly select a Boolean or an Integer sample variable;

randomly change the state of the selected sample variable; and

determine a change in the number of satisfied clauses in combined set of Boolean and Integer constraints;

generate a mixed Boolean-Integer input stimuli set for the digital design description, the input stimuli satisfying the set of Boolean constraints and the set of integer constraints;

perform a verification on the design description utilizing the input stimuli; and

produce a verification report from the verification.

10. The computing apparatus of claim 9, wherein the input stimuli set comprises samples from non-connected solution spaces.

11. The computing apparatus of claim 9, wherein the changed sample is accepted as part of the input stimuli set if the change in number of satisfied clauses exceeds a threshold and probabilistically rejected if the change does not exceed the threshold.

12. The computing apparatus of claim 11, wherein the configuration for random selection of a sample variable, the random change of state, the determination of the number of satisfied clauses and the addition of the change to the stimuli set is iterated until a predetermined number of stimuli are generated.

13. The computing apparatus of claim 9, wherein if the random sample variable is a Boolean variable the random change is complementing the value of a Boolean sample variable, the configuration further comprising a configuration to determine the validity of the random sample as an input stimulus.

14. The computing apparatus of claim 9, wherein if the random sample variable is an Integer variable the random change comprises determining a probability density function for the variable and randomly selecting a value from the density function, the configuration further comprising a configuration to determine the validity of the random sample as an input stimulus.

15. The computing apparatus of claim 14, wherein the configuration for selecting a value follows an algorithm selected from a group consisting of a Metropolis Move, a WalkSat Move and a Davis Putnam Logemann Loveland (DPLL) Move.

16. The computing apparatus of claim 9, wherein the generation of a mixed Boolean-Integer stimuli set is iteratively performed until a predetermined number of stimuli are generated in the set.

17. A computer software product comprising:

a non-transitory machine-readable medium, the non-transitory machine-readable medium containing set of processor executable instructions sufficient to configure a computing apparatus to;

generate a description of a digital design;

generate a set of Boolean constraints and a set of integer constraints describing a valid set of input stimuli for the design description, including;

randomly select a Boolean or an Integer sample variable;

randomly change the state of the selected sample variable; and

determine a change in the number of satisfied clauses in combined set of Boolean and Integer constraints;

generate a mixed Boolean-Integer input stimuli set for the digital design description, the input stimuli satisfying the set of Boolean constraints and the set of integer constraints;

perform a verification on the design description utilizing the input stimuli; and

produce a verification report from the verification.

18. The software product of claim 17, wherein the input stimuli set comprises samples from non-connected solution spaces.

19. The software product of claim 17, wherein the changed sample is accepted as part of the input stimuli set if the change in number of satisfied clauses exceeds a threshold and probabilistically rejected if the change does not exceed the threshold.

20. The software product of claim 19, wherein if the random sample variable is a Boolean variable the random change is complementing the value of a Boolean sample variable, the configuration further comprising a configuration to determine the validity of the random sample as an input stimulus.

21. The software product of claim 19, wherein if the random sample variable is an Integer variable the random change comprises determining a probability density function for the variable and randomly selecting a value from the density function, the configuration further comprising a configuration to determine the validity of the random sample as an input stimulus.

22. The software product of claim 21, wherein the selecting a value follows an algorithm selected from a group consisting of a Metropolis Move, a WalkSat Move and a Davis Putnam Logemann Loveland (DPLL) Move.

23. The software product of claim 19, wherein the configuration for the random selection of a sample variable, the random change of state, the determining the number of satisfied clauses and the addition of the change to the stimuli set is iterated until a predetermined number of stimuli are generated.

24. The software product of claim 17, wherein the configuration for generation of a mixed Boolean-Integer stimuli set is iteratively performed until a predetermined number of stimuli are generated in the set.