This thesis presents a methodology for the formal verification of memory organizations in System-on-Chip (SoC) designs described in IP-XACT. The approach involves modeling the address map structures of the design's IP-XACT description and its spreadsheet-based global address map specification into a unified graph model we developed, called an Address Map Graph (AMG). Additionally, it introduces an analysis of AMGs to determine the equivalence of their mapped addresses, called Graph Bitmapping Equivalence (GBE). The methodology was implemented through a series of modular programs integrated into a solution flow. These programs process the spreadsheet memory specifications and IP-XACT design representations into AMGs and perform efficient GBE calculation and detailed reporting. The solution was evaluated using a state-of-the-art mid-size SoC design as a case study. Verification of results was performed using commercially available design analysis tools. The results demonstrated the developed solution was effective to analyze and verify the memory organization of complex SoC designs and to assist in identifying the causes of discrepancies.