ARM Releases Machine Readable Architecture Specification
alastairreid.github.io
alastairreid.github.io
Arrrggghhhh!!!
and:
"I wrote an interpreter for ASL, added in an ELF loader and hey presto, I had a simulator for the ARMv8 architecture. (Not a very fast simulator but a simulator all the same.)
I wrote a transpiler for ASL that converts ASL to C, wrote another ELF loader and I had a faster simulator for the architecture. (Still not all that fast: I am sure you can do better!) I used that to let me run ARM’s internal architecture conformance test suite on the spec: getting the ISA to pass was a lot of work - but it was nothing compared with getting all those fiddly parts of the different privilege levels working.
I modified my interpreter to generate a symbolic representation of its actions then used a symbolic expression solver (aka an SMT solver) to generate test inputs that would make the ASL take different paths through the code for each different input. In other words, I wrote a test-case generator that could get very high branch coverage through the code. (Someday I should write about why I gave up on doing this.)"
Wow!
I would say I have a love-hate relationship with XML - your feelings seem to be less ambivalent. One good thing about XML is that you can convert it to HTML. Have a look at ISA_v82A_A64_xml_00bet3.1/xhtml/index.html (in the AArch64 tarball) - I find this to be the easiest way to navigate the ARM specs because I can follow hyperlinks inside the ASL code that take me to the function definitions. And keep going until I have read everything about what the ADD instruction does. Then I switch to the LDR instruction and I can chase down memory accesses and see code to handle big-endian configurations, unaligned accesses, page table walks, page fault handling, etc. Once you have used this, you will not go back to PDF.