diff options
| -rw-r--r-- | README.md | 260 |
1 files changed, 129 insertions, 131 deletions
@@ -26,8 +26,8 @@ This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_ [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review). -Sail ----- +What is Sail? +------------- [Sail](https://www.cl.cam.ac.uk/~pes20/sail/) ([repo](https://github.com/rems-project/sail)) is a language for describing the instruction-set architecture (ISA) semantics of processors. Sail aims to provide a @@ -59,30 +59,83 @@ for smaller fragments of IBM POWER and x86. +Example instruction specifications +---------------------------------- -Directory Structure -------------------- +These are verbatim excerpts from the main model file, [riscv.sail](https://github.com/rems-project/sail-riscv/blob/master/model/riscv.sail), with a few comments added. + +### ITYPE (or ADDI) +~~~~~ +/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */ + +union clause ast = ITYPE : (bits(12), regbits, regbits, 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 = EXTS(imm); + let result : xlenbits = match op { + RISCV_ADDI => rs1_val + immext, + RISCV_SLTI => EXTZ(rs1_val <_s immext), + RISCV_SLTIU => EXTZ(rs1_val <_u immext), + RISCV_ANDI => rs1_val & immext, + RISCV_ORI => rs1_val | immext, + RISCV_XORI => rs1_val ^ immext + }; + X(rd) = result; + true +} + +/* 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_12(imm) +~~~~~~ + +### SRET + +~~~~~ +union clause ast = SRET : unit + +mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 + +function clause execute SRET() = { + match cur_privilege { + User => handle_illegal(), + Supervisor => if mstatus.TSR() == true + then handle_illegal() + else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC), + Machine => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC) + }; + false +} + +mapping clause assembly = SRET() <-> "sret" +~~~~~ -``` -sail-riscv -- model // Sail specification modules -- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories - - c - - ocaml - - 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 -- ocaml_emulator // supporting platform files for OCaml 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 -``` Sequential execution ---------- @@ -107,16 +160,14 @@ platform devices, define the physical memory map, and use command-line options to select implementation-specific ISA choices. -Use for specification coverage measurement in testing ------------------------------------------------------ +### Use for specification coverage measurement in testing The Sail-generated C emulator can measure specification branch coverage of any executed tests, displaying the results as per-file tables and as html-annotated versions of the model source. -Use as test oracle in tandem verification ------------------------------------------ +### Use as test oracle in tandem verification For tandem verification of random instruction streams we support the protocols used in [TestRIG](https://github.com/CTSRD-CHERI/TestRIG) to @@ -133,16 +184,6 @@ implementation choices in Spike that are not mandated by the ISA specification. -Use in test generation ----------------------- - -Our OCaml backend can produce QuickCheck-style random generators for -types in Sail specifications, which we have used to produce random -instructions sequences for testing. The generation of individual -types can be overridden by the developer to, for example, remove -implementation-specific instructions or introduce register biasing. - - Concurrent execution -------------------- @@ -154,8 +195,8 @@ part of our [RMEM](http://www.cl.cam.ac.uk/users/pes20/rmem) tool. It is also integrated with the RISC-V axiomatic concurrency model as part of our [isla-axiomatic](https://isla-axiomatic.cl.cam.ac.uk/) tool. -Concurrent testing ------------------- +## Concurrent testing + As part of our concurrency architecture work, we have produced and released a library of approximately 7000 [litmus @@ -169,8 +210,20 @@ FU540 multicore proto board (Freedom Unleashed), kindly on loan from Imperas. To date, we see only sequentially consistent behaviour there. -Provers -------- + +Use in test generation +---------------------- + +Our OCaml backend can produce QuickCheck-style random generators for +types in Sail specifications, which we have used to produce random +instructions sequences for testing. The generation of individual +types can be overridden by the developer to, for example, remove +implementation-specific instructions or introduce register biasing. + + + +Generating theorem-prover definitions +-------------------------------------- With Sail we aim to support the generation of idiomatic theorem prover definitions across multiple tools. At present we support Isabelle, @@ -193,8 +246,35 @@ tool. The files under `handwritten_support` provide library definitions for Coq, Isabelle and HOL4. -Building the model ------------------- + +Directory Structure +------------------- + +``` +sail-riscv +- model // Sail specification modules +- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories + - c + - ocaml + - 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 +- ocaml_emulator // supporting platform files for OCaml 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 +``` + +Getting started +--------------- + +### Building the model Install [Sail](https://github.com/rems-project/sail/), either via opam or by building Sail from source and setting `SAIL_DIR` in your @@ -232,8 +312,7 @@ corresponding prover libraries in the Sail directory (`$SAIL_DIR/lib/$prover`) are up-to-date and built, e.g. by running `make` in those directories. -Executing test binaries ------------------------ +### Executing test binaries The C and OCaml simulators can be used to execute small test binaries. The OCaml simulator depends on the Device Tree Compiler package, which can be @@ -256,8 +335,7 @@ A suite of RV32 and RV64 test programs derived from the included under [test/riscv-tests/](test/riscv-tests/). The test-suite can be run using `test/run_tests.sh`. -Configuring platform options ----------------------------- +### Configuring platform options Some information on additional configuration options for each simulator is available from `./ocaml_emulator/riscv_ocaml_sim_<arch> @@ -268,89 +346,7 @@ Some useful options are: configuring whether misaligned accesses trap whether page-table walks update PTE bits (`--enable-dirty-update` for C and `-enable-dirty-update` for OCaml). -Booting OS images ------------------ - -For booting operating system images, see the information under the -[os-boot/](os-boot/) subdirectory. - - -Example instructions --------------------- - -These are verbatim excerpts from the main model file, [riscv.sail](https://github.com/rems-project/sail-riscv/blob/master/model/riscv.sail), with a few comments added. - -### ITYPE (or ADDI) -~~~~~ -/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */ - -union clause ast = ITYPE : (bits(12), regbits, regbits, 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 = EXTS(imm); - let result : xlenbits = match op { - RISCV_ADDI => rs1_val + immext, - RISCV_SLTI => EXTZ(rs1_val <_s immext), - RISCV_SLTIU => EXTZ(rs1_val <_u immext), - RISCV_ANDI => rs1_val & immext, - RISCV_ORI => rs1_val | immext, - RISCV_XORI => rs1_val ^ immext - }; - X(rd) = result; - true -} - -/* 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_12(imm) -~~~~~~ - -### SRET - -~~~~~ -union clause ast = SRET : unit - -mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 - -function clause execute SRET() = { - match cur_privilege { - User => handle_illegal(), - Supervisor => if mstatus.TSR() == true - then handle_illegal() - else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC), - Machine => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC) - }; - false -} - -mapping clause assembly = SRET() <-> "sret" -~~~~~ +### Booting OS images Authors @@ -379,3 +375,5 @@ This software was developed within the Rigorous Engineering of Mainstream Systems (REMS) project, partly funded by EPSRC grant EP/K008528/1, at the Universities of Cambridge and Edinburgh. +This project has received funding from the European Research Council +(ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108). |