يحتوي هذا المستودع على مواصفات رسمية للهندسة المعمارية RISC-V ، مكتوبة في الإبحار. تم تبنيه من قبل مؤسسة RISC-V.
يحدد النموذج تنسيقات لغة التجميع للتعليمات ، وملحقات التشفير والتشفير المقابلة ، ودلالات التعليمات. يتم توفير دليل القراءة للنموذج في DOC/ Subdirectory ، إلى جانب دليل حول كيفية تمديد النموذج.
يمكن إنشاء تعريفات اللاتكس أو ASCIIDOC من النموذج المناسبة للإدراج في الوثائق المرجعية. هناك أيضًا دعم وثائق Sail Asciidoctor الأحدث لـ RISC-V.
SAIL هي لغة لوصف دلالات الهندسة المعمارية (ISA) للمعالجات: المواصفات المعمارية لسلوك تعليمات الجهاز. SAIL هي لغة صديقة للمهندسين ، مثلها مثل البائع السابق للبائعين ، ولكنها محددة بدقة مع الأدوات لدعم مجموعة واسعة من حالات الاستخدام.
بالنظر إلى مواصفات الشراع ، يمكن للأداة تحديدها ، أو إنشاء مقتطفات الوثائق (باللاتكس أو ASCIIDOC) ، وإنشاء محاكيات قابلة للتنفيذ ، وإظهار تغطية المواصفات ، وإنشاء إصدارات من ISA لأدوات نموذج الذاكرة المريحة ، ودعم توليد التسلسل الآلي لتعليمات التسلسل ، ، قم بإنشاء تعريفات نظرية للاحتفالات للدليل التفاعلي (في إيزابيل ، HOL4 ، و COQ) ، ودعم دليل على الكود الثنائي (في Islaris) ، و (قيد التقدم) إنشاء نموذج ISA مرجعي في SystemVerilog يمكن استخدامه للتحقق الرسمي للأجهزة.
يتم استخدام SAIL في أوصاف ISA المتعددة ، بما في ذلك الإصدارات الكاملة بشكل أساسي من السلوك المتسلسل لـ ARM-A (مشتقة تلقائيًا من المواصفات الداخلية للذراعين ، وتم إصدارها بموجب ترخيص BSD Clear بإذن ARM) ، RISC-V ، Cheri- RISC-V ، Cheriot ، MIPS ، و Cheri-Mips ؛ كل هذه كاملة بما يكفي لإقلاع أنظمة التشغيل المختلفة. هناك أيضًا نماذج شراعية لشظايا أصغر من طاقة IBM و 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 في intered_definitions/isabelle/rv64 generated_definitions/coq/RV64/riscv.v generated_definitions/isabelle/RV64/Riscv.thy . النموذج في generated_definitions/hol4/RV64/riscvScript.sml على التوالي. لقد اختبرنا إيزابيل 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-Tests/. يمكن تشغيل مجموعة الاختبار باستخدام test/run_tests.sh .
تتوفر معلومات حول خيارات التكوين للمحاكاة من ./c_emulator/riscv_sim_<arch> -h .
بعض الخيارات المفيدة هي: تكوين ما إذا كان الوصول إلى مصيدة الوصول غير المحسّنة ( --enable-misaligned ) ، وما إذا كانت طاولة الصفحة تحديث أجزاء PTE ( --enable-dirty-update ).
للحصول على صور نظام التشغيل ، راجع المعلومات الموجودة تحت نظام OS-Boot/ Subdirectory.
نادراً ما لا تلبي نسخة إصدار SAIL احتياجاتك. قد يحدث هذا إذا كنت بحاجة إلى إصلاح الأخطاء أو ميزة جديدة لم يتم بعد في إصدار SAIL الذي تم إصداره ، أو كنت تعمل بنشاط على SAIL. في هذه الحالة ، يمكنك إخبار Makefile sail-riscv باستخدام نسخة محلية من Sail عن طريق ضبط SAIL_DIR على جذر الخروج من repo Sail عند استدعاء make . بدلاً من ذلك ، يمكنك استخدام 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"
يقوم النموذج بإنشاء محاكي C الذي يمكنه تنفيذ ملفات RISC-V ELF ، ويوفر كلا المحاكسين دعم النظام الأساسي كافيًا لتمهيد Linux و FreeBSD و SEL4. يمكن ربط محاكي C مع محاكي Spike للتنفيذ مع تحديد الترادفية لكل المعدل.
يعمل محاكي C ، من أجل Boot Linux ، حاليًا عند حوالي 300 kips على Intel I7-7700 (عند تعطيل مفصل لكل تعقب للتصنيع) ، وهناك العديد من الفرص للتحسين المستقبلي (يعمل طراز Sail MIPS في حوالي 1 mips ). هذا يمكّن أحدها من تشغيل Linux في حوالي 4 دقائق ، و FreeBSD في حوالي دقيقتين. استخدام الذاكرة لمحاكي C عند تشغيل Linux حوالي 140 ميجابايت.
تقوم الملفات الموجودة في دليل محاكي C بتنفيذ تحميل ELF وأجهزة النظام الأساسي ، وتحدد خريطة الذاكرة الفعلية ، وتستخدم خيارات سطر الأوامر لتحديد خيارات ISA الخاصة بالتنفيذ.
يمكن لمحاكي C الذي تم إنشاؤه الشراع قياس تغطية فرع المواصفات لأي اختبارات تم تنفيذها ، وعرض النتائج على جداول الملفات وكإصدارات مصنوعة من HTML لمصدر النموذج.
للتحقق من تدفقات التعليمات العشوائية ، تدعم الأدوات البروتوكولات المستخدمة في TestRig لحقن التعليمات مباشرة في محاكي C وإنتاج معلومات تتبع بتنسيق RVFI. تم استخدام هذا للاختبار المتقاطع ضد Spike ومواصفات RVBS المكتوبة في Bluespec SystemVerilog.
يمكن أيضًا ربط محاكي C بشكل مباشر بـ Spike ، والذي يوفر تحفيزًا تمادًا على ثنائيات ELF (بما في ذلك أحذية OS). غالبًا ما يكون هذا مفيدًا في تصحيح مشكلات تمهيد نظام التشغيل في النموذج عندما يكون الحذاء معروفًا على Spike. من المفيد أيضًا اكتشاف خيارات التنفيذ الخاصة بالمنصة في Spike والتي لا يتم تفويضها بواسطة مواصفات ISA.
تم دمج طراز ISA مع النموذج التشغيلي لنموذج الذاكرة المريح RISC-V ، RVWMO (كما هو موضح في ملحق لمواصفات مستوى مستخدم RISC-V) ، وهو أحد النماذج المرجعية المستخدمة في تطوير RISC -V العمارة التزامن ؛ هذا جزء من أداة RMEM. تم دمجه أيضًا مع نموذج التزامن RISC-V البديهي كجزء من أداة ISLA-Axiomatic.
كجزء من أعمال الهندسة المعمارية لجامعة كامبريدج/ إينريا ، أنتجت تلك المجموعات وأصدرت مكتبة تضم حوالي 7000 اختبار Litmus. نماذج التزامن التشغيلية والبرديهة RISC-V متزامنة مع هذه الاختبارات ، وهي علاوة على ذلك ، تتفق مع السلوك المقابل للذراع للاختبارات المشتركة.
تم إجراء هذه الاختبارات أيضًا على أجهزة RISC-V ، على لوحة Proto Multicore Proto Multicore Multicore SIFC-V FU540 ، والتي تفضلت على سبيل الإعارة من Imperas. حتى الآن ، لوحظ فقط سلوك متسق بالتتابع هناك.
تهدف SAIL إلى دعم توليد تعريفات المثل النظرية الاصطلاحية عبر أدوات متعددة. في الوقت الحاضر ، يدعم Isabelle و HOL4 و COQ ، ويوفر دليل prover_snapshots لقطات من تعريفات المثل النظرية التي تم إنشاؤها.
يمكن أن تستهدف ترجمات نظرية النيرة هذه أحاديات متعددة لأغراض مختلفة. الأول هو موناد الدولة مع nondeterminism والاستثناءات ، مناسبة للتفكير في إعداد متسلسل ، على افتراض أن التعبيرات الفعالة يتم تنفيذها دون انقطاع وبوصول حصري إلى الدولة.
للتفكير حول التزامن ، حيث تنفذ الإرشادات خارج الترتيب ، بشكل مضاربة ، وغير منطقية ، هناك موناد مجاني حول نوع بيانات التأثير من إجراءات الذاكرة. يستخدم هذا الموناد أيضًا كجزء من دعم التزامن المذكور أعلاه عبر أداة 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 للحصول على قائمة كاملة من المؤلفين.
تم تطوير هذا البرنامج من قبل ما ورد أعلاه في مشروع الهندسة الصارمة للأنظمة الرئيسية (REMS) ، بتمويل جزئيًا من EPSRC Grant EP/K008528/1 ، في جامعات كامبريدج وإدنبره.
تم تطوير هذا البرنامج من قبل SRI International ومختبر الحاسبات بجامعة كامبريدج (قسم علوم الكمبيوتر والتكنولوجيا) بموجب عقد DARPA/AFRL FA8650-18-C-7809 ("CIFV") ، وتحت عقد DARPA HR0011-18-C- 0016 ("ECATS") كجزء من برنامج أبحاث DARPA SSITH.
تلقى هذا المشروع تمويلًا من مجلس الأبحاث الأوروبية (ERC) في إطار برنامج الأبحاث والابتكار في أفق الاتحاد الأوروبي 2020 (اتفاقية المنحة 789108 ، Elver).
