Equivalence checking method, equivalence checking program, and equivalence checking device

1. A method of checking the equivalence of a high-level description taken as a behavioral description, and a hardware description obtained based on the high-level description, using a computer, said equivalence checking method comprising the steps of:

causing the computer to generate information about correlations between flip-flops with a feedback loop in the hardware description and variables associated therewith with a backward data dependence in a high-level description; and

causing the computer to check the equivalence using the correlation information related to the backward data dependence.

2. The equivalence checking method according to claim 1 , wherein when the equivalence is checked by an inductive method, the computer extracts a reset cycle number corresponding to the minimum number of stages of flip-flops necessary to carry values to the flip-flops in the feedback loop, and uses a symbolic simulation result about the extracted reset cycle number in checking of the equivalence as an initial state of the feedback loop.

3. The equivalence checking method according to claim 2 , wherein the computer generates as the correlation information related to the backward data dependence, first correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

4. The equivalence checking method according to claim 3 , wherein the computer generates as the correlation information related to the backward data dependence, second correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

5. The equivalence checking method according to claim 4 , further including the step of causing the computer to generate information indicative of a correspondence relation between flip-flops without a feedback loop in the hardware description and variables associated therewith with only a forward data dependence in a high-level description,

wherein the computer performs equivalence checking using the correlation information related to the forward data dependence along with the correlation information related to the backward data dependence.

6. The equivalence checking method according to claim 5 , wherein the computer generates as the correlation information related to the forward data dependence, third correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

7. The equivalence checking method according to claim 6 , wherein the computer generates as the correlation information related to the forward data dependence, fourth correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

8. The equivalence checking method according to claim 7 , wherein the computer checks equivalence while performing an addition and a modification on the reset cycle number, the first correlation information related to the backward data dependence, the second correlation information related to the backward data dependence, the third correlation information related to the forward data dependence and the fourth correlation information related to the forward data dependence, assign, as priorities related to the addition and the modification, a first priority to the reset cycle number, a second priority to the first correlation information related to the backward data dependence, a third priority to the second correlation information related to the backward data dependence, a fourth priority to the third correlation information related to the forward data dependence, and a fifth priority to the fourth correlation information related to the forward data dependence, respectively, and performs the addition and modification in accordance with the priorities when a process for the equivalence checking is not completed within a predetermined time constraint.

9. A non-transitory computer readable medium storing an executable equivalence checking program for causing a computer to check the equivalence of a high-level description taken as a behavioral description, and a hardware description obtained based on the high-level description, said equivalence checking program causing the computer to execute a step for generating as support information for equivalence checking, correlation information related to a backward data dependence between flip-flops with a feedback loop in the hardware description and variables associated therewith in a high-level description, and a step for performing checking for the equivalence using the correlation information related to the backward data dependence.

10. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 9 , wherein the computer is caused in the generation step to extract a reset cycle number corresponding to the minimum number of stages of flip-flops necessary to carry values to the flip-flops in the feedback loop, and

in the checking step the computer is caused to check equivalence by an inductive method, using a symbolic simulation result about the extracted reset cycle number in an initial state of the feedback loop.

11. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 10 , wherein the computer in the generation step is caused to generate as the correlation information related to the backward data dependence, first correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

12. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 11 , wherein the computer in the generation step is caused to generate as the correlation information related to the backward data dependence, second correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

13. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 12 ,

wherein in the generation step the computer is further caused to generate as support information for equivalence checking, correlation information related to a forward data dependence indicative of a correspondence relation between flip-flops without a feedback loop in the hardware description and variables associated therewith in a high-level description, and

wherein in the checking step the computer is caused to check equivalence using the correlation information related to the forward data dependence along with the correlation information related to the backward data dependence.

14. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 13 , wherein in the generation step, the computer is caused to generate as the correlation information related to the forward data dependence, third correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

15. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 14 , wherein in the generation step, the computer is caused to generate as the correlation information related to the forward data dependence, fourth correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

16. The non-transitory computer readable medium storing the executable equivalence checking program according to claim 15 , wherein in the generation step, the computer is caused to execute a necessary addition and modification on the reset cycle number, the first correlation information related to the backward data dependence, the second correlation information related to the backward data dependence, the third correlation information related to the forward data dependence and the fourth correlation information related to the forward data dependence in accordance with priorities, and

wherein in the checking step the computer is caused to check equivalence by reflection of the support information for the equivalence checking subjected to the necessary addition and modification thereon, assign, as priorities related to the addition and modification, a first priority to the reset cycle number, a second priority to the first correlation information related to the backward data dependence, a third priority to the second correlation information related to the backward data dependence, a fourth priority to the third correlation information related to the forward data dependence, and a fifth priority to the fourth correlation information related to the forward data dependence, respectively, and perform the addition and modification in accordance with the priorities when a process for the equivalence checking is not completed within a predetermined time constraint.

17. An equivalence checking device which checks by a program process, the equivalence of a high-level description taken as a behavioral description, and a hardware description obtained based on the high-level description, said equivalence checking device comprising:

a generation unit which generates by the program process, as support information for equivalence checking, correlation information related to a backward data dependence between flip-flops with a feedback loop in the hardware description and variables associated therewith in a high-level description; and

a checking unit which performs by the program process, checking for the equivalence using the correlation information related to the backward data dependence.

18. The equivalence checking device according to claim 17 ,

wherein the generation unit extracts by the program process, a reset cycle number corresponding to the minimum number of stages of flip-flops necessary to carry values to the flip-flops in the feedback loop, and

wherein the checking unit checks by the program process, equivalence by an inductive method, with a symbolic simulation result corresponding to the extracted reset cycle number being taken as an initial state of the feedback loop.

19. The equivalence checking device according to claim 18 , wherein the generation unit generates by the program process, as the correlation information related to the backward data dependence, first correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

20. The equivalence checking device according to claim 19 , wherein the generation unit generates by the program process, as the correlation information related to the backward data dependence, second correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

21. The equivalence checking device according to claim 20 ,

wherein the generation unit further generates by the program process, as support information for equivalence checking, correlation information related to a forward data dependence indicative of a correspondence relation between flip-flops without a feedback loop in a behavioral synthesis result and variables associated therewith in a high-level description, and

wherein the checking unit checks by the program process, equivalence using the correlation information related to the forward data dependence along with the correlation information related to the backward data dependence.

22. The equivalence checking device according to claim 21 , wherein the generation unit generates by the program process, as the correlation information related to the forward data dependence, third correlation information in which flip-flops corresponding to variables are placed in a one-to-one correspondence with the variables.

23. The equivalence checking device according to claim 22 , wherein the generation unit generates by the program process, as the correlation information related to the forward data dependence, fourth correlation information in which flip-flops corresponding to variables are placed in a one-to-many correspondence with the variables.

24. The equivalence checking device according to claim 23 , wherein the generation unit performs by the program process, a necessary addition and modification on the reset cycle number, the first correlation information related to the backward data dependence, the second correlation information related to the backward data dependence, the third correlation information related to the forward data dependence and the fourth correlation information related to the forward data dependence in accordance with priorities, and

wherein the checking unit checks by the program process, equivalence by reflection of the support information for the equivalence checking subjected to the necessary addition and modification thereon, assigns, as priorities related to the addition and modification, a first priority to the reset cycle number, a second priority to the first correlation information related to the backward data dependence, a third priority to the second correlation information related to the backward data dependence, a fourth priority to the third correlation information related to the forward data dependence, and a fifth priority to the fourth correlation information related to the forward data dependence, respectively, and performs the addition and modification in accordance with the priorities when a process for equivalence checking is not completed within a predetermined time constraint.