-
公开(公告)号:US20200185051A1
公开(公告)日:2020-06-11
申请号:US16792582
申请日:2020-02-17
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
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.
-
公开(公告)号:US10552155B2
公开(公告)日:2020-02-04
申请号:US15340554
申请日:2016-11-01
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
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.
-
公开(公告)号:US10346571B2
公开(公告)日:2019-07-09
申请号:US15340638
申请日:2016-11-01
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
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.
-
公开(公告)号:US20180107765A1
公开(公告)日:2018-04-19
申请号:US15784353
申请日:2017-10-16
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F17/50
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.
-
公开(公告)号:US20170344668A1
公开(公告)日:2017-11-30
申请号:US15340450
申请日:2016-11-01
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Iain Singleton
IPC: G06F17/50
CPC classification number: G06F17/504 , G06F11/3024 , G06F11/3409 , G06F11/3466 , G06F11/3608 , G06F11/3616 , G06F11/3636 , G06F11/3648 , G06F11/3652 , G06F17/5045 , G06F2217/12
Abstract: A hardware monitor arranged to assess performance of a hardware design for an integrated circuit to complete a task. The hardware monitor includes monitoring and counting logic configured to count a number of cycles between start and completion of the symbolic task in an instantiation of the hardware design; and property evaluation logic configured to evaluate one or more formal properties related to the counted number of cycles to assess the performance of the instantiation of the hardware design in completing the symbolic task. The hardware monitor may be used by a formal verification tool to exhaustively verify that the hardware design meets a desired performance goal and/or to exhaustively identify a performance metric (e.g. best case and/or worst case performance) with respect to completion of the task.
-
公开(公告)号:US09767057B2
公开(公告)日:2017-09-19
申请号:US14832526
申请日:2015-08-21
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari
CPC classification number: G06F13/364 , G06F5/00 , G06F9/467 , G06F11/28 , G06F11/30 , G06F13/36 , G06F13/4282
Abstract: Methods and hardware data structures are provided for tracking ordered transactions in a multi-transactional hardware design comprising one or more slaves configured to receive transaction requests from a plurality of masters. The data structure includes one or more counters for keeping track of the number of in-flight transactions; a table that keeps track of the age of each of the in-flight transactions for each master using the one or more counters; and control logic that verifies that a transaction response for an in-flight transaction for a particular master has been issued by the slave in a predetermined order based on the tracked age for the in-flight transaction in the table.
-
公开(公告)号:US20170205864A1
公开(公告)日:2017-07-20
申请号:US15351644
申请日:2016-11-15
Applicant: Imagination Technologies Limited
Inventor: Iain Singleton , John Alexander Osborne Netterville , Ashish Darbari
CPC classification number: G06F1/28 , G06F1/12 , G06F1/3243 , G06F17/504 , G06F17/5045 , G06F2217/78 , Y02D10/152
Abstract: Methods, systems and hardware monitors for verifying that an integrated circuit defined by a hardware design meets a power requirement including detecting whether a power consuming transition has occurred for one or more flip-flops of an instantiation of the hardware design; in response to detecting that a power consuming transition has occurred, updating a count of power consuming transitions for the instantiation of the hardware design; and determining, whether the power requirement is met at a particular point in time by evaluating one or more properties that are based on the count of power consuming transitions.
-
公开(公告)号:US20170177753A9
公开(公告)日:2017-06-22
申请号:US14674651
申请日:2015-03-31
Applicant: Imagination Technologies Limited
Inventor: Ashish Darbari , Colin McKellar
IPC: G06F17/50
CPC classification number: G06F17/5009 , G06F9/524 , G06F11/3608 , G06F17/5022 , G06F17/504 , G06F17/5045 , G06F17/505 , G06F2217/06
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.
-
公开(公告)号:US20170177521A1
公开(公告)日:2017-06-22
申请号:US15454100
申请日:2017-03-09
Applicant: Imagination Technologies Limited
Inventor: Iain Singleton , Ashish Darbari , John Alexander Osborne Netterville
IPC: G06F13/364 , G06F13/362 , G06F13/42 , G06F13/16
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.
-
公开(公告)号:US09626465B2
公开(公告)日:2017-04-18
申请号: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.
-
-
-
-
-
-
-
-
-