Dieses Repository enthält eine formale Spezifikation der RISC-V-Architektur in Sail. Es wurde von der RISC-V Foundation übernommen.
Das Modell legt Montage -Sprachformate der Anweisungen, die entsprechenden Encoder und Decoder und die Anweisungssemantik fest. Eine Leselanleitung zum Modell finden Sie im DOC/ Sub -Verzeichnis sowie eine Anleitung zum Erweitern des Modells.
Latex- oder Asciidoc -Definitionen können aus dem Modell generiert werden, die für die Aufnahme in Referenzdokumentation geeignet sind. Es gibt auch die neuere Unterstützung für die Segel-Asciidoctor-Dokumentation für RISC-V.
Sail ist eine Sprache zur Beschreibung der Semantik der Anweisungs-Architektur (ISA) von Prozessoren: die architektonische Spezifikation des Verhaltens von Maschinenanweisungen. Sail ist eine ingenieurfreundliche Sprache, ähnlich wie früherer Anbieter-Pseudocode, aber genauer definiert und mit Werkzeugen, um eine breite Palette von Anwendungen zu unterstützen.
Bei einer Segelspezifikation kann das Tool es überprüft, Dokumentationsausschnitte (in Latex oder Asciidoc) generieren, ausführbare Emulatoren generieren, Spezifikationsabdeckungen anzeigen, Versionen des ISA für entspannte Speichermodell-Tools generieren, automatisierte Anweisungs-Sequenz-Testgenerierung unterstützen, die automatisierte Anweisungs-Sequenz-Erzeugung unterstützen, die Erzeugung von Anlehnungsequenz testen, unterstützen Sie die Generierung für automatisierte Anweisungen, die die Erzeugung von Anleitungssequenz testen, die automatisierte Anweisungs-Sequenz-Erzeugung unterstützen. Generieren Sie Theorem-Prover-Definitionen für interaktive Beweise (in Isabelle, HOL4 und CoQ), unterstützen Sie den Beweis für den Binärcode (in Islaris) und generieren ein Referenz-ISA-Modell in Systemverilog, das für die formale Hardwareüberprüfung verwendet werden kann.
Sail wird für mehrere ISA-Beschreibungen verwendet, einschließlich im Wesentlichen vollständige Versionen des sequentiellen Verhaltens von ARM-A (automatisch aus der maßgeblichen Arm-Internal-Spezifikation abgeleitet und unter einer BSD Clear-Lizenz mit ARM-Genehmigung veröffentlicht), RISC-V, Cheri- RISC-V, Cheriot, MIPS und Cheri-Mips; All dies ist vollständig genug, um verschiedene Betriebssysteme zu starten. Es gibt auch Segelmodelle für kleinere Fragmente von IBM Power und X86, einschließlich einer Version des ACL2 X86 -Modells, das automatisch daraus übersetzt wurde.
Segel einbauen. Unter Linux können Sie eine binäre Version (stark empfohlen) herunterladen oder mit OPAM aus der Quelle installieren. Dann:
$ make
Erstellt den Simulator in c_emulator/riscv_sim_RV64 .
Wenn Sie eine Fehlermeldung erhalten, die sail: unknown option '--require-version'. Es ist, weil Ihr Segel Compiler zu alt ist. Sie benötigen Version 0.18 oder höher.
Man kann entweder das RV32- oder das RV64 -Modell erstellen, indem ARCH=RV32 oder ARCH=RV64 in der make -Linie und die Verwendung des passenden Zielsuffix angeben. RV64 ist standardmäßig erstellt, das RV32 -Modell kann jedoch mit:
$ ARCH=RV32 make
Dies erstellt den Simulator in c_emulator/riscv_sim_RV32 .
Die Makefile -Ziele rufen riscv_isa_build , riscv_coq_build und riscv_hol_build auf den jeweiligen Prover auf, um die Definitionen zu verarbeiten und das Isabelle -Modell in generated_definitions/isabelle/RV64/Riscv.thy , das COQ -Modell in generated_definitions/coq/RV64/riscv.v in generiertem, zu verarbeiten. Modell in generated_definitions/hol4/RV64/riscvScript.sml . Wir haben Isabelle 2018, COQ 8.8.1 und Hol4 Kananaskis-12 getestet. Stellen Sie beim Erstellen dieser Ziele sicher, dass die entsprechenden Prover-Bibliotheken im Sail-Verzeichnis ( $SAIL_DIR/lib/$prover ) aktuell und gebaut sind, z. B. durch make in diesen Verzeichnissen.
Der Simulator kann verwendet werden, um kleine Testbinärdateien auszuführen.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Eine Suite von RV32- und RV64-Testprogrammen, die aus den riscv-tests Test-SUITe abgeleitet sind, ist unter test/riscv-tests/. Der Test-Suite kann mit test/run_tests.sh ausgeführt werden.
Informationen zu Konfigurationsoptionen für den Simulator finden Sie unter ./c_emulator/riscv_sim_<arch> -h .
Einige nützliche Optionen sind: Konfigurieren Sie, ob falsch ausgerichtete Zugriffe auf Trap ( --enable-misaligned ) und ob Page-Table-Spaziergänge PTE-Bits ( --enable-dirty-update ) aktualisieren.
Weitere Informationen finden Sie unter den Informationen unter dem OS-Boot/ Unterverzeichnis.
Selten erfüllt die Release -Version von Sail Ihre Bedürfnisse möglicherweise nicht. Dies kann passieren, wenn Sie eine Fehlerbehebung oder eine neue Funktion in der veröffentlichten Segelversion benötigen oder aktiv am Segel arbeiten. In diesem Fall können Sie das sail-riscv Makefile angeben, eine lokale Kopie von Sail zu verwenden, indem SAIL_DIR auf die Wurzel eines Auscheckens des Sail Repo setzen, wenn Sie make . Alternativ können Sie opam pin verwenden, um Segel aus einer lokalen Checkout des Segel -Repo zu installieren, wie in den Anweisungen zur Installation von Segeln beschrieben.
Dies sind wörtliche Auszüge aus der Modelldatei, die die Basisanweisungen riscv_insts_base.sail enthält, mit einigen Kommentaren.
/* 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"
Das Modell erstellt einen C-Emulator, mit dem RISC-V-ELF-Dateien ausgeführt werden können. Beide Emulatoren bieten Plattformunterstützung, die ausreicht, um Linux, FreeBSD und SEL4 zu starten. Der C-Emulator kann zur Ausführung mit der Tandemverifizierung von Tandemen mit dem Spike-Emulator verknüpft werden.
Der C-Emulator für den Linux-Boot läuft derzeit mit ca. 300 KIPS auf einem Intel i7-7700 (wenn detailliert die Verfolgung der Durchführung von problematischer Bedeutung ist) und es gibt viele Möglichkeiten für die zukünftige Optimierung (das Sail MIPS-Modell läuft bei ungefähr 1 MIPS. ). Dadurch kann man Linux in etwa 4 Minuten und FreeBSD in ca. 2 Minuten booten. Die Speicherverwendung für den C -Emulator beim Booten von Linux beträgt ungefähr 140 MB.
Die Dateien im C-Emulator-Verzeichnis implementieren das Laden von ELF und die Plattformgeräte, definieren die physische Speicherkarte und verwenden Befehlszeilenoptionen, um implementierungsspezifische ISA-Auswahlmöglichkeiten auszuwählen.
Der Segelgenerierte C-Emulator kann die Spezifikationszweigabdeckung aller ausgeführten Tests messen und die Ergebnisse gemäß den Datei Tabellen und als HTML-Annotierversionen der Modellquelle anzeigen.
Für die Überprüfung von zufälligen Befehlsströmen der Tandem unterstützen die Tools die in Testrig verwendeten Protokolle, um Anweisungen direkt in den C -Emulator zu injizieren und Spureninformationen im RVFI -Format zu erstellen. Dies wurde für Kreuzungstests gegen Spike und die RVBS -Spezifikation in Bluespec Systemverilog verwendet.
Der C-Emulator kann auch direkt mit Spike verknüpft werden, was Tandem-Überwachung für ELF-Binärdateien (einschließlich Betriebssystemstiefel) liefert. Dies ist oft nützlich, um OS -Boot -Probleme im Modell zu debuggen, wenn der Start bekannt ist, wenn der Start an Spike arbeitet. Es ist auch nützlich, plattformspezifische Implementierungsentscheidungen in Spike zu erkennen, die nicht von der ISA-Spezifikation vorgeschrieben sind.
Das ISA-Modell ist in das operative Modell des RISC-V-entspannten Speichermodells RVWMO (wie in einem Anhang der Spezifikation der RISC-V-Benutzerebene beschrieben) eines der in der Entwicklung des RISC verwendeten Referenzmodelle integriert -V Parallelitätsarchitektur; Dies ist Teil des RMEM -Tools. Es ist auch als Teil des isla-axiomatischen Werkzeugs in das axiomatische Parallelitätsmodell von RISC-V integriert.
Im Rahmen der Arbeit der University of Cambridge/ INRIA Concurquency Architecture produzierten und veröffentlichten diese Gruppen eine Bibliothek mit ungefähr 7000 Lackmus -Tests. Die operativen und axiomatischen RISC-V-Parallelitätsmodelle sind für diese Tests synchronisiert, und sie stimmen außerdem mit dem entsprechenden ARM-architektierten Verhalten für die gemeinsamen Tests überein.
Diese Tests wurden auch auf RISC-V-Hardware auf einem Sifive RISC-V FU540 Multicore Proto Board (Freedom Unleashed) durchgeführt, freundlich aus Kredit von Imperas. Bisher wurde dort nur nacheinander konsistentes Verhalten beobachtet.
Sail zielt darauf ab, die Erzeugung idiomatischer Theorem -Prover -Definitionen über mehrere Tools hinweg zu unterstützen. Derzeit unterstützt es Isabelle, Hol4 und Coq, und das Verzeichnis prover_snapshots bietet Schnappschüsse der generierten Theorem -Prover -Definitionen.
Diese Theorem-Prover-Übersetzungen können mehrere Monaden für verschiedene Zwecke abzielen. Der erste ist ein Zustandsmonade mit Nicht -Tätigkeiten und Ausnahmen, die für die Argumentation in einer sequentiellen Umgebung geeignet sind, vorausgesetzt, wirksame Ausdrücke werden ohne Unterbrechungen und mit ausschließlichem Zugriff auf den Staat ausgeführt.
Um die Übereinstimmung über die Parallelität zu argumentieren, wobei die Anweisungen spekulativ und nichtatomisch außerhalb der Reihenfolge ausführen, gibt es eine freie Monate über einen Effektdatenatyp von Speicheraktionen. Diese Monate wird auch als Teil der oben genannten Unterstützung der Parallelität über das RMEM -Tool verwendet.
Die Dateien unter handwritten_support bieten Bibliotheksdefinitionen für COQ, ISABELLE und 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
Das Modell wird unter der BSD-Zweiklause-Lizenz in der Lizenz zur Verfügung gestellt.
Ursprünglich von Prashanth Mundkur an der SRI International geschrieben und von anderen weiterentwickelt, insbesondere von Forschern der Universität von Cambridge.
Siehe LICENCE und Git -Schuld für eine vollständige Liste von Autoren.
Diese Software wurde im REMS -Projekt (Rigorous Engineering Engineering of Mainstream Systems) entwickelt, das teilweise vom EPSRC Grant EP/K008528/1 an den Universitäten von Cambridge und Edinburgh finanziert wurde.
Diese Software wurde von SRI International und dem Computerlabor der Universität von Cambridge (Abteilung für Informatik und Technologie) unter DARPA/AFRL-Vertrag FA8650-18-C-7809 ("CIFV") und im Rahmen von DARPA-Vertrag HR0011-18-C- 0016 ("ECATS") als Teil des DARPA -SSITH -Forschungsprogramms.
Dieses Projekt hat vom Europäischen Forschungsrat (ERC) im Rahmen des Horizon 2020 -Forschungs- und Innovationsprogramms der Europäischen Union (Grant Abkommen 789108, Elver) Mittel erhalten.
