I wonder whether you could use Sail to make a compiler that figures out how to compile things. Then you could re-target it just by giving it a description of the new processor instead of a description of the old one.
There's work along these lines (substantially predating Sail, but one could in principle do much the same starting from Sail specs) by Dias and Ramsey, e.g. the POPL 2010 and 2011 papers at https://www.cs.tufts.edu/~nr/
If you don't care about compiler
performance, auto-generating a compiler backend from scratch is
already highly non-trivial. Sail's constrained nature may help a
little but not that much, as you essentially need to auto-understand
an interpreter for a Turing-complete language. If you do want
performance, the problem becomes much harder still. One of the biggest
problems in compiler performance is the memory model: what reordering
is permitted, what is prohibited to the optimiser? Sail does not address this. Instead, (like all similar
languages) it 'handles' main memory access by two uninterpreted functions which are
(roughly) "memory read" and "memory write" That's a polite way of
saying: Sail (like all similar languages) leaves this particular problem to the user.
If you get the compiler backend generated then that same description language could also provide optimization hints. If you look at the RISC-V spec a lot is left up to the implementation but certain optimizations leave e.g. instructions available for cache management and this would have to be exposed in the ISA description.
Save Intel's compiler, do any rely on implementation details? They rely on cache and fetch details, but only in broad, nebulous ways that seem very portable.
There may be open research questions but it seems to me the biggest thing is paying someone to do it.
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.
Curiously, not the first with this name in the hardware description space. SAIL (all caps), the Stanford AI Language, was an Algol flavored beast from the 70s. VLSI Technology (eaten by Philips) used it for internal CAD tools like place and route, layout, etc. in the 90s. They liked it so much they had an internal tools group maintaining it, along with very heavy use of ClearCase.
Sail is not at the register-transfer level (RTL) [1].
Why? Because
Sail does not offer abstractions for clocked digital circuits, which is what characterises the RTL. The most widely used DSL for the RTL is (System)Verilog [3].
Instead, Sail is a stand-alone DSL for the ISA (= instruction set architecture). The purpose of the ISA level is to talk about that a processor looks from the outside, to the programmer (most specifically to the compiler writer). Sail is a minimal programming language with a single purpose: writing ISA specifications, which means writing an interpreter for assembly language.
Technically, Sail is a simple imperative language with first-order functions. What makes Sail suitable for specifying ISAs is its typing system. Sail supports
types that are frequently used in ISA interpreters, such as dependent typing for numeric types and bitvector lengths. Sail is closely related to Arm's ASL (= architecture specification language) [2].
Since Sail is Turing-complete, any ISA can be modelled, including Mill. For the same reason any RTL can be modelled, for example by coding up an interpreter for an RTL language like Verilog, but that would be mighty inconvenient.
I see now where the confusion comes from: the abbreviation RTL is overloaded to (1) register-transfer level (as e.g. Verilog) and (2) register-transfer language (e.g. GCCs intermediate representation you cited). I think the former use is much more widespread. I agree GCC's register-transfer language is close to Sail.
