Method and system for verifying a sorter

Patent metadata

Field	Value
Publication number	US-12314645-B2
Application number	US-202318377746-A
Country	US
Kind code	B2
Filing date	Oct 6, 2023
Priority date	Mar 19, 2020
Publication date	May 27, 2025
Grant date	May 27, 2025

Abstract

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.

First claim

What is claimed is:

1. A method of verifying a hardware design for a sorter, the sorter accepting base inputs each of a bit width m, the method comprising:
formally verifying the hardware design of the sorter accepting a set of base inputs each of a bit width m by formally verifying aspects of a modified version of the hardware design of the sorter accepting a set of extended inputs with a bit width m+q, where q is a positive integer, and the most significant m bits of each extended input is equal to m bits of a respective base input.

2. The method according to claim 1 , wherein the step of performing formal verification further comprises:
implementing a constraint that q least significant bits of each input in the set of extended inputs represent a unique value; and
wherein formally verifying aspects of the modified version of the hardware design of the sorter for the set of extended inputs comprises formally verifying that the most significant m bits of each sorted output of the modified version of the hardware design of the sorter are equal to a respective output obtained by an unmodified version of the hardware design of the sorter receiving the set of base inputs.

3. The method according to claim 1 , wherein the set of base inputs consists of n inputs, and q≥┌log 2 n┐.

4. The method according to claim 3 , wherein the q least significant bits of each input in the set of extended inputs represent a unique value from 0 to n−1.

5. The method according to claim 3 , wherein q≥n.

6. The method according to claim 5 , wherein the q least significant bits of each input in the set of extended inputs implement a unique one hot encoding.

7. The method according to claim 1 , wherein formally verifying aspects of the modified version of the hardware design of the sorter accepting the set of extended inputs comprises formally verifying set equality between the set of extended inputs and the set of outputs of the modified version of the hardware design of the sorter.

8. The method according to claim 7 , wherein formally verifying aspects of the modified version of the hardware design of the sorter accepting the set of extended inputs further comprises formally verifying ordering by either:
further formally verifying aspects of the modified version of the hardware design of the sorter for the set of extended inputs by formally verifying the ordering of the outputs of the modified version of the hardware design of the sorter; or
formally verifying the ordering of the outputs of unmodified version of the hardware design of the sorter.

9. The method according to claim 8 , wherein formally verifying the set equality comprises verifying that each of the outputs appears as an input and optionally formally verifying ordering comprises verifying that the outputs of the modified version of the hardware design of the sorter are in sequence and that neighbouring outputs are not equal.

10. The method according to claim 8 , wherein formally verifying the set equality comprises verifying that each of the inputs appears as an output and optionally formally verifying the ordering comprises verifying that the outputs of the modified version or unmodified version of the hardware design of the sorter are in sequence.

11. The method according to claim 1 , wherein formally verifying the hardware design of the sorter accepting the set of base inputs further comprises implementing a constraint that all the inputs in the set of base inputs are valid inputs for the unmodified version of the hardware design of the sorter, and that all the inputs in the set of extended inputs are valid inputs for the modified version of the hardware design of the sorter.

12. A method of manufacturing, using an integrated circuit manufacturing system, an integrated circuit comprising a sorter according to a hardware design for a sorter that has been verified according to claim 1 comprising inputting a computer readable dataset description of said integrated circuit to said integrated circuit manufacturing system.

13. A non-transitory computer readable storage medium having stored thereon computer readable code that causes the method as set forth in claim 1 to be performed when the code is run on at least one processor.

14. A system for verifying a hardware design a hardware design for a sorter, the sorter accepting base inputs each of a bit width m, the system comprising:
memory configured to store:
a formal verification tool; and

one or more processors configured to formally verify the hardware design of the sorter accepting base inputs each of a bit width m, using the formal verification tool, by:
formally verifying aspects of the modified version of the hardware design of the sorter accepting a set of extended inputs with a bit width m+q, where q is a positive integer and the most significant m bits of each extended input is equal to m bits of a respective base inputs.

15. The system according to claim 14 , wherein the one or more processors are configured to perform formal verification, using the formal verification tool, by further:
implementing a constraint that q 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 comprises formally verifying that the most significant m bits of each sorted output of the modified version of the hardware design of the sorter are equal to a respective output obtained by an unmodified version of the hardware design of the sorter receiving the set of base inputs.

16. The system according to claim 14 , wherein formally verifying aspects of the modified version of the hardware design of the sorter accepting the set of extended inputs further comprises formally verifying set equality between the set of extended inputs and the set of outputs of the modified version of the hardware design of the sorter.

17. The system according to claim 16 , wherein formally verifying aspects of the modified version of the hardware design of the sorter accepting the set of extended inputs further comprises formally verifying ordering by either:
further formally verifying aspects of the modified version of the hardware design of the sorter for the set of extended inputs by formally verifying the ordering of the outputs of the modified version of the hardware design of the sorter; or
formally verifying the ordering of the outputs of unmodified version of the hardware design of the sorter.

18. The system according to claim 17 , wherein formally verifying the set equality comprises verifying that each of the outputs appears as an input and optionally formally verifying the ordering comprises verifying that the outputs of the modified version of the hardware design of the sorter are in sequence and that neighbouring outputs are not equal.

19. The system according to claim 17 , wherein formally verifying the set equality comprises verifying that each of the inputs appears as an output and optionally formally verifying the ordering comprises verifying that the outputs of the modified version or unmodified version of the hardware design of the sorter are in sequence.

Assignees

• Imagination Tech Ltd

Inventors

• Gaulter Simon
• Ferrere Thomas
• Nazar Faizan
• Elliott Sam

Classifications

• G06F7/24 Primary

  Sorting, i.e. extracting data from one or more carriers, rearranging the data in numerical or other ordered sequence, and rerecording the sorted data on the original carrier or on a different carrier or set of carriers {sorting methods in general}(G06F7/36 takes precedence) · CPC title

• G06F30/3323 Primary

  using formal methods, e.g. equivalence checking or property checking · CPC title

• G06F30/33 Primary

  Design verification, e.g. functional simulation or model checking · CPC title