System, method, and computer program product for over-constraint/deadcode detection in a formal verification
The present disclosure relates to a method for use in the formal verification of an electronic circuit. Embodiments may include receiving, using a processor, a portion of an electronic circuit design and analyzing a syntactic structure of a string associated with the electronic circuit design. Embodiments may also include generating a parse tree, based upon, at least in part, the analysis and traversing the parse tree to identify one or more conditional nodes. Embodiments may further include generating a new node for each of the one or more conditional nodes and displaying, at a graphical user interface, a check, at least one of the one or more conditional nodes or the new node prior to performing either register-transfer-level RTL synthesis or final synthesis.
1. A computer-implemented method comprising:
receiving, using a processor, a portion of an electronic circuit design;
analyzing a syntactic structure of a string associated with the electronic circuit design;
generating a parse tree, based upon, at least in part, the analysis;
traversing the parse tree to identify one or more conditional nodes;
generating a new node for each of the one or more conditional nodes; and
displaying, at a graphical user interface, an option to define or select a check associated with at least one of the one or more conditional nodes or the new node prior to performing either register-transfer-level RTL synthesis or final synthesis.
2. The computer-implemented method of claim 1 , wherein the string is based upon, at least in part, a grammar corresponding to a set of rules used to describe all possible strings of a programming language.
3. The computer-implemented method of claim 1 , wherein the portion of an electronic circuit design includes an HDL file.
4. The computer-implemented method of claim 1 , wherein the one or more conditional nodes represent at least one of a then path and an else path.
5. The computer-implemented method of claim 1 , wherein the new node corresponds to an automatic reachability check.
6. The computer-implemented method of claim 1 , wherein the parse tree includes at least one deadcode check.
7. The computer-implemented method of claim 6 , further comprising:
allowing a user to filter, using the graphical user interface, the at least one deadcode check.
8. A computer-readable storage medium, the computer-readable storage medium having stored thereon instructions that when executed by a machine result in one or more operations, the operations comprising:
receiving, using a processor, a portion of an electronic circuit design;
analyzing a syntactic structure of a string associated with the electronic circuit design;
generating a parse tree, based upon, at least in part, the analysis;
traversing the parse tree to identify one or more conditional nodes;
generating a new node for each of the one or more conditional nodes; and
displaying, at a graphical user interface, an option to define or select a check associated with at least one of the one or more conditional nodes or the new node prior to performing either register-transfer-level RTL synthesis or final synthesis.
9. The computer-readable storage medium of claim 8 , wherein the string is based upon, at least in part, a grammar corresponding to a set of rules used to describe all possible strings of a programming language.
10. The computer-readable storage medium of claim 8 , wherein the portion of an electronic circuit design includes an HDL file.
11. The computer-readable storage medium of claim 8 , wherein the one or more conditional nodes represent at least one of a then path and an else path.
12. The computer-readable storage medium of claim 8 , wherein the new node corresponds to an automatic reachability check.
13. The computer-readable storage medium of claim 8 , wherein the parse tree includes at least one deadcode check.
14. The computer-readable storage medium of claim 13 , further comprising: allowing a user to filter, using the graphical user interface, the at least one deadcode check.
15. A system comprising:
a computing device having at least one processor configured to receive, using a processor, a portion of an electronic circuit design and to analyze a syntactic structure of a string associated with the electronic circuit design, the at least one processor further configured to generate a parse tree, based upon, at least in part, the analysis, the at least one processor further configured to traverse the parse tree to identify one or more conditional nodes and to generate a new node for each of the one or more conditional nodes, the at least one processor further configured to display, at a graphical user interface, an option to define or select a check associated with at least one of the one or more conditional nodes or the new node prior to performing either register-transfer-level RTL synthesis or final synthesis.
16. The system of claim 15 , wherein the string is based upon, at least in part, a grammar corresponding to a set of rules used to describe all possible strings of a programming language.
17. The system of claim 15 , wherein the portion of an electronic circuit design includes an HDL file.
18. The system of claim 15 , wherein the one or more conditional nodes represent at least one of a then path and an else path.
19. The system of claim 15 , wherein the new node corresponds to an automatic reachability check.
20. The system of claim 15 , wherein the parse tree includes at least one deadcode check.