BACKGROUND

There are many functions which receive an input vector x comprising a plurality of input elements (x0, x1, . . . , xn−) and produce permutation related outputs for at least two different orderings (or permutations) of a set of input elements. A function is said to produce permutation related outputs if the function produces a first output in response to a first input vector, and produces a second output in response to a second input vector that is a permutation of the first input vector, and the second output can be deduced solely from the first output and the permutation. Such a function is referred to herein as a permutation respecting function. The set of input vector permutations for which a function is permutation respecting (i.e. produces permutation related outputs for an input vector and the permutation of the input vector) is referred to herein as the set or group of respected input vector permutations. Permutation respecting functions include, but are not limited to, functions F that are invariant with respect to one or more input vector permutations σ (i.e. F(σx)=F (x)); functions F that are equivariant with respect to one or more input vector permutations σ (i.e. σF(x)=F(σx)); and functions that satisfy t (x)=F(σx) wherein the input vector permutation σ is mapped to the output transformation tσby a homomorphism from the group of respected input vector permutations to the automorphism group of the outputs.

An example permutation respecting function is a sorting function Fsort(a,b,c) which receives an input vector comprising three input elements a, b, c and outputs a vector comprising the input elements in ascending order. This function is a permutation respecting function because it is invariant with respect to all input vector permutations—i.e. it will produce the same output for any permutation of a set of input elements. For example, the function Fsortwill output 4, 5, 6 when it receives input elements 4, 5 and 6 in any order. Specifically, the function Fsortwill output 4, 5, 6 when it receives (i) a=4, b=5 and c=6, (ii) a=4, b=6 and c=5; (iii) a=5, b=4, c=6; (iv) a=5, b=6 and c=4; (v) a=6, b=4, and c=5, or, (vi) a=6, b=5, and c=4. Examples of other permutation respecting functions include, but are not limited to, a mean function that outputs the mean of a plurality of input elements; a median function that outputs the median of a plurality of input elements; a maximum function that outputs the maximum of a plurality of input elements; a minimum function that outputs the minimum of a plurality of input elements; and a function that receives a set of input elements that represent the entries of a square matrix and outputs the determinant of that matrix.

Many electronic devices, such as systems-on-chips (SoCs), include a component that implements a permutation respecting function. Generating a component that implements a permutation respecting function typically includes developing a hardware design that describes the structure and function of an integrated circuit that implements the permutation respecting function; verifying or testing the hardware design to ensure that an integrated circuit manufactured according to the design will behave as expected; and once verified, manufacturing an integrated circuit, at an integrated circuit manufacturing system, in accordance with the hardware design. Verifying the operation, or behaviour, of a hardware design for a component that implements a permutation respecting function comprises verifying that an instantiation of the hardware design produces the correct (or expected) output, according to the function, for all valid input vectors.

A hardware design may be verified, for example, by formal verification or simulation-based verification. Formal verification is a systematic process that uses a mathematical model of the hardware design and mathematical reasoning to verify the hardware design. In contrast, simulation-based verification is a process in which a hardware design is tested by applying stimuli to an instantiation of the hardware design and monitoring the output of the instantiation of the hardware design in response to the stimuli.

Formal verification can improve controllability as compared to simulation-based verification. Low controllability occurs when the number of simulation test signals or vectors required to thoroughly simulate a hardware design becomes unmanageable. For example, a 32-bit comparator requires 264test vectors. This may take millions of years to verify exhaustively by simulation-based verification. By performing formal verification, the 32-bit comparator can be verified in less than a minute.

While formal verification can be an effective method for exhaustively verifying properties of a hardware design, this is only true if the properties that are to be verified are presented in such a manner that a formal verification tool can solve the mathematical problem presented thereby. Specifically, during formal verification of a hardware design the hardware design is represented as a mathematical model, the properties to be proved are also represented mathematically, and mathematical reasoning is used to determine if the properties are true for the hardware design based on the mathematical model. In other words, in formal verification the verification is presented as a mathematical problem to be solved. Some mathematical problems will be solvable within a reasonable amount of time by a formal verification tool whereas others will not. When a formal verification tool is able to solve the mathematical problem presented by the hardware design and the properties to be verified then the formal verification is said to converge. When, however, a formal verification tool is unable to solve the mathematical problem presented by the hardware design and the properties to be verified, then the formal verification does not converge, and no results are output, and the verification is inconclusive.

The embodiments described below are provided by way of example only and are not limiting of implementations which solve any or all of the disadvantages of known methods and systems for verifying hardware designs for components that implement a permutation respecting function.

SUMMARY

This summary is provided to introduce a selection of concepts that are further described below in the detailed description. This summary is not intended to identify key features or essential features of the claimed subject matter, nor is it intended to be used to limit the scope of the claimed subject matter.

Described herein are methods and systems for verifying a hardware design for a component that implements a permutation respecting function. The methods include formally verifying that an instantiation of the hardware design outputs the correct result to the function for a subset of valid input vectors; and formally verifying that an instantiation of the hardware design is permutation respecting for each of one or more input vector permutations (i.e. that an instantiation of the hardware design produces permutation related outputs for an input vector and the permutation of that input vector). The subset and the input vector permutations are selected so that any input vector that is not in the subset can be generated from an input vector in the subset via a combination of the one or more input vector permutations.

A first aspect provides a method of verifying a hardware design for a component that implements permutation respecting function, the component configured to receive an input vector comprising a plurality of input elements and generate an output based on the input vector and the function, the method comprising: verifying, at one or more processors, that an instantiation of the hardware design generates an expected output for each input vector of a subset of valid input vectors; and verifying, at the one or more processors, that, for each of one or more input vector permutations, an instantiation of the hardware design generates permutation related outputs for any input vector in a set of valid input vectors and the permutation of that input vector; wherein each valid input vector that is not in the subset of valid input vectors can be obtained by applying one or more of the one or more input vector permutations to an input vector in the subset.

A second aspect provides a system for verifying a hardware design for a component that implements permutation respecting function, the system comprising: memory comprising: the hardware design for a component that implements a permutation respecting function, the component configured to receive an input vector comprising a plurality of input elements and generate an output based on the input vector and the function; and one or more verification tools; and one or more processors configured to: verify, using one of the one or more verification tools, that an instantiation of the hardware design generates an expected output for each input vector of a subset of valid input vectors; and verify, using one of the one or more verification tools, that, for each of one or more input vector permutations, an instantiation of the hardware design generates permutation related outputs for any input vector in a set of valid input vectors and the permutation of that input vector; wherein each valid input vector that is not in the subset of valid input vectors can be obtained by applying one or more of the one or more input vector permutations to an input vector in the subset.

A hardware design for a component that implements a permutation respecting function, when processed in an integrated circuit manufacturing system, may configure the system to manufacture an integrated circuit embodying the component. There may be provided a non-transitory computer readable storage medium having stored thereon a hardware design for a component that implements a permutation respecting function that, when processed in an integrated circuit manufacturing system, causes the integrated circuit manufacturing system to manufacture an integrated circuit embodying the component.

There may be provided an integrated circuit manufacturing system comprising: a non-transitory computer readable storage medium having stored thereon a hardware design for a component that implements a permutation respecting function; a layout processing system configured to process the hardware design so as to generate a circuit layout description of an integrated circuit embodying the component; and an integrated circuit generation system configured to manufacture the integrated circuit embodying the component according to the circuit layout description.

There may be provided computer program code for performing a method as described herein. There may be provided non-transitory computer readable storage medium having stored thereon computer readable instructions that, when executed at a computer system, cause the computer system to perform the methods as described herein.

The above features may be combined as appropriate, as would be apparent to a skilled person, and may be combined with any of the aspects of the examples described herein.

