RTL2M$\hat{I}¼$PATH: Multi-$\hat{I}¼$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 $\hat{I}¼$SPEC models. Despite…