Repositori ini berisi spesifikasi formal arsitektur RISC-V, yang ditulis dengan berlayar. Ini telah diadopsi oleh RISC-V Foundation.
Model ini menentukan format bahasa perakitan dari instruksi, encoder dan decoder yang sesuai, dan semantik instruksi. Panduan membaca untuk model disediakan di DOC/ Subdirektori, bersama dengan panduan tentang cara memperluas model.
Definisi lateks atau asciidoc dapat dihasilkan dari model yang cocok untuk dimasukkan dalam dokumentasi referensi. Ada juga dukungan dokumentasi Asciidoctor Sail Sail yang lebih baru untuk RISC-V.
Sail adalah bahasa untuk menggambarkan semantik instruksi-set arsitektur (ISA) dari prosesor: spesifikasi arsitektural perilaku instruksi mesin. Sail adalah bahasa yang ramah insinyur, seperti pseudocode vendor sebelumnya, tetapi lebih didefinisikan secara tepat dan dengan perkakas untuk mendukung berbagai kasus penggunaan.
Diberikan spesifikasi Sail, alat ini dapat memeriksanya, menghasilkan cuplikan dokumentasi (dalam lateks atau asciidoc), menghasilkan emulator yang dapat dieksekusi, menunjukkan cakupan spesifikasi, menghasilkan versi ISA untuk alat model memori yang santai, mendukung pembuatan uji pengajaran-pengajaran otomatis, Menghasilkan definisi pendakian teorema untuk bukti interaktif (dalam Isabelle, Hol4, dan COQ), bukti dukungan tentang kode biner (dalam Islaris), dan (sedang berlangsung) menghasilkan model ISA referensi dalam SystemVerilog yang dapat digunakan untuk verifikasi perangkat keras formal.
Layar sedang digunakan untuk beberapa deskripsi ISA, termasuk versi yang pada dasarnya lengkap dari perilaku berurutan ARM-A (secara otomatis berasal dari spesifikasi lengan-internal yang otoritatif, dan dirilis di bawah lisensi BSD yang jelas dengan izin ARM), RISC-V, Cheri- RISC-V, Cheriot, MIPS, dan Cheri-MIPS; Semua ini cukup lengkap untuk mem -boot berbagai sistem operasi. Ada juga model layar untuk fragmen yang lebih kecil dari daya IBM dan x86, termasuk versi model ACL2 X86 secara otomatis diterjemahkan dari itu.
Pasang layar. Di Linux Anda dapat mengunduh rilis biner (sangat disarankan), atau Anda dapat menginstal dari sumber menggunakan OPAM. Kemudian:
$ make
akan membangun simulator di c_emulator/riscv_sim_RV64 .
Jika Anda mendapatkan pesan kesalahan yang mengatakan sail: unknown option '--require-version'. Itu karena kompiler layar Anda terlalu tua. Anda membutuhkan versi 0.18 atau lebih baru.
Seseorang dapat membangun model RV32 atau RV64 dengan menentukan ARCH=RV32 atau ARCH=RV64 pada garis make , dan menggunakan akhiran target yang cocok. RV64 dibangun secara default, tetapi model RV32 dapat dibangun menggunakan:
$ ARCH=RV32 make
yang membuat simulator di c_emulator/riscv_sim_RV32 .
Makefile menargetkan riscv_isa_build , riscv_coq_build , dan riscv_hol_build memanggil prover masing -masing untuk memproses definisi dan menghasilkan model isabelle dalam model hole generated_definitions/coq/RV64/riscv.v generated_definitions/isabelle/RV64/Riscv.thy Model di masing -masing generated_definitions/hol4/RV64/riscvScript.sml . Kami telah menguji Isabelle 2018, CoQ 8.8.1, dan Hol4 Kananaskis-12. Saat membangun target-target ini, pastikan perpustakaan pepatah yang sesuai di direktori Sail ( $SAIL_DIR/lib/$prover ) terbaru dan dibangun, misalnya dengan menjalankan make di direktori tersebut.
Simulator dapat digunakan untuk menjalankan biner uji kecil.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Serangkaian program uji RV32 dan RV64 yang berasal dari tes- riscv-tests -suite dimasukkan dalam tes/RISCV-tes/. Test-suite dapat dijalankan menggunakan test/run_tests.sh .
Informasi tentang opsi konfigurasi untuk simulator tersedia dari ./c_emulator/riscv_sim_<arch> -h .
Beberapa opsi yang bermanfaat adalah: Mengkonfigurasi apakah mengakses perangkap yang tidak selaras ( --enable-misaligned ), dan apakah jalan-jalan halaman memperbarui bit PTE ( --enable-dirty-update ).
Untuk mem-boot gambar sistem operasi, lihat informasi di bawah OS-boot/ subdirektori.
Jarang, versi rilis Sail mungkin tidak memenuhi kebutuhan Anda. Ini bisa terjadi jika Anda memerlukan perbaikan bug atau fitur baru yang belum dalam versi layar yang dirilis, atau Anda secara aktif bekerja di layar. Dalam hal ini Anda dapat memberi tahu sail-riscv Makefile untuk menggunakan salinan Sail Local dengan mengatur SAIL_DIR ke akar checkout repo Sail saat Anda make . Atau, Anda dapat menggunakan opam pin untuk memasang Sail dari checkout lokal repo Sail seperti yang dijelaskan dalam instruksi pemasangan layar.
Ini adalah kutipan kata demi kata dari file model yang berisi instruksi dasar, riscv_insts_base.sail, dengan beberapa komentar ditambahkan.
/* 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"
Model ini membangun emulator C yang dapat menjalankan file RISC-V Elf, dan kedua emulator memberikan dukungan platform yang cukup untuk boot Linux, FreeBSD dan Sel4. Emulator C dapat dikaitkan dengan spike emulator untuk dieksekusi dengan verifikasi tandem per-instruksi.
Emulator C, untuk boot Linux, saat ini berjalan pada sekitar 300 kips pada Intel I7-7700 (ketika penelusuran per-instruksi terperinci dinonaktifkan), dan ada banyak peluang untuk optimasi di masa depan (model Sail MIPS berjalan di sekitar 1 MIPS di masa depan ). Ini memungkinkan seseorang untuk mem -boot Linux dalam waktu sekitar 4 menit, dan FreeBSD dalam waktu sekitar 2 menit. Penggunaan memori untuk emulator C saat booting Linux sekitar 140MB.
File dalam direktori C Emulator mengimplementasikan pemuatan ELF dan perangkat platform, mendefinisikan peta memori fisik, dan menggunakan opsi baris perintah untuk memilih pilihan ISA khusus implementasi.
Emulator C yang dihasilkan oleh Sail dapat mengukur cakupan cabang spesifikasi dari setiap tes yang dieksekusi, menampilkan hasil sesuai tabel per file dan sebagai versi HTML-dianotasi dari sumber model.
Untuk verifikasi tandem aliran instruksi acak, alat mendukung protokol yang digunakan dalam tesrig untuk secara langsung menyuntikkan instruksi ke dalam emulator C dan menghasilkan informasi jejak dalam format RVFI. Ini telah digunakan untuk pengujian silang terhadap Spike dan spesifikasi RVBS yang ditulis dalam bluespec systemverilog.
Emulator C juga dapat dihubungkan langsung ke Spike, yang memberikan verifikasi tandem pada binari ELF (termasuk sepatu bot OS). Ini sering berguna dalam men -debug masalah boot OS dalam model ketika boot diketahui bekerja di Spike. Ini juga berguna untuk mendeteksi pilihan implementasi spesifik platform di Spike yang tidak diamanatkan oleh spesifikasi ISA.
Model ISA terintegrasi dengan model operasional model memori santai RISC-V, RVWMO (seperti yang dijelaskan dalam lampiran spesifikasi tingkat pengguna RISC-V), yang merupakan salah satu model referensi yang digunakan dalam pengembangan RISC -V Arsitektur Konkurensi; Ini adalah bagian dari alat RMEM. Ini juga terintegrasi dengan model konkurensi aksiomatik RISC-V sebagai bagian dari alat ISLA-AXIOMATIC.
Sebagai bagian dari pekerjaan arsitektur Cambridge of Cambridge/ INRIA, kelompok -kelompok tersebut memproduksi dan merilis perpustakaan sekitar 7000 tes lakmus. Model konkurensi RISC-V operasional dan aksiomatik selaras untuk tes ini, dan mereka juga setuju dengan perilaku arm yang sesuai untuk tes yang sama.
Tes-tes tersebut juga telah dijalankan pada perangkat keras RISC-V, pada papan proto multicore RISC-V FU540 SIFIVE (Freedom Unleashed), dengan pinjaman dengan pinjaman dari Imperas. Sampai saat ini, hanya perilaku yang konsisten secara berurutan yang diamati di sana.
Sail bertujuan untuk mendukung generasi definisi pepatah teorema idiomatik di berbagai alat. Saat ini mendukung Isabelle, Hol4 dan COQ, dan direktori prover_snapshots menyediakan snapshot dari definisi pepatah teorema yang dihasilkan.
Terjemahan pendanaan teorema ini dapat menargetkan beberapa monad untuk tujuan yang berbeda. Yang pertama adalah monad negara dengan nondeterminisme dan pengecualian, cocok untuk penalaran dalam pengaturan berurutan, dengan asumsi bahwa ekspresi yang efektif dieksekusi tanpa gangguan dan dengan akses eksklusif ke negara.
Untuk penalaran tentang konkurensi, di mana instruksi mengeksekusi out-of-order, spekulatif, dan non-atomis, ada monad gratis atas efek data dari tindakan memori. Monad ini juga digunakan sebagai bagian dari dukungan konkurensi yang disebutkan di atas melalui alat RMEM.
File di bawah handwritten_support memberikan definisi perpustakaan untuk COQ, Isabelle dan 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
Model ini tersedia di bawah lisensi BSD Two-Clause dalam lisensi.
Awalnya ditulis oleh Prashanth Mundkur di Sri International, dan dikembangkan lebih lanjut oleh orang lain, terutama para peneliti di University of Cambridge.
Lihat LICENCE dan menyalahkan git untuk daftar lengkap penulis.
Perangkat lunak ini dikembangkan oleh di atas dalam Proyek Rekayasa Sistem Mainstream (REMS) yang ketat, sebagian didanai oleh EPSRC Grant EP/K008528/1, di universitas Cambridge dan Edinburgh.
Perangkat lunak ini dikembangkan oleh SRI International dan Laboratorium Komputer Universitas Cambridge (Departemen Ilmu dan Teknologi Komputer) di bawah kontrak DARPA/AFRL FA8650-18-C-7809 ("CIFV"), dan di bawah kontrak DARPA HR0011-18-C- 0016 ("ECATS") sebagai bagian dari program penelitian DARPA Ssith.
Proyek ini telah menerima dana dari Dewan Penelitian Eropa (ERC) di bawah Program Penelitian dan Inovasi Horizon 2020 Uni Eropa (Perjanjian Hibah 789108, Elver).
