ที่เก็บนี้มีข้อกำหนดอย่างเป็นทางการของสถาปัตยกรรม RISC-V ที่เขียนด้วยการแล่นเรือ มันได้รับการรับรองจากมูลนิธิ RISC-V
แบบจำลองระบุรูปแบบภาษาแอสเซมบลีของคำแนะนำตัวเข้ารหัสและตัวถอดรหัสที่สอดคล้องกันและความหมายของคำสั่ง คู่มือการอ่านเกี่ยวกับโมเดลนั้นมีอยู่ใน DOC/ Subdirectory พร้อมด้วยคำแนะนำเกี่ยวกับวิธีการขยายโมเดล
คำจำกัดความของ LaTex หรือ Asciidoc สามารถสร้างได้จากแบบจำลองที่เหมาะสมสำหรับการรวมไว้ในเอกสารอ้างอิง นอกจากนี้ยังมีเอกสารประกอบการสนับสนุน Sail Asciidoctor รุ่นใหม่สำหรับ RISC-V
Sail เป็นภาษาสำหรับการอธิบายความหมายของสถาปัตยกรรมชุดคำสั่ง (ISA) ของโปรเซสเซอร์: ข้อกำหนดทางสถาปัตยกรรมของพฤติกรรมของคำแนะนำเครื่อง Sail เป็นภาษาที่เป็นมิตรกับวิศวกรเช่นเดียวกับ Pseudocode ผู้ขายก่อนหน้านี้ แต่มีการกำหนดอย่างแม่นยำมากขึ้นและด้วยเครื่องมือเพื่อรองรับกรณีการใช้งานที่หลากหลาย
ด้วยข้อกำหนดการแล่นเรือใบเครื่องมือสามารถตรวจสอบได้สร้างตัวอย่างเอกสาร (ใน LaTex หรือ Asciidoc) สร้างอีมูเลเตอร์ที่ปฏิบัติการได้แสดงความครอบคลุมข้อมูลจำเพาะสร้างเวอร์ชันของ ISA สำหรับเครื่องมือโมเดลหน่วยความจำที่ผ่อนคลายรองรับการสร้างการทดสอบลำดับการเรียนการสอนอัตโนมัติ สร้างคำจำกัดความทฤษฎีบท-พร็อพเพอร์เพื่อพิสูจน์การโต้ตอบ (ใน Isabelle, Hol4 และ COQ), หลักฐานสนับสนุนเกี่ยวกับรหัสไบนารี (ใน Islaris) และ (อยู่ระหว่างคืบหน้า) สร้างแบบจำลอง ISA อ้างอิงใน SystemVerilog ที่สามารถใช้สำหรับการตรวจสอบฮาร์ดแวร์อย่างเป็นทางการ
การแล่นเรือกำลังถูกใช้สำหรับคำอธิบาย ISA หลายรายการรวมถึงพฤติกรรมที่สมบูรณ์แบบของพฤติกรรมตามลำดับของ ARM-A (ได้มาจากข้อกำหนดด้านแขนภายในโดยอัตโนมัติและปล่อยภายใต้ใบอนุญาต BSD ที่ชัดเจนโดยได้รับอนุญาตจาก ARM), RISC-V, Cheri- Cheri- RISC-V, Cheriot, MIPS และ Cheri-Mips; ทั้งหมดนี้สมบูรณ์เพียงพอที่จะบูตระบบปฏิบัติการต่างๆ นอกจากนี้ยังมีรุ่นแล่นเรือสำหรับชิ้นส่วนขนาดเล็กของ IBM Power และ X86 รวมถึงรุ่นของรุ่น ACL2 X86 ที่แปลโดยอัตโนมัติจากนั้น
ติดตั้งใบเรือ บน Linux คุณสามารถดาวน์โหลดรุ่นไบนารี (แนะนำอย่างยิ่ง) หรือคุณสามารถติดตั้งได้จากแหล่งที่มาโดยใช้ OPAM แล้ว:
$ make
จะสร้างตัวจำลองใน c_emulator/riscv_sim_RV64
หากคุณได้รับข้อความแสดงข้อผิดพลาดที่บอกว่า sail: unknown option '--require-version'. เป็นเพราะคอมไพเลอร์เรือของคุณเก่าเกินไป คุณต้องการเวอร์ชัน 0.18 หรือใหม่กว่า
หนึ่งสามารถสร้างโมเดล RV32 หรือ RV64 ได้โดยการระบุ ARCH=RV32 หรือ ARCH=RV64 บนเส้น make และใช้คำต่อท้ายเป้าหมายที่ตรงกัน RV64 ถูกสร้างขึ้นโดยค่าเริ่มต้น แต่รุ่น RV32 สามารถสร้างได้โดยใช้:
$ ARCH=RV32 make
ซึ่งสร้างตัวจำลองใน c_emulator/riscv_sim_RV32
MakeFile เป้าหมาย riscv_isa_build , riscv_coq_build และ riscv_hol_build เรียกใช้สุภาษิตที่เกี่ยวข้องเพื่อประมวลผลคำจำกัดความและสร้างแบบจำลอง Isabelle ใน generated_definitions/coq/RV64/riscv.v generated_definitions/isabelle/RV64/Riscv.thy โมเดลใน 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>
ชุดทดสอบโปรแกรมทดสอบ RV32 และ RV64 ที่ได้มาจากการทดสอบ riscv-tests ห้องทดสอบรวมอยู่ในการทดสอบ/การทดสอบ RISCV/ ห้องทดสอบสามารถทำงานได้โดยใช้ test/run_tests.sh
ข้อมูลเกี่ยวกับตัวเลือกการกำหนดค่าสำหรับตัวจำลองมีให้บริการจาก ./c_emulator/riscv_sim_<arch> -h
ตัวเลือกที่มีประโยชน์บางอย่างคือ: การกำหนดค่าการเข้าถึงกับดักที่ไม่ถูกต้อง ( --enable-misaligned ) และไม่ว่าจะเป็นการอัปเดต PTE บิตหน้าโต๊ะ ( --enable-dirty-update )
สำหรับการบูตภาพระบบปฏิบัติการให้ดูข้อมูลภายใต้ Os-Boot/ Subdirectory
การแล่นเรือใบรุ่นปล่อยอาจไม่ตรงกับความต้องการของคุณ สิ่งนี้อาจเกิดขึ้นได้หากคุณต้องการการแก้ไขข้อผิดพลาดหรือคุณสมบัติใหม่ที่ยังไม่ได้อยู่ในเวอร์ชันเรือใบที่ปล่อยออกมาหรือคุณกำลังทำงานอย่างแข็งขันในการแล่นเรือ ในกรณีนี้คุณสามารถบอกให้ Makefile sail-riscv ใช้สำเนาของเรือใบในท้องถิ่นโดยการตั้ง SAIL_DIR เพื่อรูทของการชำระเงินของเรือสำเภาเมื่อคุณเรียก make อีกทางเลือกหนึ่งคุณสามารถใช้ opam pin เพื่อติดตั้งการแล่นเรือใบจากการชำระเงินในท้องถิ่นของ repo เรือใบตามที่อธิบายไว้ในคำแนะนำการติดตั้งใบเรือ
สิ่งเหล่านี้เป็นข้อความที่ตัดตอนมาจากไฟล์โมเดลที่มีคำแนะนำพื้นฐาน 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"
โมเดลสร้างตัวจำลอง C ที่สามารถเรียกใช้ไฟล์ RISC-V ELF และ Emulators ทั้งสองให้การสนับสนุนแพลตฟอร์มที่เพียงพอในการบูต Linux, FreeBSD และ SEL4 C emulator สามารถเชื่อมโยงกับตัวจำลองสไปค์เพื่อดำเนินการด้วยการตรวจสอบตีคู่แบบต่อเนื่อง
C Emulator สำหรับการบูต Linux ซึ่งปัจจุบันทำงานที่ประมาณ 300 kips บน Intel i7-7700 (เมื่อมีการติดตามรายละเอียดต่อการแนะนำการแนะนำ) และมีโอกาสมากมายสำหรับการเพิ่มประสิทธิภาพในอนาคต ). สิ่งนี้จะช่วยให้การบูต Linux ในเวลาประมาณ 4 นาทีและ FreeBSD ในเวลาประมาณ 2 นาที การใช้หน่วยความจำสำหรับตัวจำลอง C เมื่อบูต Linux อยู่ที่ประมาณ 140MB
ไฟล์ในไดเรกทอรี C Emulator ใช้การโหลด ELF และอุปกรณ์แพลตฟอร์มกำหนดแผนที่หน่วยความจำทางกายภาพและใช้ตัวเลือกบรรทัดคำสั่งเพื่อเลือกตัวเลือก ISA เฉพาะการใช้งาน
ตัวจำลอง C ที่สร้างขึ้นจากเรือสามารถวัดความครอบคลุมสาขาข้อมูลจำเพาะของการทดสอบที่ดำเนินการใด ๆ ซึ่งแสดงผลลัพธ์ตามตารางไฟล์และเป็นรุ่น HTML ที่มีคำย่อของแหล่งที่มาของแบบจำลอง
สำหรับการตรวจสอบแบบตีคู่ของสตรีมคำสั่งแบบสุ่มเครื่องมือสนับสนุนโปรโตคอลที่ใช้ใน TestRig เพื่อฉีดคำแนะนำโดยตรงลงในตัวจำลอง C และสร้างข้อมูลการติดตามในรูปแบบ RVFI สิ่งนี้ใช้สำหรับการทดสอบข้ามกับสไปค์และข้อกำหนด RVBS ที่เขียนใน Bluespec SystemVerilog
C emulator สามารถเชื่อมโยงโดยตรงกับสไปค์ซึ่งให้การตรวจสอบตีคู่บน ELF ไบนารี (รวมถึงรองเท้าบูทระบบปฏิบัติการ) สิ่งนี้มักจะมีประโยชน์ในการดีบักปัญหาการบูตระบบปฏิบัติการในรุ่นเมื่อการบูตเป็นที่รู้จักกันทำงานกับสไปค์ นอกจากนี้ยังมีประโยชน์ในการตรวจจับตัวเลือกการใช้งานเฉพาะแพลตฟอร์มใน Spike ที่ไม่ได้รับคำสั่งจากข้อกำหนดของ ISA
โมเดล ISA ถูกรวมเข้ากับโมเดลการดำเนินงานของโมเดลหน่วยความจำที่ผ่อนคลาย RISC-V, RVWMO (ตามที่อธิบายไว้ในภาคผนวกของข้อกำหนดระดับผู้ใช้ RISC-V) ซึ่งเป็นหนึ่งในโมเดลอ้างอิงที่ใช้ในการพัฒนา RISC -v สถาปัตยกรรมพร้อมกัน; นี่เป็นส่วนหนึ่งของเครื่องมือ RMEM นอกจากนี้ยังรวมเข้ากับโมเดลการพร้อมกันของ Axiomatic RISC-V ซึ่งเป็นส่วนหนึ่งของเครื่องมือ Isla-Axiomatic
ในฐานะส่วนหนึ่งของงานสถาปัตยกรรมพร้อมกันของมหาวิทยาลัยเคมบริดจ์/ Inria กลุ่มเหล่านั้นผลิตและเปิดตัวห้องสมุดการทดสอบสารสีน้ำเงินประมาณ 7,000 ครั้ง แบบจำลองการทำงานร่วมกันของ RISC-V ในการปฏิบัติงานและจริงนั้นอยู่ในการซิงค์สำหรับการทดสอบเหล่านี้และพวกเขาก็เห็นด้วยกับพฤติกรรมที่มีการออกแบบแขนที่สอดคล้องกันสำหรับการทดสอบที่เหมือนกัน
การทดสอบเหล่านั้นยังดำเนินการบนฮาร์ดแวร์ RISC-V บนกระดานโปรโต Multicore RISC-V FU540 Sifive (Freedom Unleashed) กรุณายืมตัวจาก Imperas จนถึงปัจจุบันพบพฤติกรรมที่สอดคล้องกันตามลำดับเท่านั้น
Sail มีจุดมุ่งหมายเพื่อสนับสนุนการสร้างคำจำกัดความของคำทฤษฎีเชิงทฤษฎีบทของสำนวนในเครื่องมือหลายอย่าง ในปัจจุบันรองรับ Isabelle, Hol4 และ Coq และไดเรกทอรี prover_snapshots ให้ภาพรวมของคำจำกัดความของทฤษฎีบทที่สร้างขึ้น
การแปลทฤษฎีบทแบบพร็อพเพอร์เหล่านี้สามารถกำหนดเป้าหมายหลาย monads เพื่อวัตถุประสงค์ที่แตกต่างกัน ครั้งแรกคือรัฐ monad ที่มี nondeterminism และข้อยกเว้นเหมาะสำหรับการให้เหตุผลในการตั้งค่าตามลำดับโดยสมมติว่าการแสดงออกที่มีประสิทธิภาพจะดำเนินการโดยไม่หยุดชะงักและมีการเข้าถึงรัฐพิเศษ
เพื่อการให้เหตุผลเกี่ยวกับการเกิดขึ้นพร้อมกันซึ่งคำแนะนำดำเนินการตามลำดับการสั่งซื้อแบบเก็งกำไรและไม่ใช่ในเชิงอะตอมมี monad ฟรีผ่านข้อมูลแบบเอฟเฟกต์ของการกระทำของหน่วยความจำ monad นี้ยังใช้เป็นส่วนหนึ่งของการสนับสนุนการพร้อมกันดังกล่าวผ่านเครื่องมือ 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 ในใบอนุญาต
เขียนโดย Prashanth Mundkur ที่ Sri International และพัฒนาโดยผู้อื่นโดยเฉพาะนักวิจัยที่มหาวิทยาลัยเคมบริดจ์
ดู LICENCE และ GIT ตำหนิสำหรับรายชื่อผู้เขียนที่สมบูรณ์
ซอฟต์แวร์นี้ได้รับการพัฒนาโดยด้านบนภายในโครงการวิศวกรรมที่เข้มงวดของโครงการ Mainstream Systems (REMS) ซึ่งได้รับทุนบางส่วนโดย EPSRC Grant EP/K008528/1 ที่มหาวิทยาลัยเคมบริดจ์และเอดินบะระ
ซอฟต์แวร์นี้ได้รับการพัฒนาโดย SRI International และ University of Cambridge Computer Laboratory (ภาควิชาวิทยาศาสตร์คอมพิวเตอร์และเทคโนโลยี) ภายใต้สัญญา DARPA/AFRL FA8650-18-C-7809 ("CIFV") และภายใต้สัญญา DARPA HR0011-18-C----C- 0016 ("ECATS") เป็นส่วนหนึ่งของโครงการวิจัย DARPA SSITH
โครงการนี้ได้รับเงินทุนจากสภาวิจัยยุโรป (ERC) ภายใต้โครงการวิจัยและนวัตกรรมของสหภาพยุโรปในสหภาพยุโรป (ข้อตกลงการให้สิทธิ์ 789108, Elver)
