Verification of scheduling in the presence of loops using uninterpreted symbolic simulation

• US 6,745,160 B1
• Filed: 10/08/1999
• Issued: 06/01/2004
• Est. Priority Date: 10/08/1999
• Status: Expired due to Fees

• Current Assignee: NEC Corporation
• Original Assignee: NEC Corporation
• Inventors: Bhattacharya, Subhrajit, Gupta, Aarti, Ashar, Pranav, Raghunathan, Anand
• Primary Examiner(s): Jones, Hugh
• Assistant Examiner(s): FERRIS III, FRED O
• Application Number:
  US09/414,815
• Time in Patent Office: 1,698 Days
• Field of Search: 716/18, 716/1, 703/2, 703/14, 703/15, 703/16, 703/13, 714/807
• US Class Current: 703/14
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A method of checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description. The method comprising extracting loop invariants to determine a sufficient set of acyclic threads when loops are present, performing symbolic simulation to extract the above loop invariants, and proving equivalence of the acyclic threads. Systems, computer systems and computer program products that incorporate the techniques of verification and correctness checking according to the present invention have also been disclosed.

Claims

1. A method of verifying a schedule of a circuit against a behavioral description of the circuit, said method comprising:

(a) specifying the schedule as a schedule state transition graph;

(b) representing a behavior of the circuit as a behavioral state transition graph;

(c) selecting a schedule thread of execution from said schedule state transition graph;

(d) identifying a corresponding behavior thread from said behavioral state transition graph;

(e) converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph;

(f) checking equivalence of said schedule structure graph and said behavior structure graph; and

(g) repeating steps (c)-(f) for all threads of execution.

2. The method of claim 1 wherein step (f) further comprises:

(i) creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node;

(ii) creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node;

(iii) traversing arr1 and identifying basis variables in the behavior structure graph;

(iv) expressing non-basis variables in the behavior structure graph in terms of basis variables;

(v) constructing equivalence lists for input nodes in the schedule structure graph;

(vi) traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule structures graph to output of the schedule structure graph, wherein an entry in each of said equivalence lists is a pair

(u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence;

(vii) checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; and

(viii) repeating step (vii) for all output nodes in arr2; and

(ix) finding equivalence if all output nodes are found to be equivalent.

3. A method of verifying equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said method comprising:

(a) representing the schedule as a schedule state transition graph;

(b) representing the behavior as a behavior state transition graph;

(c) identifying strongly connected components in the schedule state transition graph;

(d) identifying exit nodes in each of said strongly connected components;

(e) collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components;

(f) selecting a hitherto unselected path;

(g) obtaining a structural RTL circuit for the path selected in step (f);

(h) adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path;

(i) performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph, and obtaining a structural RTL circuit for said path;

(j) selecting a hitherto unselected strongly connected component in the selected path;

(k) extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets;

(l) selecting a correspondence set from the list of correspondence sets;

(m) redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation;

(n) repeating steps (i)-(m) for all correspondence set in the list of correspondence sets;

(o) testing if an output equivalence condition is conditional on anything other than path conditions;

(p) reporting non-equivalence and exiting this method if said output equivalence is conditional in step (o);

(q) repeating steps (j)-(p) for all strongly connected components in the selected path; and

(r) repeating steps (f)-(q) for all paths from a root to sink such that any exit point appears at most thrice.

4. The method of claim 3 wherein the unconstrained symbolic simulation of step (i) is performed using a process comprising:

(i) assigning a begin state of the behavior state transition graph to a permissible paths list;

(ii) selecting a hitherto unvisited state in the permissible paths list;

(iii) generating a behavior structural RTL;

(iv) performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL;

(v) adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero;

(vi) repeating sub-step (v) for each outgoing transition from Si to Sj; and

(vii) repeating steps (iii)-(vi) for all unvisited states until only unvisited states remaining in permissible paths list are instances of an end state.

5. The method of claim 3 wherein invariants are extracted from loops in step (k) using a process comprising for each loop:

(i) identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop;

(ii) identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the subcircuits between the first and second, and second and third cuts are isomorphic;

(iii) identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits;

(iv) checking if the equivalence relationships between the latest and its previous cuts are identical;

(v) if the relationships of step (iv) are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vi) if the relationships of step (iv) are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vii) if the relationships in step (iv) are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets;

(viii) removing all entries in the set of equivalence relationship sets that are supersets of other entries;

(ix) designating the final set of equivalence relationship sets as the desired set of invariants.

6. A system for checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, said system comprising:

a loop invariants extractor to determine a sufficient set of acyclic threads when loops are present;

a symbolic simulator to extract the loop invariants; and

an equivalence prover to prove equivalence of the acyclic threads.

7. The system of claim 6 wherein said behavioral description is transformed through introduction of cycle boundaries.

8. The system of claim 6 wherein said behavioral description is transformed through operation reordering.

9. The system of claim 6 wherein said behavioral description is transformed through loop unrolling, winding, folding and pipelining.

10. The system of claim 6 wherein said behavioral description is transformed through speculative execution of operations.

11. A system for verifying a schedule of a circuit against a behavioral description of the circuit, comprising:

a schedule state transition graph generator for specifying the schedule as a schedule state transition graph;

a behavior state transition graph generator for specifying the behavior of the circuit as a behavioral state transition graph;

a schedule thread selector for selecting a schedule thread of execution from said schedule state transition graph;

a behavior thread selector for selecting a corresponding behavior thread from said behavioral state transition graph;

a convertor for converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; and

an equivalence checker for checking equivalence of said schedule structure graph and said behavior structure graph.

12. A computer system with a processor and memory for checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, said memory comprising instructions said instructions capable of enabling the computer to perform said checking, said instructions comprising:

instructions for extracting loop invariants to determine a sufficient set of acyclic threads when loops are present;

instructions for symbolic simulation to extract the loop invariants; and

instructions to prove equivalence of the acyclic threads.

13. The computer system of claim 12 wherein said behavioral description is transformed through introduction of cycle boundaries.

14. The computer system of claim 12 wherein said behavioral description is transformed through operation reordering.

15. The computer system of claim 12 wherein said behavioral description is transformed through loop unrolling, winding, folding and pipelining.

16. The computer system of claim 12 wherein said behavioral description is transformed through speculative execution of operations.

17. A computer system with a processor and memory for verifying a schedule of a circuit against a behavioral description of the circuit, said

memory comprising instructions capable of enabling the computer to perform said verifying, said instructions comprising:

instructions for specifying the schedule as a schedule state transition graph;

instructions for representing a behavior of the circuit as a behavioral state transition graph;

instructions for selecting a schedule thread of execution from said schedule state transition graph;

instructions for selecting a corresponding behavior thread from said behavioral state transition graph;

instructions for converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph;

instructions for checking equivalence of said schedule structure graph and said behavior structure graph; and

instructions for repeating through all threads of execution.

18. A computer system with a processor and memory for verifying a schedule of a circuit against a behavioral description of the circuit, said memory comprising instructions, said instructions capable of enabling the computer to perform the following steps:

(a) specifying the schedule as a schedule state transition graph;

(b) representing a behavior of the circuit as a behavioral state transition graph;

(c) selecting a schedule thread of execution from said schedule state transition graph;

(d) identifying a corresponding behavior thread from said behavioral state transition graph;

(e) converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph;

(f) checking equivalence of said schedule structure graph and said behavior structure graph; and

(g) repeating steps (c)-(f) for all threads of execution.

19. The computer system of claim 18 wherein said instructions further comprises instructions capable of enabling the computer to perform step (f) using the following steps:

(i) creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node;

(ii) creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node;

(iii) traversing arr1 and identifying basis variables in the behavior structure graph;

(iv) expressing non-basis variables in the behavior structure graph in terms of basis variables;

(v) constructing equivalence lists for input nodes in the schedule structure graph;

(vi) traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule structures graph to output of the schedule structure graph,

wherein an entry in each of said equivalence lists is a pair (u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence;

(vii) checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; and

(viii) repeating step (vii) for all output nodes in arr2; and

(ix) finding equivalence if all output nodes are found to be equivalent.

20. A computer system with a processor and memory for verifying equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said memory comprising instructions capable of enabling the computer to perform said verifying using the following steps:

(a) representing the schedule as a schedule state transition graph;

(b) representing the behavior as a behavior state transition graph;

(c) identifying strongly connected components in the schedule state transition graph;

(d) identifying exit nodes in each of said strongly connected components;

(e) collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components;

(f) selecting a hitherto unselected path;

(g) obtaining a structural RTL circuit for the path selected in step (f);

(h) adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path;

(i) performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph, and obtaining a structural RTL circuit for said path;

(j) selecting a hitherto unselected strongly connected component in the selected path;

(k) extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets;

(l) selecting a correspondence set from the list of correspondence sets;

(m) redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation;

(n) repeating steps (i)-(m) for all correspondence set in the list of correspondence sets;

(o) testing if an output equivalence condition is conditional on anything other than path conditions

(p) reporting non-equivalence and exiting this method if said output equivalence is conditional in step o;

(q) repeating steps (j)-(p) for all strongly connected components in the selected path; and

(r) repeating steps (f)-(q) for all paths from a root to sink such that any exit point appears at most thrice.

21. The computer system of claim 20 wherein said instructions further comprises instructions capable of enabling the computer to perform step (i) using the following steps:

(i) assigning a begin state of the behavior state transition graph to a permissible paths list;

(ii) selecting a hitherto unvisited state in the permissible paths list;

(iii) generating a behavior structural RTL

(iv) performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL;

(v) adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero;

(vi) repeating sub-step v for each outgoing transition from Si to Sj; and

(vii) repeating steps iii to vi for all unvisited states until only unvisited states remaining in permissible paths list are instance of an end state.

22. The computer system of claim 20 wherein said instructions further comprises instructions capable of enabling the computer to perform step (k) using the following steps for each loop:

(i) identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop;

(ii) identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the

subcircuits between the first and second, and second and third cuts are isomorphic;

(iii) identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits;

(iv) checking if the equivalence relationships between the latest and its previous cuts are identical;

(v) if the relationships of step (iv) are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vi) if the relationships of step (iv) are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vii) if the relationships in step (iv) are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets;

(viii) removing all entries in the set of equivalence relationship sets that are supersets of other entries;

(ix) designating the final set of equivalence relationship sets as the desired set of invariants.

23. A computer program product including a computer readable media comprising computer code that is capable of enabling a computer to check correctness of scheduling of a circuit, where a schedule for the circuit is obtained from a behavioral description, said computer code comprising:

computer code for extracting loop invariants to determine a sufficient set of acyclic threads when loops are present;

computer code for symbolic simulation to extract the loop invariants; and

computer code to prove equivalence of the acyclic threads.

24. The computer program product of claim 23 wherein said behavioral description is transformed through introduction of cycle boundaries.

25. The computer program product of claim 23 wherein said behavioral description is transformed through operation reordering.

26. The computer program product of claim 23 wherein said behavioral description is transformed through loop unrolling, winding, folding and pipelining.

27. The computer program product of claim 23 wherein said behavioral description is transformed through speculative execution of operations.

28. A computer program product including a computer readable media comprising computer code that is capable of enabling a computer to verify a schedule of a circuit against a behavioral description of the circuit, said computer code comprising:

a schedule state transition graph generator code for enabling the computer to specify the schedule as a schedule state transition graph;

a behavior state transition graph generator code for enabling the computer to specify the behavior of the circuit as a behavioral state transition graph;

a schedule thread selector code for enabling the computer to select a schedule thread of execution from said schedule state transition graph;

a behavior thread selector code for enabling the computer to select a corresponding behavior thread from said behavioral state transition graph;

a convertor code for enabling the computer to convert said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; and

an equivalence checker code for enabling the computer to check equivalence of said schedule structure graph and said behavior structure graph.

29. A computer program product including a computer readable media comprising computer code that is capable of enabling a computer to verify a schedule of a circuit against a behavioral description of the circuit, said computer code enabling the computer to perform the following steps:

(a) specifying the schedule as a schedule state transition graph;

(b) representing a behavior of the circuit as a behavioral state transition graph;

(c) selecting a schedule thread of execution from said schedule state transition graph;

(d) identifying a corresponding behavior thread from said behavioral state transition graph;

(e) converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph;

(f) checking equivalence of said schedule structure graph and said behavior structure graph; and

(g) repeating steps (c)-(f) for all threads of execution.

30. The method of claim 29 wherein said computer code is capable of enabling the computer to perform step (f) using the following steps:

(i) creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node;

(ii) creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node;

(iii) traversing arr1 and identifying basis variables in the behavior structure graph;

(iv) expressing non-basis variables in the behavior structure graph in terms of basis variables;

(v) constructing equivalence lists for input nodes in the schedule structure graph;

(vi) traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule

structures graph to output of the schedule structure graph, wherein an entry in each of said equivalence lists is a pair (u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence;

(vii) checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; and

(viii) repeating step (vii) for all output nodes in arr2; and

(ix) finding equivalence if all output nodes are found to be equivalent.

31. A computer program product including a computer readable media comprising computer code that is capable of enabling a computer to verify a equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said computer code enabling the computer to perform the following steps:

(a) representing the schedule as a schedule state transition graph;

(b) representing the behavior as a behavior state transition graph;

(c) identifying strongly connected components in the schedule state transition graph;

(d) identifying exit nodes in each of said strongly connected components;

(e) collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components;

(f) selecting a hitherto unselected path;

(g) obtaining a structural RTL circuit for the path selected in step (f);

(h) adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path;

(i) performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph, and obtaining a structural RTL circuit for said path;

(j) selecting a hitherto unselected strongly connected component in the selected path;

(k) extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets;

(l) selecting a correspondence set from the list of correspondence sets;

(m) redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation;

(n) repeating steps (i)-(m) for all correspondence set in the list of correspondence sets;

(o) testing if an output equivalence condition is conditional on anything other than path conditions;

(p) reporting non-equivalence and exiting this method if said output equivalence is conditional in step o;

(q) repeating steps (j)-(p) for all strongly connected components in the selected path; and

(r) repeating steps (f)-(q) for all paths from a root to sink such that any exit point appears at most thrice.

32. The computer program code of claim 31 wherein the computer code is capable of enabling the computer to perform unconstrained symbolic simulation of step (i) using the following steps:

(i) assigning a begin state of the behavior state transition graph to a permissible paths list;

(ii) selecting a hitherto unvisited state in the permissible paths list;

(iii) generating a behavior structural RTL

(iv) performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL;

(v) adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero;

(vi) repeating sub-step v for each outgoing transition from Si to Sj; and

(vii) repeating steps iii to vi for all unvisited states until only unvisited states remaining in permissible paths list are instance of an end state.

33. The computer program code of claim 31 wherein the computer code is capable of enabling the computer to extract invariants in step (k) using the following steps for each loop:

(i) identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop;

(ii) identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the subcircuits between the first and second, and second and third cuts are isomorphic;

(iii) identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits;

(iv) checking if the equivalence relationships between the latest and its previous cuts are identical;

(v) if the relationships of step (iv) are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vi) if the relationships of step (iv) are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeat from step (iii);

(vii) if the relationships in step (iv) are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets;

(viii) removing all entries in the set of equivalence relationship sets that are supersets of other entries;

designating the final set of equivalence relationship sets as the desired set of invariants.