Verifying Clock/Reset Domain Crossings (CDC/RDCs) comprehensively is one of the key requirements for multi-clock/reset designs. Manual reviews and design-property based dispositioning of CDC/RDC results from RTL analyses need be backed up by a comprehensive verification of assumptions. Additionally, the design has to be verified to ensure correct functional operation even in the presence of metastability in the CDC/RDC paths. In this paper, we present strategies for CDC/RDC signoff using formal checks to verify design assumptions and the impact of metastability, with relevant simulation linkages where needed. We share results from real design scenarios using the Cadence JasperGoldĀ® CDC verification solution.