35 ms·

Can it model an ISA like the Mill?

sanxiyn 6y ago
I don't know, but that's not the goal. REMS stands for Rigorous Engineering of Mainstream Systems. Mill is not a mainstream system.
monocasa 6y ago
Yeah, at it's core, Sail is an RTL. It shouldn't have a problem with the Mill, but it probably isn't the most ergonomic arch for Sail.
- GregarianChild 6y ago
  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. [1] https://en.wikipedia.org/wiki/Register-transfer_level https://en.wikipedia.org/wiki/Register-transfer_level [2] https://alastairreid.github.io/ARM-v8a-xml-release/ https://alastairreid.github.io/ARM-v8a-xml-release/ [3] https://en.wikipedia.org/wiki/Verilog https://en.wikipedia.org/wiki/Verilog
  - monocasa 6y ago
    There are RTLs that aren't HDLs. For instance one of GCCs intermediate representations really reminds me of Sail. https://gcc.gnu.org/onlinedocs/gccint/RTL.html https://gcc.gnu.org/onlinedocs/gccint/RTL.html
    - GregarianChild 6y ago
      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.

I don't know, but that's not the goal. REMS stands for Rigorous Engineering of Mainstream Systems. Mill is not a mainstream system.

monocasa 6y ago

Yeah, at it's core, Sail is an RTL. It shouldn't have a problem with the Mill, but it probably isn't the most ergonomic arch for Sail.

GregarianChild 6y ago
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. [1] https://en.wikipedia.org/wiki/Register-transfer_level https://en.wikipedia.org/wiki/Register-transfer_level [2] https://alastairreid.github.io/ARM-v8a-xml-release/ https://alastairreid.github.io/ARM-v8a-xml-release/ [3] https://en.wikipedia.org/wiki/Verilog https://en.wikipedia.org/wiki/Verilog
- monocasa 6y ago
  There are RTLs that aren't HDLs. For instance one of GCCs intermediate representations really reminds me of Sail. https://gcc.gnu.org/onlinedocs/gccint/RTL.html https://gcc.gnu.org/onlinedocs/gccint/RTL.html
  - GregarianChild 6y ago
    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.