Hardware-software (HW-SW) contracts beyond traditional instruction set architecture, such as memory consistency model, are useful only if the underlying hardware complies with them (microarchitectural compliance). Standard top-down hardware MCM verification is manual and non-scalable. Our recent work proposes a bottom-up approach, called rtl2$\mu$spec, by synthesizing an axiomatic model of MCM implementation directly from SystemVerilog design using a combination of static analysis of netlist, property generation, and model checking. The synthesized axiomatic model is proven correct by construction and can be input to existing formal MCM verification flows. This bottom-up approach achieves better efficiency and scalability over the prior work as demonstrated in a case study on a four-core RISC-V multi-V-scale processor, which implements sequential consistency. In this work, we aim to conduct MCM verification on advanced processor designs. This requires 1) scaling rtl2$\mu$spec to support input design with features such as out-of-order execution, speculation, caches, and so on, and 2) developing novel design-for-verification (DFV) that addresses the model-checker limitation. In this talk, we will discuss the challenges in doing both and the steps we have taken toward solving some of the challenges.