-
公开(公告)号:US20180107825A1
公开(公告)日:2018-04-19
申请号:US15784615
申请日:2017-10-16
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari
CPC classification number: G06F21/572 , G06F21/51 , G06F2221/033
Abstract: Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected. The hardware monitor may be used by a formal verification tool to exhaustively verify that the firmware boot image does not comprise an illegal firmware instruction, or during simulation to detect illegal firmware instructions in a firmware boot image.
-
公开(公告)号:US20170364363A1
公开(公告)日:2017-12-21
申请号:US15340554
申请日:2016-11-01
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
CPC classification number: G06F9/3865 , G06F9/30145 , G06F9/3802 , G06F9/3861 , G06F9/3867 , G06F11/00
Abstract: Livelock recovery circuits configured to detect livelock in a processor, and cause the processor to transition to a known safe state when livelock is detected. The livelock recovery circuits include detection logic configured to detect that the processor is in livelock when the processor has illegally repeated an instruction; and transition logic configured to cause the processor to transition to a safe state when livelock has been detected by the detection logic.
-
43.
公开(公告)号:US09519611B2
公开(公告)日:2016-12-13
申请号:US14832087
申请日:2015-08-21
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari
CPC classification number: G06F9/466 , G06F5/00 , G06F11/0745 , G06F11/0751 , G06F11/079 , G06F11/28 , G06F11/30 , G06F13/36 , G06F13/4221
Abstract: Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design using a counter and an indexed table. The data structure includes a counter that keeps track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions using the counter; and control logic that verifies a transaction response has been received in the correct order (e.g. corresponds to the oldest in-flight transaction) based on the age information in the table.
Abstract translation: 提供了方法和硬件数据结构,用于使用计数器和索引表在多事务硬件设计中跟踪有序事务。 数据结构包括跟踪飞行中交易数量的计数器; 使用计数器跟踪每次飞行中交易的年龄的表格; 并且基于表中的年龄信息,以正确的顺序(例如对应于最早的机上交易)接收到验证交易响应的控制逻辑。
-
公开(公告)号:US20160210381A1
公开(公告)日:2016-07-21
申请号:US14920445
申请日:2015-10-22
Applicant: Imagination Technologies Limited
Inventor: Iain Singleton , Ashish Darbari , John Alexander Osborne Netterville
IPC: G06F17/50
CPC classification number: G06F13/364 , G06F13/1621 , G06F13/3625 , G06F13/4252 , G06F13/4256 , G06F17/5009 , G06F17/5022 , G06F17/5045
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.
Abstract translation: 验证硬件设计中仲裁器的操作。 仲裁器在多个时钟周期内接收多个请求,包括被监视的请求,并以优先顺序输出请求。 识别在每个时钟周期中由仲裁器接收和输出的请求。 然后,使用基于在每个时钟周期中输入到仲裁器并从仲裁器输出的请求而更新的计数器跟踪观察请求相对于仲裁器中的其他未决请求的优先级,以及识别由所述仲裁器接收的请求的相对优先级的掩码 仲裁者在同一个时钟周期。 使用断言来确认仲裁器的操作,该断言建立从仲裁器输出监视请求的计数器与时钟周期之间的关系。
-
公开(公告)号:US20240330553A1
公开(公告)日:2024-10-03
申请号:US18742457
申请日:2024-06-13
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F30/3323 , G06F9/30 , G06F9/38 , G06F11/07 , G06F11/30 , G06F30/33 , G06F30/333
CPC classification number: G06F30/3323 , G06F9/30145 , G06F9/3802 , G06F11/076 , G06F11/3055 , G06F30/33 , 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.
-
公开(公告)号:US12093621B2
公开(公告)日:2024-09-17
申请号:US18202929
申请日:2023-05-28
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F30/3323 , G06F11/07 , G06F11/34 , G06F30/39
CPC classification number: G06F30/3323 , G06F11/0754 , G06F11/3466 , 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.
-
公开(公告)号:US12050849B2
公开(公告)日:2024-07-30
申请号:US17749054
申请日:2022-05-19
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F30/3323 , G06F9/30 , G06F9/38 , G06F11/07 , G06F11/30 , G06F30/33 , G06F30/333
CPC classification number: G06F30/3323 , G06F9/30145 , G06F9/3802 , G06F11/076 , G06F11/3055 , G06F30/33 , 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.
-
公开(公告)号:US11989299B2
公开(公告)日:2024-05-21
申请号:US17158798
申请日:2021-01-26
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari
CPC classification number: G06F21/572 , G06F21/51 , G06F2221/033
Abstract: Described herein are hardware monitors arranged to detect illegal firmware instructions in a firmware binary image using a hardware design and one or more formal assertions. The hardware monitors include monitor and detection logic configured to detect when an instantiation of the hardware design has started and/or stopped execution of the firmware and to detect when the instantiation of the hardware design has decoded an illegal firmware instruction. The hardware monitors also include assertion evaluation logic configured to determine whether the firmware binary image comprises an illegal firmware instruction by evaluating one or more assertions that assert that if a stop of firmware execution has been detected, that a decode of an illegal firmware instruction has (or has not) been detected. The hardware monitor may be used by a formal verification tool to exhaustively verify that the firmware boot image does not comprise an illegal firmware instruction, or during simulation to detect illegal firmware instructions in a firmware boot image.
-
公开(公告)号:US20240020447A1
公开(公告)日:2024-01-18
申请号:US18202929
申请日:2023-05-28
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F30/3323 , G06F11/07 , G06F11/34 , G06F30/39
CPC classification number: G06F30/3323 , G06F11/0754 , G06F11/3466 , 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.
-
公开(公告)号:US20230205621A1
公开(公告)日:2023-06-29
申请号:US18114963
申请日:2023-02-27
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
CPC classification number: G06F11/0793 , G06F30/30 , G06F11/073 , G06F21/52 , G06F11/0736 , G06F11/0754 , G06F30/392
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.
-
-
-
-
-
-
-
-
-