公开(公告)号：EP4300348A1

公开(公告)日：2024-01-03

申请号：EP23182437.6

申请日：2023-06-29

申请人： Imagination Technologies Limited

发明人： Edmonds, Rachel ,  Elliott, Sam ,  Gaulter, Simon

IPC分类号： G06F30/3323 ,  G06F7/487 ,  G06F7/556 ,  G06F119/16

摘要： Methods of verifying a property of a hardware design for an integrated circuit to implement a product of power functions of the form x 0 t 0 × ... × x n t n , wherein t 0 ··· t n are fixed, rational numbers, x 0 ··· x n are floating point inputs, and n is an integer greater than, or equal to, one. The methods include: performing a first verification phase which comprises formally verifying that, for any first non-exception input set X = X 0 , ..., X n and any second non-exception input set Y = Y 0 , ... , Y n in an input space wherein corresponding inputs have a same mantissa and ( t 0 X 0 .exp + ··· + t n X n.exp ) - ( t 0 Y 0 .exp + ··· + t n Y n.exp ) is an integer, an instantiation of the hardware design generates outputs X' and Y' with a same mantissa and X' exp - ( t 0 X 0. exp + ··· + t n X n.exp ) = Y' exp - ( t 0 Y 0. exp + ··· + t n Y n.exp ); and performing a second verification phase which comprises verifying the property for the hardware design for a subset of input sets in the input space, the subset of input sets selected based on exponents sets wherein ( t 0 X 0 .exp + ··· + t n X n.exp ) - ( t 0 Y 0 .exp + ··· + t n Y n.exp ) is an integer. The notation "exp" denotes an exponent of an input or an output.

公开(公告)号：EP3882761A1

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

申请号：EP21161631.3

申请日：2021-03-09

申请人： Imagination Technologies Limited

发明人： Ferrere, Thomas ,  Gaulter, Simon ,  Nazar, Faizan ,  Elliott, Sam

IPC分类号： G06F7/24 ,  G06F30/3323

摘要： Methods and systems of verifying a hardware design for a sorter are disclosed. The methods include generating a modified version of the hardware design of the sorter accepting extended inputs and performing formal verification comprising: implementing a constraint that the least significant bits of each input in a set of extended inputs represent a unique value; and formally verifying aspects of the modified version of the hardware design of the sorter for the set of extended inputs.