Device, system and method of generating a hardware-verification test case

1. A method for verifying a hardware design, comprising the steps of:

providing an input specification for a test case that includes a set of constraints;

with a constraint satisfaction problem (CSP) solver generating CSP-generated transactions for the hardware design that satisfy the set of constraints;

with a transaction generator altering at least a portion of the CSP-generated transactions to generate manipulated transactions that exceed the CSP-generated transactions in number;

forming the test case for the hardware design from the manipulated transactions; and

submitting the test case to an execution engine.

2. The method according to claim 1 , wherein the CSP-generated transactions have a pre-condition that must be satisfied prior to an execution thereof in the test case and a post-condition that is satisfied after the execution, and wherein altering comprises classifying at least a portion of the CSP-generated transactions into a first type, wherein the post-condition thereof does not affect the pre-condition of any of the CSP-generated transactions and a second type wherein the execution thereof renders the precondition thereof unsatisfied.

3. The method according to claim 2 , wherein altering further comprises duplicating at least a portion of the CSP-generated transactions that are classified as the first type.

4. The method according to claim 2 , wherein altering comprises reconstructing the precondition of the CSP-generated transactions that are classified as the second type.

5. The method according to claim 1 , wherein altering comprises duplicating at least one of the CSP-generated transactions without mutation thereof.

6. The method according to claim 1 , wherein forming the test case comprises incorporating permutations of a set of the manipulated transactions therein, the permutations comprising at least first and second arrangements of the set of the manipulated transactions.

7. A computer software product for verifying a hardware design, including a computer storage medium in which computer program instructions are stored, the instructions organized into distinct software modules comprising a constraint satisfaction problem (CSP) solver and a transaction generator, which instructions, when executed by a computer, cause the computer to perform the steps of:

accepting an input specification for a test case that includes a set of constraints;

with the CSP solver generating CSP-generated transactions for the hardware design that satisfy the set of constraints;

with the transaction generator altering at least a portion of the CSP-generated transactions to generate manipulated transactions that exceed the CSP-generated transactions in number;

forming the test case for the hardware design from the manipulated transactions; and

submitting the test case to an execution engine.

8. The computer software product according to claim 7 , wherein the CSP-generated transactions having a pre-condition that must be satisfied prior to an execution thereof in the test case and a post-condition that is satisfied after the execution, and wherein altering comprises classifying at least a portion of the CSP-generated transactions into a first type, wherein the post-condition thereof does not affect the pre-condition of any of the CSP-generated transactions and a second type wherein the execution thereof renders the pre-condition thereof unsatisfied.

9. The computer software product according to claim 8 , wherein altering further comprises duplicating at least a portion of the CSP-generated transactions that are classified as the first type.

10. The computer software product according to claim 8 , and wherein altering comprises reconstructing the precondition of the CSP-generated transactions that are classified as the second type.

11. The computer software product according to claim 7 , wherein altering comprises duplicating at least one of the CSP-generated transactions without mutation thereof.

12. The computer software product according to claim 7 , wherein forming the test case comprises incorporating permutations of a set of the manipulated transactions therein, the permutations comprising at least first and second arrangements of the set of the manipulated transactions.

13. A data processing system for verifying a hardware design, comprising:

a processor;

a memory accessible to the processor storing programs and data objects therein, the programs including a constraint satisfaction problem (CSP) solver and a transaction generator, wherein execution of the programs cause the processor to perform the steps of:

accepting an input specification for a test case that includes a set of constraints;

with the CSP solver generating CSP-generated transactions for the hardware design that satisfy the set of constraints;

with the transaction generator altering at least a portion of the CSP-generated transactions to generate manipulated transactions that exceed the CSP-generated transactions in number;

forming the test case for the hardware design from the manipulated transactions; and

submitting the test case to an execution engine.

14. The data processing system according to claim 13 , wherein the CSP-generated transactions having a pre-condition that must be satisfied prior to an execution thereof in the test case and a post-condition that is satisfied after the execution, and wherein altering comprises classifying at least a portion of the CSP-generated transactions into a first type, wherein the post-condition thereof does not affect the pre-condition of any of the CSP-generated transactions and a second type wherein the execution thereof renders the pre-condition thereof unsatisfied.

15. The data processing system according to claim 14 , wherein altering further comprises duplicating at least a portion of the CSP-generated transactions that are classified as the first type.

16. The data processing system according to claim 14 , and wherein altering comprises reconstructing the pre-condition of the CSP-generated transactions that are classified as the second type.

17. The data processing system according to claim 13 , wherein altering comprises duplicating at least one of the CSP-generated transactions without mutation thereof.

18. The data processing system according to claim 13 , wherein forming the test case comprises incorporating permutations of a set of the manipulated transactions therein, the permutations comprising at least first and second arrangements of the set of the manipulated transactions.

19. A method for verifying a hardware design, comprising the steps of:

providing an input specification for a test case that includes a set of constraints;

with a constraint satisfaction problem (CSP) solver generating CSP-generated transactions for the hardware design that satisfy the set of constraints, the CSP-generated transactions having a pre-condition that must be satisfied prior to an execution thereof and a post-condition that is satisfied after the execution;

with a transaction generator duplicating at least respective portions of the CSP-generated transactions without mutation thereof to generate new transactions that exceed the CSP-generated transactions in number;

forming the test case for the hardware design from the new transactions; and

submitting the test case to an execution engine.

20. The method according to claim 19 , wherein the CSP-generated transactions have an initialization, further comprising the steps of:

identifying CSP-generated transactions wherein the execution thereof renders the pre-condition thereof unsatisfied; and

reconstructing the pre-condition of a portion of the identified CSP-generated transactions by duplicating the initialization thereof.