Closed avpatel closed 5 years ago
I agree that pseudo-code specification style would be an improvement. Given the existence of the formal modeling effort, would direct reference to an "official" complete formal model, either the source or possibly some generated presentation thereof, be suitable?
I made a very quick search for equivalents to your first blurb in the source of formal models that implement traps:
The plan is for the formal models to address this need, rather than including this kind of thing in the English spec.
Well, IMhO it belong in the spec and it should have been written like this from the beginning. There are a lot of ambiguity in the English prose that shows up again and again. Rather than waiting for the perfect four formal specs, I'd much rather see us incrementally move to a more explicit spec and have the formal spec be complementary.
FWIW, I don't think the formal spec serves exactly the same purpose. The formal specs come with their own formalism that require a new level of interpretation whereas Anup's style is somewhere between the freewheeling english prose and a machine comprehensible formal spec.
Tommy
On Mon, Apr 8, 2019 at 9:54 AM Andrew Waterman notifications@github.com wrote:
The plan is for the formal models to address this need, rather than including this kind of thing in the English spec.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/riscv/riscv-isa-manual/issues/364#issuecomment-480913415, or mute the thread https://github.com/notifications/unsubscribe-auth/AA0pmKhgXxxBe9mdjB7fOAlzs0akkO3Gks5ve3RXgaJpZM4chkgP .
The set of pseudocodes in RISC-V spec don't need to be very detailed like the formal spec but it should give high-level idea about the sequence of HW state changes for functional correctness.
The formal spec will be used to document this exactly, and is designed to be human-readable.
It will be very helpful to HW designers, simulator/emulator developers, and hypervisor developers if we have a separate section in RISC-V privilege spec providing reference pseudo-codes for complex HW events such as trap and trap return.
These reference pseudo-code will show a order/sequence for HW-state change when a complex HW event such as trap or trap return happens. Of course, HW designers can do things differently to optimize as long as end-result is same.
Here are few reference pseudo-codes which I came-up with based on my limited understanding...
PC == Current program counter MODE == Current mode (M/HS/U/VS/VU) V == Current virtualization state (1 == inside VM and 0 == not inside VM)
Trap taken into M-mode (M/HS/U/VS/VU ==> M)
Trap return from M-mode using MRET (M ==> M/HS/U/VS/VU)
Trap taken into HS-mode (VS/VU/HS/U ==> HS)
Trap return from HS-mode using SRET (HS ==> VS/VU/HS/U)
Trap taken into VS-mode (VS/VU ==> VS)
Trap return from VS-mode using SRET (VS ==> VS/VU)