US 11,948,652 B2
Formal verification tool to verify hardware design of memory unit
Ashish Darbari, Abbots Langley (GB); and Iain Singleton, Hemel Hempstead (GB)
Assigned to Imagination Technologies Limited, Kings Langley (GB)
Filed by Imagination Technologies Limited, Kings Langley (GB)
Filed on Jan. 11, 2022, as Appl. No. 17/573,542.
Application 17/573,542 is a continuation of application No. 16/792,582, filed on Feb. 17, 2020, granted, now 11,250,927.
Application 16/792,582 is a continuation of application No. 15/340,726, filed on Nov. 1, 2016, granted, now 10,580,511, issued on Mar. 3, 2020.
Claims priority of application No. 1519890 (GB), filed on Nov. 11, 2015.
Prior Publication US 2022/0139480 A1, May 5, 2022
This patent is subject to a terminal disclaimer.
Int. Cl. G11C 29/38 (2006.01); G06F 11/22 (2006.01); G06F 11/30 (2006.01); G06F 11/34 (2006.01); G11C 29/12 (2006.01); G11C 29/44 (2006.01); G11C 29/04 (2006.01)
CPC G11C 29/38 (2013.01) [G06F 11/2221 (2013.01); G06F 11/3037 (2013.01); G06F 11/3409 (2013.01); G11C 29/1201 (2013.01); G11C 29/44 (2013.01); G11C 2029/0409 (2013.01)] 20 Claims
OG exemplary drawing
 
14. A method of verifying operation of an instantiation of a hardware unit for storing data defined by a hardware design, the method comprising:
verifying operation of the instantiation of the hardware unit, using a formal verification tool, by verifying a formal assertion that establishes that when a read of a symbolic address of the instantiation of the hardware unit occurs after one or more writes to the symbolic address, read data corresponding to the read of the symbolic address matches write data corresponding to the one or more writes to the symbolic address, wherein the symbolic address is a variable that represents each possible address value of the instantiation of the hardware unit which causes the formal verification tool to assess each of the possible address values.