Hardware Monitor to Verify Memory Units
First Claim
1. A hardware monitor configured to verify operation of an instantiation of a memory unit defined in a hardware design, the hardware monitor comprising:
- detection logic configured to monitor one or more control signals of the instantiation of the memory unit to detect writes to a symbolic address of the instantiation of the memory unit and reads of the symbolic address of the instantiation of the memory unit, wherein the symbolic address is a variable that represents each possible address value of the instantiation of the memory unit which causes a formal verification tool to assess each of the possible address values; and
assertion verification logic configured to verify a formal assertion that establishes that when the detection logic detects a read of the symbolic address that 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.
2 Assignments
0 Petitions
Accused Products
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.
-
Citations
20 Claims
-
1. A hardware monitor configured to verify operation of an instantiation of a memory unit defined in a hardware design, the hardware monitor comprising:
-
detection logic configured to monitor one or more control signals of the instantiation of the memory unit to detect writes to a symbolic address of the instantiation of the memory unit and reads of the symbolic address of the instantiation of the memory unit, wherein the symbolic address is a variable that represents each possible address value of the instantiation of the memory unit which causes a formal verification tool to assess each of the possible address values; and assertion verification logic configured to verify a formal assertion that establishes that when the detection logic detects a read of the symbolic address that 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 19)
-
-
16. The test system of claim 16, further comprising a configuration application program interface configured to identify the one or more control signals of the memory unit to be monitored by the detection logic based on a type of the memory unit, a configuration of the memory unit or both the type of the memory unit and the configuration of the memory unit.
-
17. A method of verifying operation of an instantiation of a memory unit defined by a hardware design, the method comprising:
-
monitoring, using detection logic, one or more control signals of the instantiation of the memory unit to detect writes to a symbolic address of the instantiation of the memory unit, wherein the symbolic address is a variable that represents each possible address value of the instantiation of the memory unit which causes a formal verification tool to assess each of the possible address values; monitoring, using detection logic, one or more control signals of the instantiation of the memory unit to detect reads of the symbolic address of the instantiation of the memory unit; and verifying operation of the instantiation of the memory unit, using assertion verification logic, by verifying a formal assertion that establishes that when a read of the symbolic address 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. - View Dependent Claims (18)
-
-
20. A hardware monitor configured to verify a hardware design which defines operation of a unit in a computing system, the hardware monitor comprising:
-
detection logic configured to monitor one or more control signals of an instantiation of the unit to detect indications of the operation of the instantiation of the unit; and assertion verification logic configured to verify the hardware design by verifying an assertion that the detection logic detects indications which are indicative of correct operation of the instantiation of the unit.
-
Specification