このリポジトリには、帆に記述されたRISC-Vアーキテクチャの正式な仕様が含まれています。 RISC-V財団によって採用されています。
モデルは、命令のアセンブリ言語形式、対応するエンコーダーとデコーダー、および命令セマンティクスを指定します。モデルの読書ガイドは、Modelの拡張方法に関するガイドとともに、Doc/ Sub -Directoryで提供されています。
ラテックスまたはアスシドックの定義は、参照文書に含めるのに適したモデルから生成できます。また、RISC-Vの新しいSail Asciidoctorドキュメントサポートもあります。
Sailは、プロセッサの命令セットアーキテクチャ（ISA）セマンティクスを説明するための言語です。マシン命令の動作のアーキテクチャ仕様です。 Sailは、以前のベンダーPseudocodeと同様に、エンジニアに優しい言語ですが、より正確に定義され、幅広いユースケースをサポートするツールを使用しています。
セイル仕様が与えられた場合、ツールはそれをタイプチェックし、ドキュメントスニペット（ラテックスまたはAsciidocで）を生成し、実行可能なエミュレーターを生成し、仕様カバレッジを表示し、リラックスしたメモリモデルツールのISAのバージョンを生成し、自動命令テストの生成をサポートすることができます。インタラクティブプルーフ（Isabelle、hol4、およびCoqで）の定理プロバー定義を生成し、バイナリコード（Islarisで）に関するサポート証明、および（進行中）正式なハードウェア検証に使用できるSystemverilogで参照ISAモデルを生成します。
Sailは、ARM-Aの順次動作の本質的に完全なバージョン（権威あるARM内部仕様から自動的に導出され、ARMの許可を得てBSDクリアライセンスの下でリリースされた）、RISC-V、Cheri-を含む、複数のISAの説明に使用されています。 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以降が必要です。
ARCH=RV32またはARCH=RV64 make Lineで指定し、一致するターゲットの接尾辞を使用することにより、RV32またはRV64モデルのいずれかを構築できます。 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 、COQモデル、CoQ Models/definitions/rv64 generated_definitions/hol4/RV64/riscvScript.smlのモデル。 Isabelle 2018、Coq 8.8.1、およびHol4 Kananaskis-12をテストしました。これらのターゲットを構築するときは、Sail Directoryの対応するProverライブラリmake $SAIL_DIR/lib/$prover ）が最新で構築されていることを確認してください。
シミュレータは、小さなテストバイナリを実行するために使用できます。
$ ./c_emulator/riscv_sim_<arch> <elf-file>
riscv-testsテストスイートから派生したRV32およびRV64テストプログラムのスイートは、テスト/RISCVテスト/に含まれています。テストスイートはtest/run_tests.shを使用して実行できます。
シミュレータの構成オプションに関する情報は、 ./c_emulator/riscv_sim_<arch> -hから入手できます。
いくつかの有用なオプションは、不整合されたアクセスにTRAP（ --enable-misaligned ）にアクセスするかどうか、およびPage-Table WalksがPTEビット（ --enable-dirty-update ）を更新するかどうかを構成することです。
オペレーティングシステムの画像を起動するには、OS-Boot/ Subdirectoryの下の情報を参照してください。
まれに、Sailのリリースバージョンがあなたのニーズを満たしていないかもしれません。これは、リリースされた帆バージョンにまだバグ修正または新機能が必要な場合、またはSailに積極的に作業している場合に発生する可能性があります。この場合、 make呼び出し時にSail_dirをSAIL_DIRをSail_dirをルートに設定することにより、 sail-riscv Makefile Sailのローカルコピーを使用するように指示できます。または、 opam pin使用して、Sailの設置手順に記載されているように、Sail RepoのローカルチェックアウトからSAILをインストールできます。
これらは、基本指示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エミュレータは、インストラクションごとのタンデム検証を使用して実行するためにスパイクエミュレータに対してリンクできます。
Linuxブーツ用のCエミュレータは、現在、Intel I7-7700で約300キップで実行されています（詳細なインストラクショントレースが無効になっている場合）。 ）。これにより、約4分でLinuxを起動し、約2分でFreeBSDを起動できます。 Linuxの起動時のCエミュレータのメモリ使用量は約140MBです。
Cエミュレータディレクトリのファイルは、ELFの読み込みとプラットフォームデバイスを実装し、物理メモリマップを定義し、コマンドラインオプションを使用して実装固有のISA選択を選択します。
帆生成Cエミュレーターは、実行されたテストの仕様分岐カバレッジを測定し、ファイルごとのテーブルとして、およびモデルソースのHTML解釈バージョンとして結果を表示できます。
ランダム命令ストリームのタンデム検証のために、ツールはtestRigで使用されるプロトコルをサポートし、cmulatorに命令を直接挿入し、RVFI形式でトレース情報を作成します。これは、Bluespec Systemverilogで書かれたSpikeおよびRVBS仕様に対するクロステストに使用されています。
Cエミュレーターは、ELFバイナリ（OSブーツを含む）のタンデム検証を提供するSpikeに直接リンクすることもできます。これは、ブートがスパイクで作業していることが知られている場合、モデルのOSブーツの問題をデバッグするのに役立つことがよくあります。また、ISA仕様によって義務付けられていないスパイクのプラットフォーム固有の実装の選択を検出することも役立ちます。
ISAモデルは、RISC-Vリラックスメモリモデルの運用モデルであるRVWMO（RISC-Vユーザーレベル仕様の付録で説明されているように）と統合されています。これは、RISCの開発で使用される参照モデルの1つです。 -v並行性アーキテクチャ。これはRMEMツールの一部です。また、ISLA軸ツールの一部としてRISC-V Axiomatic Concurrencyモデルと統合されています。
ケンブリッジ大学/ INRIAの同時構造アーキテクチャ作業の一環として、これらのグループは約7000のリトマステストのライブラリを作成およびリリースしました。これらのテストでは、動作および公理的RISC-Vの並行性モデルが同期しており、さらに、共通のテストの対応するARMアーキテクチオビールに同意します。
これらのテストは、RISC-Vハードウェア、Sifive RISC-V FU540マルチコアプロトボード（Freedom Unleashed）でも、Imperasからの貸し出しで実行されています。現在までに、そこで順次一貫した動作のみが観察されました。
Sailは、複数のツールにわたる慣用定理上の定義の生成をサポートすることを目的としています。現在、Isabelle、Hol4、およびCoqをサポートしており、 prover_snapshotsディレクトリは、生成された定理Prover定義のスナップショットを提供しています。
これらの定理プロバー翻訳は、さまざまな目的で複数のモナドをターゲットにすることができます。 1つ目は、非決定的と例外を備えた州のモナドで、順次設定での推論に適しています。
命令が秩序外、投機的、および非原子的に実行される同時性についての推論のために、メモリアクションの効果データ型をめぐる無料のモナドがあります。このモナドは、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インターナショナルのPrashanth Mundkurによって執筆され、他の人、特にケンブリッジ大学の研究者によってさらに開発されました。
著者の完全なリストについては、 LICENCEとgitの責任を参照してください。
このソフトウェアは、ケンブリッジ大学とエジンバラ大学で、EPSRC助成金EP/K008528/1によって部分的に資金提供されている主流システム（REMS）プロジェクトの厳格なエンジニアリング内で上記によって開発されました。
このソフトウェアは、SRI InternationalとCambridge Computer Laboratory（コンピューターサイエンステクノロジー科）がDARPA/AFRL契約FA8650-18-C-7809（「CIFV」）の下で開発し、DARPA契約HR0011-18-C-の下で開発しました。 0016（ "Ecats"）DARPA SSITH研究プログラムの一部として。
このプロジェクトは、欧州連合の地平線2020研究イノベーションプログラム（助成金789108、エルバー）の下で、欧州研究評議会（ERC）から資金を受け取っています。
