公开(公告)号：US11593193B2

公开(公告)日：2023-02-28

申请号：US17338538

申请日：2021-06-03

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G06F11/07 ,  G06F21/52 ,  G06F30/30 ,  G06F30/392 ,  G06F115/10 ,  G06F117/06

Abstract: Out-of-bounds recovery circuits configured to detect an out-of-bounds violation in an electronic device, and cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation is detected. The out-of-bounds recovery circuits include detection logic configured to detect that an out-of-bounds violation has occurred when a processing element of the electronic device has fetched an instruction from an unallowable memory address range for the current operating state of the electronic device; and transition logic configured to cause the electronic device to transition to a predetermined safe state when an out-of-bounds violation has been detected by the detection logic.

公开(公告)号：US11475193B2

公开(公告)日：2022-10-18

申请号：US17167698

申请日：2021-02-04

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Sam Elliott

IPC: G06F30/3312 ,  G06F119/12 ,  G06F30/33

Abstract: Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data should be equal to one of one or more predetermined values.

公开(公告)号：US11250927B2

公开(公告)日：2022-02-15

申请号：US16792582

申请日：2020-02-17

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G11C29/00 ,  G11C29/38 ,  G06F11/22 ,  G06F11/30 ,  G06F11/34 ,  G11C29/12 ,  G11C29/44 ,  G11C29/04

Abstract: Hardware monitors which can be used by a formal verification tool to exhaustively verify a hardware design for a memory unit. The hardware monitors include detection logic to monitor one or more control signals and/or data signals of an instantiation of the memory unit to detect symbolic writes and symbolic reads. In some examples a symbolic write is a write of symbolic data to a symbolic address; and in other examples a symbolic write is a write of any data to a symbolic address. A symbolic read is a read of the symbolic address. The hardware monitors also include assertion verification logic that verifies an assertion that read data corresponding to a symbolic reads matches write data associated with one or more symbolic writes preceding the read.

公开(公告)号：US11250192B2

公开(公告)日：2022-02-15

申请号：US17168945

申请日：2021-02-05

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G06F30/3323 ,  G06F11/07 ,  G06F11/34 ,  G06F30/39

Abstract: A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory address of the fetched instruction to an allowable memory address range associated with the current operating state of the instantiation of the hardware design to determine whether there has been an out-of-bounds violation. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design does not cause an instruction to be fetched from an out-of-bounds address.

公开(公告)号：US20210117602A1

公开(公告)日：2021-04-22

申请号：US17133294

申请日：2020-12-23

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G06F30/3323 ,  G06F11/07 ,  G06F11/30 ,  G06F30/33 ,  G06F9/30 ,  G06F9/38

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 an instantiation of 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 instantiation of the hardware design to detect whether the instantiation of 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 instantiation of the hardware design cannot enter a livelock comprising the predetermined state.

公开(公告)号：US10949590B2

公开(公告)日：2021-03-16

申请号：US16399218

申请日：2019-04-30

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Sam Elliott

IPC: G06F30/3312 ,  G06F30/33 ,  G06F119/12

Abstract: Methods and systems for verifying that logic for implementing a pipelined process in hardware correctly moves data through the pipelined process. The method includes: (a) monitoring data input to the pipelined process to determine when watched data has been input to the pipelined process; (b) in response to determining the watched data has been input to the pipelined process counting a number of progressing clock cycles for the watched data; and (c) evaluating an assertion written in an assertion based language, the assertion establishing that when the watched data is output from the pipelined process the counted number of progressing clock cycles for the watched data should be equal to one of one or more predetermined values.

公开(公告)号：US10936775B2

公开(公告)日：2021-03-02

申请号：US16930424

申请日：2020-07-16

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G06F30/3323 ,  G06F30/39 ,  G06F11/34 ,  G06F11/07

Abstract: A hardware monitor arranged to detect out-of-bounds violations in a hardware design for an electronic device. The hardware monitors include monitor and detection logic configured to monitor the current operating state of an instantiation of the hardware design and detect when the instantiation of the hardware design implements a fetch of an instruction from memory; and assertion evaluation logic configured to evaluate one or more assertions that assert a formal property that compares the memory address of the fetched instruction to an allowable memory address range associated with the current operating state of the instantiation of the hardware design to determine whether there has been an out-of-bounds violation. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design does not cause an instruction to be fetched from an out-of-bounds address.

公开(公告)号：US10909289B2

公开(公告)日：2021-02-02

申请号：US16419734

申请日：2019-05-22

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Iain Singleton

IPC: G06F30/3323 ,  G06F30/33 ,  G06F11/07 ,  G06F11/30 ,  G06F9/30 ,  G06F9/38 ,  G06F30/333

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 an instantiation of 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 instantiation of the hardware design to detect whether the instantiation of 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 instantiation of the hardware design cannot enter a livelock comprising the predetermined state.

公开(公告)号：US10210119B2

公开(公告)日：2019-02-19

申请号：US15454100

申请日：2017-03-09

Applicant: Imagination Technologies Limited

Inventor： Iain Singleton ,  Ashish Darbari ,  John Alexander Osborne Netterville

IPC: G06F9/455 ,  G06F17/50 ,  G06F13/364 ,  G06F13/16 ,  G06F13/362 ,  G06F13/42

Abstract: Operation of an arbiter in a hardware design is verified. The arbiter receives a plurality of requests over a plurality of clock cycles, including a monitored request and outputs the requests in priority order. The requests received by and output from the arbiter in each clock cycle are identified. The priority of the watched request relative to other pending requests in the arbiter is then tracked using a counter that is updated based on the requests input to and output from the arbiter in each clock cycle and a mask identifying the relative priority of requests received by the arbiter in the same clock cycle. The operation of the arbiter is verified using an assertion which establishes a relationship between the counter and the clock cycle in which the watched request is output from the arbiter.

公开(公告)号：US10083262B2

公开(公告)日：2018-09-25

申请号：US15689021

申请日：2017-08-29

Applicant: Imagination Technologies Limited

Inventor： Ashish Darbari ,  Colin McKellar

IPC: G06F9/455 ,  G06F17/50

Abstract: Methods and systems for detecting deadlock in a hardware design. The method comprises identifying one or more control signals in the hardware design; generating a state machine for each of the one or more control signals to track the state of the control signal; generating one or more assertions for each control signal to detect that the control signal is in a deadlock state from the state machine; and detecting whether any of the one or more control signal are in a deadlock state using the assertions. The method may also comprise generating one or more fairness constraints to impose on a particular assertion and detecting the particular control signal is in the deadlock state using the assertions under the fairness constraints.