Unpacking Challenges from the POWER ISA: Why I'm Exploring RISC-V's Formal Models

In the POWER Instruction Set Architecture (ISA), the Machine State Register's Hypervisor bit (MSR_HV) and the most significant bit of the Effective Address (EA_0) play crucial roles in address translation:

When MSR_HV == 1:

• If EA_0 == 0, the Hypervisor Offset Real Mode Address mechanism (as described in Section 5.7.3.1 of the POWER ISA) controls the access.
• If EA_0 == 1, bits 4:63 of the effective address are used as the real address for the access.

It's important to note that in the POWER ISA, the 0 index refers to the most significant bit. Therefore, when storing to an address whose most significant bit is high (i.e., EA_0 == 1) and MSR_HV == 1, an offset from the Hypervisor Real Mode Offset Register (HRMOR) is applied to the real address. This means that the address used in real mode can affect the translation mode.

Initially, I found this design choice questionable, as I believed that conditions affecting address translation modes should be independent of the address presented to the load-store unit. I also thought that such behavior would be easier to manage if the POWER ISA had a formal ISA model. This led me to explore the formal models for RISC-V, specifically the Haskell and SAIL models.

I hope to discuss working with SAIL in more detail in future posts.