https://github.com/rems-project/sail
Sail — это язык, созданный в Кембридже специально для описания процессоров
(на нем описаны ARM, RISC-V и x86).
Вы пишете императивный код (как в C), но компилятор Sail умеет автоматически:
- Генерировать из него C-код симулятора.
- Генерировать из него логические формулы (для Isabelle/HOL или Coq).
«Sail is a language for defining the instruction-set architecture (ISA) semantics of processors:
the architectural specification of the behaviour of machine instructions.»
Отредактировано Лис (2026-01-01 16:26:32)