[thechao]

I really think something like Ghidra/SLEIGH and a formal specification of the p-code could help; but, only if the following things happened:

1. A p-code parser front end in C existed;

2. An alternate XML/JSON version of SLEIGH; and,

3. A way to integrate the above to document (book) generation.

For the latter I'd prefer HTML. I've found the SLEIGH spec, itself, heavy enough going that I can't tell if it supports full constraint specifications, or not.

[IAmLiterallyAB]

> full constraint specifications

Is that a technical term? (if so, can you explain further)

I've made SLEIGH specs for two architectures. In my experience, it can describe 95% of the semantics well enough for decompilation (it gets weird when your ISA has quirks). Not as comprehensive as SAIL appears to be

Also, SLEIGH compiles to an XML format which is what Ghidra actually uses

[thechao]

CPUs are fairly orthogonal in terms of capabilities; if the instruction can encode it, the CPU can interpret it. Coprocessors (GPUs, NPUs, etc.) have ISA where the legal encoding space is much larger than a the legal instruction space: the set of valid instructions is not dense in its own encoding space. This smaller legal space is defined by a set of constraints on the set of legal encodings.