이 저장소에는 항해로 작성된 RISC-V 아키텍처의 공식 사양이 포함되어 있습니다. RISC-V 재단에 의해 채택되었습니다.
이 모델은 지침의 어셈블리 언어 형식, 해당 인코더 및 디코더 및 명령 의미를 지정합니다. 모델에 대한 읽기 안내서는 Doc/ Subdirectory에서 모델을 확장하는 방법에 대한 안내서와 함께 제공됩니다.
라텍스 또는 asciidoc 정의는 참조 문서에 포함하기에 적합한 모델에서 생성 될 수 있습니다. RISC-V에 대한 최신 SAIL ASCIIDOCTOR 문서 지원도 있습니다.
SAIL은 프로세서의 ISA (Instruction-Set Architecture) 시맨틱을 설명하는 언어 : 기계 지침의 행동의 아키텍처 사양입니다. SAIL은 이전 공급 업체 유사 코드와 마찬가지로 엔지니어 친화적 인 언어이지만보다 정확하게 정의되고 광범위한 사용 사례를 지원하기위한 툴링을 사용합니다.
돛 사양이 주어지면 도구는 유형을 확인하고 문서 스 니펫 (라텍스 또는 ASCIIDOC에서)을 생성하고 실행 가능한 에뮬레이터를 생성하고 사양 범위를 표시하며 편안한 메모리 모델 도구를위한 ISA 버전을 생성하고 자동 지침 시퀀스 테스트 생성을 지원할 수 있습니다. 대화 형 증명 (Isabelle, Hol4 및 CoQ)에 대한 정리 전단 정의를 생성하고, 이진 코드 (Islaris)에 대한 증거를 지원하며 (진행 중) 공식 하드웨어 검증에 사용할 수있는 SystemVerilog에서 참조 ISA 모델을 생성합니다.
SAIL은 ARM-A의 순차적 동작 (권위있는 ARM- 내부 사양에서 자동으로 파생 된 ARM의 허가를받은 BSD 클리어 라이센스에 따라 릴리스), RISC-V, Cheri-를 포함하여 여러 ISA 설명에 사용됩니다. RISC-V, Cheriot, MIPS 및 Cheri-MIPS; 이 모든 것이 다양한 운영 체제를 부팅하기에 충분히 완성됩니다. ACL2 X86 모델의 버전을 포함하여 IBM Power 및 X86의 작은 조각에 대한 항해 모델도 있습니다.
항해를 설치하십시오. Linux에서는 이진 릴리스를 다운로드하거나 (강력하게 권장) OPAM을 사용하여 소스에서 설치할 수 있습니다. 그 다음에:
$ make
c_emulator/riscv_sim_RV64 에서 시뮬레이터를 구축합니다.
sail: unknown option '--require-version'. 항해 컴파일러가 너무 오래 되었기 때문입니다. 버전 0.18 이상이 필요합니다.
make 라인에 ARCH=RV32 또는 ARCH=RV64 지정하고 일치하는 대상 접미사를 사용하여 RV32 또는 RV64 모델을 빌드 할 수 있습니다. RV64는 기본적으로 구축되었지만 RV32 모델은 다음을 사용하여 구축 할 수 있습니다.
$ ARCH=RV32 make
c_emulator/riscv_sim_RV32 에서 시뮬레이터를 만듭니다.
MakeFile은 riscv_isa_build , riscv_coq_build 및 riscv_hol_build 대상으로합니다. 각 속담을 발산하여 정의를 처리하고 generated_definitions/isabelle/RV64/Riscv.thy 에서 generated_definitions/coq/RV64/riscv.v , rucv.v. generated_definitions/hol4/RV64/riscvScript.sml 의 모델. 우리는 Isabelle 2018, CoQ 8.8.1 및 Hol4 Kananaskis-12를 테스트했습니다. 이러한 대상을 구축 할 때는 SAIL 디렉토리 ( $SAIL_DIR/lib/$prover )의 해당 프로버 라이브러리가 해당 디렉토리에서 make 실행하여 최신 및 구축되어 있는지 확인하십시오.
시뮬레이터를 사용하여 소규모 테스트 바이너리를 실행할 수 있습니다.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
riscv-tests 에서 파생 된 RV32 및 RV64 테스트 프로그램은 테스트/RISCV- 테스트/에 포함됩니다. test/run_tests.sh 사용하여 테스트 스위트를 실행할 수 있습니다.
시뮬레이터의 구성 옵션에 대한 정보는 ./c_emulator/riscv_sim_<arch> -h 에서 제공됩니다.
유용한 옵션은 다음과 같습니다. 잘못 정렬 된 액세스에 대한 액세스 여부 ( --enable-misaligned )와 페이지 테이블 워크가 PTE 비트 ( --enable-dirty-update )를 업데이트하는지 여부를 구성합니다.
운영 체제 이미지를 부팅하려면 OS-Boot/ Subdirectory의 정보를 참조하십시오.
드물게 항해의 릴리스 버전은 귀하의 요구를 충족시키지 못할 수 있습니다. 릴리스 된 SAIL 버전에 아직 버그 수정 또는 새로운 기능이 필요하거나 항해를 적극적으로 작업하는 경우 발생할 수 있습니다. 이 경우 sail-riscv Makefile SAIL_DIR 를 make 호출 할 때 Sail repo의 근본 원인으로 설정하여 Sail_dir의 로컬 사본을 사용하도록 지시 할 수 있습니다. 또는 SAIL 설치 지침에 설명 된대로 opam pin 사용하여 항해 핀의 로컬 체크 아웃에서 항해를 설치할 수 있습니다.
이들은 기본 지침이 포함 된 모델 파일의 발췌문 인 RISCV_INSTS_BASE.SAIL을 포함하여 몇 가지 의견이 추가되었습니다.
/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
/* the encode/decode mapping between AST elements and 32-bit words */
mapping encdec_iop : iop <-> bits(3) = {
RISCV_ADDI <-> 0b000,
RISCV_SLTI <-> 0b010,
RISCV_SLTIU <-> 0b011,
RISCV_ANDI <-> 0b111,
RISCV_ORI <-> 0b110,
RISCV_XORI <-> 0b100
}
mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
/* the execution semantics for the ITYPE instructions */
function clause execute (ITYPE (imm, rs1, rd, op)) = {
let rs1_val = X(rs1);
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
};
X(rd) = result;
RETIRE_SUCCESS
}
/* the assembly/disassembly mapping between AST elements and strings */
mapping itype_mnemonic : iop <-> string = {
RISCV_ADDI <-> "addi",
RISCV_SLTI <-> "slti",
RISCV_SLTIU <-> "sltiu",
RISCV_XORI <-> "xori",
RISCV_ORI <-> "ori",
RISCV_ANDI <-> "andi"
}
mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
union clause ast = SRET : unit
mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
Machine => not(extensionEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
else if not(ext_check_xret_priv (Supervisor))
then { ext_fail_xret_priv(); RETIRE_FAIL }
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
}
}
mapping clause assembly = SRET() <-> "sret"
이 모델은 RISC-V ELF 파일을 실행할 수있는 C 에뮬레이터를 구축하고 두 에뮬레이터는 Linux, FreeBSD 및 SEL4를 부팅하기에 충분한 플랫폼 지원을 제공합니다. C 에뮬레이터는 스파이크 에뮬레이터와 연결하여 비 지적 탠덤 검증으로 실행할 수 있습니다.
L Linux Boot의 C Emulator는 현재 Intel i7-7700에서 약 300 개의 킬로그램으로 실행되고 있습니다 (세부 간주 추적 추적이 비활성화 될 때). 향후 최적화를위한 많은 기회가 있습니다 (Sail MIPS 모델은 대략 1 MIPS에서 실행됩니다. ). 이를 통해 약 4 분 안에 Linux를 부팅하고 약 2 분 안에 FreeBsd를 부팅 할 수 있습니다. Linux를 부팅 할 때 C 에뮬레이터의 메모리 사용량은 약 140MB입니다.
C Emulator 디렉토리의 파일은 ELF로드 및 플랫폼 장치를 구현하고 물리적 메모리 맵을 정의하며 명령 줄 옵션을 사용하여 구현 별 ISA 선택을 선택합니다.
돛 생성 C 에뮬레이터는 실행 된 테스트의 사양 지부 범위를 측정하여 결과를 파일 당 테이블 및 HTML- 공개 버전의 모델 소스로 표시 할 수 있습니다.
임의의 명령 스트림의 탠덤 검증을 위해, 도구는 테스트 리그에 사용 된 프로토콜을 지원하여 C 에뮬레이터에 명령을 직접 주입하고 RVFI 형식으로 추적 정보를 생성합니다. 이것은 Spike에 대한 교차 테스트 및 Bluespec SystemVerilog에 작성된 RVBS 사양에 사용되었습니다.
C 에뮬레이터는 Spike에 직접 연결될 수 있으며, 이는 ELF Binaries (OS 부츠 포함)에 대한 탠덤 검증을 제공합니다. 이는 부팅이 스파이크에서 작동하는 것으로 알려진 모델에서 OS 부팅 문제를 디버깅하는 데 유용합니다. 또한 ISA 사양에 의해 의무화되지 않은 스파이크에서 플랫폼 별 구현 선택을 감지하는 것이 유용합니다.
ISA 모델은 RISC 개발에 사용되는 기준 모델 중 하나 인 RISC-V 완화 메모리 모델 인 RVWMO (RISC-V 사용자 수준 사양의 부록에 설명 된대로)와 통합되어 있습니다. -V 동시성 아키텍처; 이것은 RMEM 도구의 일부입니다. 또한 ISLA-AXIOMATIC 도구의 일부로 RISC-V 공리 동시성 모델과 통합됩니다.
캠브리지 대학/ 인리아 동맹 아키텍처 작업의 일환 으로이 그룹은 약 7000 개의 리트머스 테스트 라이브러리를 제작하고 발표했습니다. 운영 및 공리적 RISC-V 동시성 모델은 이러한 테스트와 동기화되며 공통 테스트에 해당하는 ARM 아키텍처 동작에 동의합니다.
이러한 테스트는 RISC-V 하드웨어에서, Sifive RISC-V FU540 Multicore Proto Board (Freedom Unleashed)에서 Imperas의 대출에 대해 실행되었습니다. 현재까지 순차적으로 일관된 행동 만 관찰되었습니다.
Sail은 여러 도구에서 관용 정리 속담의 생성을 지원하는 것을 목표로합니다. 현재 Isabelle, Hol4 및 CoQ를 지원하며 prover_snapshots 디렉토리는 생성 된 정리 서프로우 정의의 스냅 샷을 제공합니다.
이러한 정리를 추적하는 번역은 다른 목적을 위해 여러 모나드를 대상으로 할 수 있습니다. 첫 번째는 비 정체주의와 예외가있는 국가 모나드이며, 영향력있는 표현이 중단없이 발생하고 국가에 대한 독점적으로 접근 할 수 있다고 가정 할 때 순차적 환경에서 추론에 적합합니다.
지시 사항이 지시, 추측 및 비 원자적으로 실행되는 동시성에 대한 추론을 위해서는 메모리 동작의 효과 데이터 유형에 대한 무료 모나드가 있습니다. 이 모나드는 또한 RMEM 도구를 통한 앞서 언급 한 동시성 지원의 일부로 사용됩니다.
handwritten_support 의 파일은 CoQ, Isabelle 및 Hol4에 대한 라이브러리 정의를 제공합니다.
sail-riscv
- model // Sail specification modules
- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories
- c
- lem
- isabelle
- coq
- hol4
- latex
- prover_snapshots // snapshots of generated theorem prover definitions
- handwritten_support // prover support files
- c_emulator // supporting platform files for C emulator
- doc // documentation, including a reading guide
- test // test files
- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
- os-boot // information and sample files for booting OS images
이 모델은 BSD 2- 클라스 라이센스에 따라 라이센스로 제공됩니다.
Sri International의 Prashanth Mundkur가 원래 작성했으며 다른 사람들, 특히 캠브리지 대학교의 연구원들에 의해 더 발전했습니다.
전체 저자 목록은 LICENCE 및 git 비난을 참조하십시오.
이 소프트웨어는 Cambridge와 Edinburgh의 대학에서 EPSRC Grant EP/K008528/1이 부분적으로 자금을 지원하는 주류 시스템 (REMS) 프로젝트의 엄격한 엔지니어링 내에서 위의 내용에 의해 개발되었습니다.
이 소프트웨어는 SRI International과 Cambridge Computer Laboratory (Computer Science and Technology)에서 DARPA/AFRL 계약 FA8650-18-C-7809 ( "CIFV") 및 DARPA 계약 HR0011-18-C-에 의해 개발되었습니다. DARPA SSITH Research Program의 일환으로 0016 ( "ECATS").
이 프로젝트는 유럽 연합의 Horizon 2020 Research and Innovation Program (Grant Agrence 789108, Elver)에 따라 ERC (European Research Council)로부터 자금을 받았습니다.
