Method and system for realizing a logic model design
View Patent ↗Techniques directed to realizing and verifying a logic model design are provided by first dividing the logic model design into two or more logic portions. The various model portions can then realized to form various realized logic portions. A first realized logic portion can then be wrapped and formally verified against its respective model. The wrapper can then be verified by first applying the wrapper to a second logic model portion and a second realized logic portion, then formally verifying them against each other. The resulting output can then be used to prove wrapper correctness.
1. A method for realizing a logic model design, comprising:
dividing a logic model design into two or more logic model portions;
performing a realization step on a first logic model portion to produce a first realized logic portion;
applying a first wrapper to the first realized logic portion;
verifying the functionality of the first wrapped realized logic portion; and
verifying the functionality of the first wrapper if the first wrapped realized logic portion is verified to be functioning correctly.
2. The method of claim 1 , wherein verifying the functionality of the first realized logic portion includes performing a verification operation on the first wrapped realized logic portion to produce a first realized output.
3. The method of claim 1 , wherein verifying the functionality of the first realized logic portion includes:
performing a verification operation on the first wrapped realized logic portion to produce a first realized output;
performing a verification operation on the first logic model portion to produce a first model output; and
comparing the first realized output to the first model output.
4. The method of claim 3 , further comprising:
performing a realization step on a second logic model portion to produce a-second realized logic portion; and
performing a verification operation on the second realized logic portion to produce a second realized output.
5. The method of claim 4 , further comprising:
applying the first wrapper to the second logic model portion;
performing a verification operation on the second wrapped logic model portion to produce a second model output; and
comparing the second realized output to the second model output.
6. The method of claim 3 , wherein the functionality of the first wrapper is verified using an associativity-based technique.
7. The method of claim 3 , wherein verifying the functionality of the first wrapper includes:
applying the first wrapper to a second logic model portion, and
performing a verification operation on the second wrapped logic model portion to produce a second model output.
8. The method of claim 7 , wherein verifying the functionality of the first wrapper further includes:
performing a verification operation on the second realized logic portion to produce a second realized output, and
comparing the second realized output to the second model output.
9. The method of claim 7 , wherein the first wrapper is applied to the output of the first realized logic portion and further applied to the input of the second logic model portion.
10. The method of claim 8 , wherein an input of the second logic model portion is logically linked to an output of the first logic model portion.
11. A machine-readable medium including instructions for realizing a logic model design and being arranged to cause a machine to perform the steps of:
dividing a logic model design into two or more logic model portions;
performing a realization step on a first logic model portion to produce a first realized logic portion;
applying a first wrapper to the first realized logic portion;
verifying the functionality of the first wrapped realized logic portion; and
verifying the functionality of the first wrapper if the first wrapped realized logic portion is verified to be functioning correctly.
12. The machine-readable medium of claim 11 , wherein verifying the functionality of the first realized logic portion includes performing a verification operation on the first wrapped realized logic portion to produce a first realized output.
13. The machine-readable medium of claim 11 , wherein verifying the functionality of the first realized logic portion includes:
performing a verification operation on the first wrapped realized logic portion to produce a first realized output;
performing a verification operation on the first logic model portion to produce a first model output; and
comparing the first realized output to the first model output.
14. The machine-readable medium of claim 13 , further including the steps of:
performing a realization on a second logic model portion to produce a second realized logic portion; and
performing a verification operation on the second realized logic portion to produce a second realized output.
15. The machine-readable medium of claim 14 , further including the steps of:
applying the first wrapper to the second logic model portion;
performing a verification operation on the second wrapped logic model portion to produce a second model output; and
comparing the second realized output to the second model output.
16. The machine-readable medium of claim 13 , wherein the step of verifying the functionality of the first wrapper uses an associativity-based technique.
17. The machine-readable medium of claim 13 , wherein verifying the functionality of the first wrapper includes:
applying the first wrapper to a second logic model portion, and
performing a verification operation on the second wrapped logic model portion to produce a second model output.
18. The machine-readable medium of claim 17 , wherein verifying the functionality of the first wrapper further includes:
performing a verification operation on the second realized logic portion to produce a second realized output, and
comparing the second realized output to the second model output.
19. The machine-readable medium of claim 18 , wherein the first wrapper is applied to the output of the first realized logic portion and the further applied to the input of the second logic model portion.
20. The machine-readable medium of claim 18 , wherein an input of the second logic model portion is logically linked to an output of the first logic model portion.
21. An apparatus for realizing a logic model design, comprising:
logic development circuitry operable to divide a logic model design into two or more logic model portions, said development circuitry being further operable to realize at least one logic model portion to form a first realized logic portion;
a wrapping device that applies a first wrapper to the first realized logic portion; and
one or more second devices that verify the functionality of the first wrapped realized logic portion and verify the functionality of the first wrapper if the first wrapped realized logic portion is verified to be functioning correctly.
22. The apparatus of claim 21 , wherein the one or more second devices includes a verification device, that performs a verification operation on the first wrapped realized logic portion to produce a first realized output.
23. The apparatus of claim 21 , wherein the one or more second devices includes:
a verification device that performs a verification operation on the first wrapped realized logic portion to produce a first realized output, and wherein the verification device further performs a verification operation on the first logic model portion to produce a first model output; and
a comparing device that compares the first realized output to the first model output.
24. The apparatus of claim 23 , wherein the verification device further performs a verification operation on a second realized logic portion to produce a second realized output, the second realized logic portion being realized based on a second logic model portion.
25. The apparatus of claim 24 , wherein the wrapping device further applies the first wrapper to the second logic model portion, wherein the verification device further performs a verification operation on the second wrapped logic model portion to produce a second model output and wherein the comparing device further compares the second realized output to the second model output.
26. The apparatus of claim 23 , wherein the apparatus verifies the functionality of the first wrapper using an associativity-based technique.
27. The apparatus of claim 23 , wherein the wrapping device further applies the first wrapper to a second logic model portion, and wherein the verification device further performs a verification operation on the second wrapped logic model portion to produce a second model output.
28. The apparatus of claim 27 , wherein the verification device further performs a verification operation on the second realized logic portion to produce a second realized output, and the comparing device further compares the second realized output to the second model output.
29. The apparatus of claim 27 , wherein the first wrapper is applied to the output of the first realized logic portion and the further applied to the input of the second logic model portion.
30. The apparatus of claim 28 , wherein an input of the second logic model portion is logically linked to an output of the first logic model portion.
31. A method for realizing a logic model design, comprising:
dividing a logic model design into two or more logic model portions;
performing realization steps on first and second logic model portions to produce respective first and second realized logic portions;
applying a first wrapper to the first realized logic portion and performing a verification operation to verify the first realized logic portion has correct functionality; and
applying the first wrapper to the second logic model portion and performing a verification operation to verify the first wrapper if the first wrapped realized logic portion is verified to be functioning correctly.
32. A computer program product including a computer readable medium including program code for realizing a logic model design and arranged to cause performance of the steps of claim 31 .
33. A method for realizing a logic model design divided into two or more logic model portions, comprising:
realizing a first logic model portion to produce a first realized logic portion; and
formally verifying the functionality of the first wrapped realized logic portion using a first wrapper applied to the first realized logic portion; and
verifying the functionality of the first wrapper if the first wrapped realized logic portion is verified to be functioning correctly.
34. The method of claim 33 , wherein verifying the first wrapper includes the step of:
applying the first wrapper to a second realized logic portion; and
performing a formal verification on the second wrapped logic model portion.
35. The method of claim 33 , wherein verifying the first wrapper includes the step of:
applying the first wrapper to a second logic model portion; and
performing a formal verification on the second wrapped logic model portion.
36. The method of claim 34 , wherein verifying the first wrapper uses an associativity-based technique.