System and methods for reasonable functional verification of an integrated circuit design
View Patent ↗A system and methods for reasonable formal verification provides a user with coverage information that is used for verification signoff. The coverage is calculated based on formal analysis techniques and is provided to the user in terms of design-centric metrics rather than formal-centric metrics. Design-centric metrics include the likes of a number of reads from or writes to memories and a number of bit changes for counters, among many others. Accordingly, a setup for failure (SFF) function and a trigger the failure (TTF) function take place. During SFF formal analysis is applied in an attempt to reach a set of states close enough to suspected failure states. During TTF formal analysis is applied, starting from the SFF states, to search for a state violating a predetermined property. If results are inconclusive the user is provided with a design-centric coverage metric that can be used in signoff.
1. A method implemented in a programmable system for reasonable functional verification of a design of an integrated circuit (IC), the method comprising:
retrieving from storage by the programmable system a description of the design of at least a portion of the IC;
causing the programmable system to bring at least a portion of the IC in the received description to a state close to a suspected point of failure through analysis of a setup for failure (SFF) property;
executing by the programmable system functional verification of at least a portion of the design of the IC from the suspected point of failure through analysis of a trigger for failure (TFF) property; and
providing by the programmable system a report respective of a result of the executing of the set of instructions.
2. The method of claim 1 , wherein retrieving from storage a description of at least a portion of the design of the IC further comprises selecting the at least a portion of the design of the IC.
3. The method of claim 1 , wherein the description is provided in a register-transfer level (RTL) description language.
4. The method of claim 1 , wherein to bring at least a portion of the IC in the received description to a state close to a suspected point of failure comprises a bounded checking of the at least a portion of the IC by the programmable system to reach a suspected point of failure which is specific to a property to be verified.
5. The method of claim 1 , wherein the property is defined in an assertion specification language.
6. The method of claim 5 , wherein the assertion specification language is at least one of property specification language (PSL) and System Verilog® assertion (SVA).
7. The method of claim 1 , further comprising determining by the programmable system a coverage metric that is a ratio between a number of operations actually performed for functional verification and a minimum number of operations necessary for a desired level of coverage.
8. The method of claim 7 , further comprising reporting by the programmable system the coverage metric.
9. The method of claim 7 , further comprising reporting by the programmable system reasonable coverage upon determination that no failure respective of a TFF was detected and coverage is equal to or higher than a predetermined coverage metric.
10. The method of claim 1 , further comprising reporting by the programmable system failure upon determination that a failure was detected respective of a TFF.
11. The method of claim 1 , further comprising reporting by the programmable system failure for lack of sufficient coverage upon determination that no failure respective of a TFF was detected and coverage is lower than a predetermined coverage metric.
12. The method of claim 1 , further comprising reporting by the programmable system failure to reach a desired SFF property.
13. A computer software product containing instructions embodied in a non-transitory tangible computer-readable medium that, when executed by the computer, perform the method of claim 1 .
14. A system for reasonable functional verification of a design of an integrated circuit (IC), the system comprising:
a processing unit;
a storage coupled to the processing unit; and,
a memory coupled to the processing unit, the memory containing instructions that when executed by the processing unit: retrieve from storage a description of the design of at least a portion of the IC; bring the at least a portion of the IC in the received description to a state close to a suspected point of failure respective of a setup for failure (SFF) property; execute a set of instructions by functional verification of the at least a portion of the design of the IC from the suspected point of failure respective of at least a trigger for failure (TFF) property; and, providing a report respective of a result of execution of the functional verification.
15. The system of claim 14 , wherein the processing unit comprises one or more central processing units.
16. The system of claim 14 , wherein the system is a computer aided design (CAD) system.
17. The system of claim 14 , wherein the retrieve from storage a description of at least a portion of the design of the IC further comprises a selection of the at least a portion of the design of the IC.
18. The system of claim 14 , wherein the description is provided in a register-transfer level (RTL) description language.
19. The system of claim 14 , wherein the memory further contains instructions that, when executing by the processing unit, provide for a bounded check to reach a suspected point of failure which is specific to a property to be verified.
20. The system of claim 14 , wherein the property is defined in an assertion specification language.
21. The system of claim 20 , wherein the assertion specification language is at least one of property specification language (PSL) and System Verilog® assertion (SVA).
22. The system of claim 14 , wherein the memory further contains instructions that, when executed by the processing unit, provide for determination of a coverage metric that is a ratio between a number of operations actually performed for function verification and a minimum number of operations necessary for a desired level of coverage.
23. The system of claim 22 , wherein the memory further contains instructions that, when executed by the processing unit, provide for a report of the coverage metric.
24. The system of claim 22 , wherein the memory further contains instructions that, when executed by the processing unit, provide for a report of reasonable coverage upon determination that the instructions have executed and no failure was detected respective of a TFF property.
25. The system of claim 14 , wherein the memory further contains instructions that, when executed by the processing unit, provide for a report of failure respective of a TFF property.
26. The system of claim 14 , wherein the memory further contains instructions that, when executed by the processing unit, provide for a report of failure for lack of sufficient coverage upon determination that no failure respective of a TFF property was detected and coverage is lower than a predetermined coverage metric.
27. The system of claim 14 , wherein the memory further contains instructions that, when executed by the processing unit, provide for a report of failure to reach a desired SFF property.