Search for a command to run...
High bandwidth memory (HBM) comprises three dimensional vertically stacked DRAM memory interfaces integrated within CPU or GPU chips. It is directly connected to the memory controller logic via an interposer, facilitating communication between HBM stacks and the main die through various independent channels responsible for transmitting data and other signals. Each stack consists of multiple layers of DRAM, interconnected vertically using Through Silicon vias (TSV). Address hashing is a technique that modifies memory addresses to spread them more evenly across hardware components like cache sets or memory banks. This helps prevent performance issues caused by many addresses following similar, predictable patterns. These complex interconnections enable the transfer of numerous signals, enhancing performance but complicating verification. The intricate architecture of HBM necessitates precise manufacturing, as defective layers within the stacks can jeopardize integrity. To mitigate this risk, a harvesting feature is implemented, allowing for rerouting to adjacent DRAM layers in the event of a defect. Furthermore, the complexity of verifying multiple stacks, combined with harvesting, underscores the importance of exhaustive testing to assess all potential defect combinations and to ensure that memory requests are successfully transmitted without loss. In this paper, we illustrate how we effectively verify this design using formal verification(FV) methodologies (Formal Property Verification(FPV), Connectivity Check (CC)) and a checker-based simulation method. We complement formal with a functional verification (simulation based) integrated checker, that reproduces the hashing logic, tracks per-channel queues with latency tolerance, and validates routing across modes and harvesting configurations. This dynamic method catches spec-to-RTL drifts and corner cases under stress and fault injection, enabling fast iteration and high functional coverage with practical regression effort.