Method and apparatus using formal methods for checking generated-clock timing definitions
View Patent ↗A generated-clock checker compares timing definitions against a register transfer level description of the design using formal methods. The generated-clock checker derives generated-clock timing waveform models from the timing definitions, derives generated-clock waveform models from the register level design and then compares the waveform models using formal methods.
1. A method implemented as a generated-clock checker tool in a programmable computing system for checking timing definitions of generated-clocks against a register-level design for an integrated circuit, the method comprising:
constructing waveform models from both user-specified timing definitions and a register-level design for each generated clock, by considering all logic paths from a master clock to each generated-clock, and keeping track of any inversions in a logic path, while ignoring any combinational logic unrelated to clock generation, and generating finite state machines to represent the waveform models;
comparing, using formal methods, the two sets of constructed waveform models obtained from the timing definitions and the register-level design, by using a satisfiability checker to compare the finite state machines; and
reporting, by using the programmable computing system, any discrepancies found between the two sets of waveforms.
2. The method as in claim 1 , wherein ignoring combinational logic assumes only cases where a clock signal is enabled in the considered logic path.
3. The method as in claim 1 , when the constructing of the waveform models further ignores any logic paths that a user has indicated.
4. The method as in claim 1 , wherein the considering of all logic paths also keeps track of register inputs and outputs.
5. The method as in claim 1 , wherein the user specifies reset conditions that define initial values of registers in the design.
6. The method as in claim 1 , wherein the generated-clock checker reports any mismatched generated-clock timing definitions.
7. The method as in claim 1 , wherein the generated-clock checker reports any missing generated-clock timing definitions.
8. The method as in claim 1 , wherein reporting any waveform discrepancies includes:
displaying actual and expected waveforms and the related logic path between the master clock and the generated-clock.
9. A generated-clock checker software tool stored on a non-transitory storage media and running on a programmed computer for checking user-specified timing definitions of generated-clocks against a register-level design file for an integrated circuit, wherein the computer when running the generated-clock checker:
accepts a timing definition file and a register-level design file from a user input interface or memory access;
constructs sets of waveform models of each generated-clock both from the timing definition file and from the design file, by considering all logic paths from a master clock to each generated-clock, and keeping track of any inversions in a logic path, while ignoring any combinational logic unrelated to clock generation and generating finite state machines to represent the waveform models;
compares the two constructed sets of waveforms using formal methods, by using a satisfiability checker to compare the finite state machines; and
reports any discrepancies between the sets of waveforms.
10. The software tool running on a programmed computer as in claim 9 , wherein ignoring combinational logic assumes only cases where a clock signal is enabled in the considered logic path.
11. The software tool running on a programmed computer as in claim 9 , when the constructing of the waveform models further ignores any logic paths that a user has indicated.
12. The software tool running on a programmed computer as in claim 9 , wherein the considering of all logic paths also keeps track of register inputs and outputs.
13. The software tool running on a programmed computer as in claim 9 , wherein the user specifies reset conditions that define initial values of registers in the design.
14. The software tool running on a programmed computer as in claim 9 , wherein the generated-clock checker reports any mismatched generated-clock timing definitions.
15. The software tool running on a programmed computer as in claim 9 , wherein the generated-clock checker reports any missing generated-clock timing definitions.
16. The software tool running on a programmed computer as in claim 9 , wherein reporting any waveform discrepancies includes:
displaying actual and expected waveforms and the related logic path between the master clock and the generated-clock.