Patent application EP17176642A (EP), filed 2017-06-19
Publication number: EP3261002A1
Title: LIVELOCK DETECTION IN A HARDWARE DESIGN USING FORMAL VERIFICATION
Abstract: A hardware monitor arranged to detect livelock in a hardware design for an integrated circuit. The hardware monitor includes monitor and detection logic configured to detect when a particular state has occurred in the hardware design; and assertion evaluation logic configured to periodically evaluate one or more assertions that assert a formal property related to reoccurrence of the particular state in the hardware design to detect whether the hardware design is in a livelock comprising the predetermined state. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design cannot enter a livelock comprising the predetermined state.
IPC codes: G06F  17/    50            A I
G06F  11/    07            A I
G06F  11/    30            A I
G06F  30/  3323            A I
G06F  30/   333            A I
Claims: number: 1
text: A computer-implemented method (200) of detecting livelock in a hardware design (102, 502) for an integrated circuit (104, 504), the method (200) comprising:
number: 2
text: The method (200) of claim 1, wherein the assertion evaluation logic (110, 310, 510) is configured to evaluate one or more formal assertions that assert that if the particular state has occurred in the hardware design (102, 502) that the particular state does not reoccur in the hardware design (102, 502) within a predetermined number of clock cycles.
number: 3
text: The method (200) of claim 2, wherein the monitor and detection logic (108, 308) comprises a state register (316) and state detection logic (314) configured to detect when the particular state has occurred in the hardware design (102) and in response to detecting the particular state has occurred in the hardware design (102), set the state register (316).
number: 4
text: The method (200) of claim 2, wherein the integrated circuit (504) forms a processor and the particular state is that the processor has fetched an instruction from a symbolic address; and wherein the assertion evaluation logic (110, 510) is configured to evaluate one or more formal assertions that assert that if the processor has fetched an instruction from the symbolic address the processor does not fetch an instruction from the symbolic address within the predetermined number of clock cycles.
number: 5
text: The method (200) of claim 4, wherein the processor is configured to execute a plurality of different instructions and the assertion evaluation logic (110, 510) is configured to evaluate an assertion for each of the different instructions that asserts that if the processor has fetched an instruction from the symbolic address that is the particular instruction then the processor cannot fetch an instruction from the symbolic address within the predetermined number of clock cycles.
number: 6
text: The method (200) of claim 4 or claim 5, wherein the monitor and detection logic (108, 508) comprises a symbolic fetch register (516) and symbolic fetch detection logic (514) configured to detect when the processor (504) has fetched an instruction from the symbolic address, and in response to detecting the processor has fetched an instruction from the symbolic address, set the symbolic fetch register (516).
number: 7
text: The method (200) of claim 1, wherein the assertion evaluation logic (110, 710) is configured to evaluate one or more formal assertions that assert that a number of occurrences of the particular state between a start event and a stop event is less than a predetermined number.
number: 8
text: The method (200) of claim 7, wherein the integrated circuit forms a processor and the start event is when the processor is in an idle state and the stop event is when the processor is in an idle state.
number: 9
text: The method (200) of claim 7 or claim 8, wherein the monitor and detection logic (708) comprises:
number: 10
text: The method (200) of any of claims 1 to 9, wherein when the hardware design (102, 502) is processed in an integrated circuit manufacturing system (1002), the hardware design (102, 502) configures the integrated circuit manufacturing system (1002) to manufacture the integrated circuit (104, 504).
number: 11
text: The method (200) of any preceding claim, further comprising, when one of the one or more formal assertions is not successfully verified, outputting, an indication of a sequence of states of the hardware design (102, 502) in which that formal assertion is not true.
number: 12
text: The method (200) of any preceding claim, wherein the particular state is based on a symbolic variable, and formally verifying the one or more formal assertions comprises formally verifying the one or more formal assertions are true for the hardware design for each valid value of the symbolic variable.
number: 13
text: The method (200) of any preceding claim, further comprising, in response to each of the one or more formal assertions being successfully verified, generating a hardware manifestation of the integrated circuit based on the hardware design.
number: 14
text: A system (100) configured to detect livelock in a hardware design (102, 502) for an integrated circuit (104, 504), the system (100) comprising:
number: 15
text: A hardware monitor (106, 300, 500, 700) arranged to detect livelock in a hardware design (102, 502) for an integrated circuit (104, 504), the hardware monitor (106, 300, 500, 700) comprising:
Office action: search_report, dated 2017-12-27
Prior art cited: ref_id: US6553514B1
ref_type: patent
severity: background
ref_id: EP3168746A1
ref_type: patent
severity: background
ref_id: GB2526052A
ref_type: patent
severity: background
ref_id: - JESSE G BEU ET AL: "High-speed formal verification of heterogeneous coherence hierarchies", HIGH PERFORMANCE COMPUTER ARCHITECTURE (HPCA2013), 2013 IEEE 19TH INTERNATIONAL SYMPOSIUM ON, IEEE, 23 February 2013 (2013-02-23), pages 566 - 577, XP032415851, ISBN: 978-1-4673-5585-8, DOI: 10.1109/HPCA.2013.6522350
ref_type: npl
severity: background
ref_id: US6553514
ref_type: patent
severity: background
ref_id: GB2526052
ref_type: patent
severity: background
ref_id: EP3168746
ref_type: patent
severity: background
ref_id: - JESSE G BEU ET AL, "High-speed formal verification of heterogeneous coherence hierarchies", HIGH PERFORMANCE COMPUTER ARCHITECTURE (HPCA2013), 2013 IEEE 19TH INTERNATIONAL SYMPOSIUM ON, IEEE, (20130223), doi:10.1109/HPCA.2013.6522350, ISBN 978-1-4673-5585-8, pages 566 - 577, XP032415851 [A] 1-15 * the whole document *
ref_type: npl
severity: background
Final disposition: pending (2017-12-27)