When I worked at a large US-Based CPU company about 10 years ago I was always wondering why we didn't have a tool like this. Instead the ISA semantics were desc

When I worked at a large US-Based CPU company about 10 years ago I was always wondering why we didn't have a tool like this. Instead the ISA semantics were described in multiple word docs. Everything was mostly* manually created from those docs - it was fraught with the possibility of error. I did hear from someone who had worked at the same company in the 90s that they had had a tool akin to Sail back then that was based on an ML language (Oh, and it seems Sail is written in OCaml!) - it seems like Nirvana had been achieved then, but then paradise was lost by the time I was working there. *'mostly' because there was a research group that was working on tools that would read the word docs and do some automation, though they seemed mostly still experimental... and it also seemed like a really bad way to approach the problem, but they were working with what the designers were used to - Word Docs.