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.