RTL2M$\mu$PATH: Multi-$\mu$PATH Synthesis with Applications to Hardware Security Verification

Yao Hsiao, Nikos Nikoleris, Artem Khyzha +4

The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $\mu$SPEC models. Despite…