diff --git a/CODE_STYLE.md b/CODE_STYLE.md index 4463e3aef..f4eef2247 100644 --- a/CODE_STYLE.md +++ b/CODE_STYLE.md @@ -6,7 +6,7 @@ RISC-V Sail model. Where something is not specified, please look for existing code similar to what is being added and copy the predominant style. -For C and OCaml, the formatting rules should be followed where applicable. +For C the formatting rules should be followed where applicable. For other languages, follow the standard style for that language if it exists; for example, Python should follow the standard PEP-8 style. @@ -86,7 +86,7 @@ Implementation * Do not use strings for anything that is not text * No new compile-time warnings from the Sail compiler should be introduced - (this does not include C or OCaml warnings for the code generated by the Sail + (this does not include C warnings for the code generated by the Sail compiler) * Do not use the `ext*` types and hooks for standard extensions unless diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index ed27b8c69..000000000 --- a/Dockerfile +++ /dev/null @@ -1,5 +0,0 @@ -FROM ocaml/opam -USER root -RUN DEBIAN_FRONTEND=noninteractive apt-get -y install zlib1g-dev pkg-config libgmp-dev z3 -USER opam -RUN opam install sail diff --git a/Makefile b/Makefile index 13e55a720..893c8841d 100644 --- a/Makefile +++ b/Makefile @@ -127,8 +127,6 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(S SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS)) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS)) -PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml) - SAIL_FLAGS += -dno_cast SAIL_DOC_FLAGS ?= -doc_embed plain @@ -205,7 +203,7 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) .PHONY: -all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) +all: c_emulator/riscv_sim_$(ARCH) .PHONY: all # the following ensures empty sail-generated .c files don't hang around and @@ -231,40 +229,12 @@ generated_definitions/ocaml/$(ARCH)/riscv.ml: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/ocaml/$(ARCH) $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_definitions/ocaml/$(ARCH) -o riscv $(SAIL_SRCS) -# cp -f is required because the generated_definitions/ocaml/$ARCH/*.ml files can -# be read-only, which would otherwise make subsequent builds fail. -ocaml_emulator/_sbuild/riscv_ocaml_sim.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) Makefile - mkdir -p ocaml_emulator/_sbuild - cp ocaml_emulator/_tags $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild - cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild - cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native - -ocaml_emulator/_sbuild/coverage.native: generated_definitions/ocaml/$(ARCH)/riscv.ml ocaml_emulator/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile - mkdir -p ocaml_emulator/_sbuild - cp $(PLATFORM_OCAML_SRCS) ocaml_emulator/_sbuild - cp -f generated_definitions/ocaml/$(ARCH)/*.ml ocaml_emulator/_sbuild - cp ocaml_emulator/_tags.bisect ocaml_emulator/_sbuild/_tags - cd ocaml_emulator/_sbuild && ocamlbuild -use-ocamlfind riscv_ocaml_sim.native && cp -L riscv_ocaml_sim.native coverage.native - -ocaml_emulator/riscv_ocaml_sim_$(ARCH): ocaml_emulator/_sbuild/riscv_ocaml_sim.native - rm -f $@ && cp -L $^ $@ && rm -f $^ - -ocaml_emulator/coverage_$(ARCH): ocaml_emulator/_sbuild/coverage.native - rm -f ocaml_emulator/riscv_ocaml_sim_$(ARCH) && cp -L $^ ocaml_emulator/riscv_ocaml_sim_$(ARCH) # since the test scripts runs this file - rm -rf bisect*.out bisect ocaml_emulator/coverage_$(ARCH) $^ - ./test/run_tests.sh # this will generate bisect*.out files in this directory - mkdir ocaml_emulator/bisect && mv bisect*.out bisect/ - mkdir ocaml_emulator/coverage_$(ARCH) && bisect-ppx-report -html ocaml_emulator/coverage_$(ARCH)/ -I ocaml_emulator/_sbuild/ bisect/bisect*.out - cloc: cloc --by-file --force-lang C,sail $(SAIL_SRCS) gcovr: gcovr -r . --html --html-detail -o index.html -ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml - ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ - c_preserve_fns=-c_preserve _set_Misa_C generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile @@ -281,8 +251,6 @@ $(SOFTFLOAT_LIBS): # convenience target .PHONY: csim csim: c_emulator/riscv_sim_$(ARCH) -.PHONY: osim -osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH) .PHONY: rvfi rvfi: c_emulator/riscv_rvfi_$(ARCH) @@ -468,29 +436,12 @@ sail-riscv.install: FORCE echo 'bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]' > sail-riscv.install echo 'share: [ $(foreach f,$(SHARE_FILES),"$f" {"$f"}) ]' >> sail-riscv.install -opam-build: - $(MAKE) ARCH=64 c_emulator/riscv_sim_RV64 - $(MAKE) ARCH=32 c_emulator/riscv_sim_RV32 - $(MAKE) riscv_rmem - -opam-install: - if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi - mkdir -p $(INSTALL_DIR)/bin - cp c_emulator/riscv_sim_RV64 $(INSTALL_DIR)/bin - cp c_emulator/riscv_sim_RV32 $(INSTALL_DIR)/bin - -opam-uninstall: - if [ -z "$(INSTALL_DIR)" ]; then echo INSTALL_DIR is unset; false; fi - rm $(INSTALL_DIR)/bin/riscv_sim_RV64 - rm $(INSTALL_DIR)/bin/riscv_sim_RV32 - clean: - -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* + -rm -rf generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* -$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64 - -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda -rm -f z3_problems -Holmake cleanAll @@ -498,4 +449,3 @@ clean: -rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.vos handwritten_support/mem_metadata.vok handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux -rm -f sail_doc/riscv_RV32.json -rm -f sail_doc/riscv_RV64.json - ocamlbuild -clean diff --git a/README.md b/README.md index 25057078d..69e885695 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ What is Sail? engineer-friendly language, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use-cases.

-Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate executable emulators (in C or OCaml), show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate theorem-prover definitions for +Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate an executable emulators, show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate theorem-prover definitions for interactive proof (in Isabelle, HOL4, and Coq), support proof about binary code (in Islaris), and (in progress) generate a reference ISA model in SystemVerilog that can be used for formal hardware verification.

@@ -139,13 +139,9 @@ mapping clause assembly = SRET() <-> "sret" Sequential execution ---------- -The model builds OCaml and C emulators that can execute RISC-V ELF +The model builds a C emulator that can execute RISC-V ELF files, and both emulators provide platform support sufficient to boot -Linux, FreeBSD and seL4. The OCaml emulator can generate its own -platform device-tree description, while the C emulator currently -requires a consistent description to be manually provided. The C -emulator can be linked against the Spike emulator for execution with -per-instruction tandem-verification. +Linux, FreeBSD and seL4. The C emulator can be linked against the Spike emulator for execution with per-instruction tandem-verification. The C emulator, for the Linux boot, currently runs at approximately 300 KIPS on an Intel i7-7700 (when detailed per-instruction tracing @@ -154,8 +150,8 @@ is disabled), and there are many opportunities for future optimisation boot Linux in about 4 minutes, and FreeBSD in about 2 minutes. Memory usage for the C emulator when booting Linux is approximately 140MB. -The files in the OCaml and C emulator directories implement ELF loading and the -platform devices, define the physical memory map, and use command-line +The files in the C emulator directory implements ELF loading and the +platform devices, defines the physical memory map, and usees command-line options to select implementation-specific ISA choices. @@ -208,8 +204,6 @@ Those tests have also been run on RISC-V hardware, on a SiFive RISC-V FU540 multicore proto board (Freedom Unleashed), kindly on loan from Imperas. To date, only sequentially consistent behaviour was observed there. - - Use in test generation ---------------------- @@ -219,8 +213,6 @@ 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 -------------------------------------- @@ -254,7 +246,6 @@ sail-riscv - model // Sail specification modules - generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories - c - - ocaml - lem - isabelle - coq @@ -263,7 +254,6 @@ sail-riscv - 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 @@ -280,9 +270,8 @@ Install [Sail](https://github.com/rems-project/sail/) [using opam](https://githu ``` $ make ``` -will build the 64-bit OCaml simulator in -`ocaml_emulator/riscv_ocaml_sim_RV64` and the C simulator in -`c_emulator/riscv_sim_RV64`. + +will build the C simulator in `c_emulator/riscv_sim_RV64`. One can build either the RV32 or the RV64 model by specifying `ARCH=RV32` or `ARCH=RV64` on the `make` line, and using the matching @@ -293,9 +282,7 @@ built using: $ ARCH=RV32 make ``` -which creates the 32-bit OCaml simulator in -`ocaml_emulator/riscv_ocaml_sim_RV32` and the C simulator in -`c_emulator/riscv_sim_RV32`. +which creates the C simulator in `c_emulator/riscv_sim_RV32`. The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and `riscv_hol_build` invoke the respective prover to process the @@ -311,19 +298,9 @@ corresponding prover libraries in the Sail directory ### 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 -installed in Ubuntu with: - -``` -$ sudo apt-get install device-tree-compiler -``` - -Then, you can run test binaries: - +The C simulator can be used to execute small test binaries. ``` -$ ./ocaml_emulator/riscv_ocaml_sim_ $ ./c_emulator/riscv_sim_ ``` @@ -335,17 +312,11 @@ can be run using `test/run_tests.sh`. ### Configuring platform options Some information on additional configuration options for each -simulator is available from `./ocaml_emulator/riscv_ocaml_sim_ --h` and `./c_emulator/riscv_sim_ -h`. +simulator is available from `./c_emulator/riscv_sim_ -h`. Some useful options are: configuring whether misaligned accesses trap -(`--enable-misaligned` for C and `-enable-misaligned` for OCaml), and -whether page-table walks update PTE bits (`--enable-dirty-update` for C -and `-enable-dirty-update` for OCaml). - -### Experimental integration with riscv-config - -There is also (as yet unmerged) support for [integration with riscv-config](https://github.com/rems-project/sail-riscv/pull/43) to allow configuring the compiled model according to a riscv-config yaml specification. +(`--enable-misaligned`), and +whether page-table walks update PTE bits (`--enable-dirty-update`). ### Booting OS images @@ -361,26 +332,12 @@ Licence The model is made available under the BSD two-clause licence in LICENCE. - Authors ------- - Prashanth Mundkur, SRI International; - Rishiyur S. Nikhil (Bluespec Inc.); - Jon French, University of Cambridge; - Brian Campbell, University of Edinburgh; - Robert Norton-Wright, University of Cambridge and Microsoft; - Alasdair Armstrong, University of Cambridge; - Thomas Bauereiss, University of Cambridge; - Shaked Flur, University of Cambridge; - Christopher Pulte, University of Cambridge; - Peter Sewell, University of Cambridge; - Alexander Richardson, University of Cambridge; - Hesham Almatary, University of Cambridge; - Jessica Clarke, University of Cambridge; - Nathaniel Wesley Filardo, Microsoft; - Peter Rugg, University of Cambridge; - Scott Johnson, Aril Computer Corp. +Originally written by Prashanth Mundkur at SRI International, and further developed by others, especially researchers at the University of Cambridge. + +See `LICENCE` and Git blame for a complete list of authors. Funding ------- diff --git a/build_simulators.sh b/build_simulators.sh index 8ad23e0bb..8fb76414f 100755 --- a/build_simulators.sh +++ b/build_simulators.sh @@ -10,8 +10,5 @@ function test_build () { fi } -test_build make ARCH=RV32 ocaml_emulator/riscv_ocaml_sim_RV32 -test_build make ARCH=RV64 ocaml_emulator/riscv_ocaml_sim_RV64 - test_build make ARCH=RV32 c_emulator/riscv_sim_RV32 test_build make ARCH=RV64 c_emulator/riscv_sim_RV64 diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md index b32b9a942..c00683b25 100644 --- a/doc/ExtendingGuide.md +++ b/doc/ExtendingGuide.md @@ -60,7 +60,7 @@ construct of the Sail language. `riscv_platform.sail` can be examined to see how this is done for the SiFive core-local interrupt (CLINT) controller, the HTIF timer and terminal devices. The implementation of the actual functionality provided by these MMIO -devices would need to be added to the C and OCaml emulators. +devices would need to be added to the C emulators. If this functionality requires the definition of new interrupt sources, their encodings would need to be added to `riscv_types.sail`, diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index 5c8d0f603..bf647932e 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -63,12 +63,12 @@ such as the platform memory map. controller, and the MMIO interfaces to the clock, timer and terminal devices. Sail `extern` definitions are used to connect externally provided (i.e. external to the Sail model) platform functionality, - such as those provided by the platform support in the C and OCaml - emulators. This file also contains the externally selectable + such as those provided by the platform support in the C + emulator. This file also contains the externally selectable options for platform behavior, such as the handling of misaligned memory accesses, the handling of PTE dirty-bit updates during address translation, etc. These platform options can be specified - via command line switches in the C and OCaml emulators. + via command line switches in the C emulator. - `riscv_mem.sail` contains the functions that convert accesses to physical addresses into accesses to physical memory, or MMIO @@ -128,7 +128,7 @@ Structure of the C emulator ---------------------------- The diagram below illustrates how the C emulator is built from the -Sail model. The OCaml emulator follows the same approach. +Sail model. diff --git a/model/prelude.sail b/model/prelude.sail index 3555296b3..bc06d622c 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -47,16 +47,16 @@ val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), overload operator - = {sub_vec, sub_vec_int} -val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int +val quot_round_zero = {interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int +val rem_round_zero = {interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int /* The following defines % as euclidean modulus */ overload operator % = {emod_int} -val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y. +val min_int = {interpreter: "min_int", lem: "min", coq: "min_atom", c: "min_int"} : forall 'x 'y. (int('x), int('y)) -> {'z, ('x <= 'y & 'z == 'x) | ('x > 'y & 'z == 'y). int('z)} -val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y. +val max_int = {interpreter: "max_int", lem: "max", coq: "max_atom", c: "max_int"} : forall 'x 'y. (int('x), int('y)) -> {'z, ('x >= 'y & 'z == 'x) | ('x < 'y & 'z == 'y). int('z)} overload min = {min_int} @@ -68,20 +68,20 @@ val pow2 = "pow2" : forall 'n. int('n) -> int(2 ^ 'n) val print = "print_endline" : string -> unit val print_string = "print_string" : (string, string) -> unit -val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_instr = {interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_reg = {interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_mem = {interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit +val print_platform = {interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_step = {ocaml: "Platform.print_step", c: "print_step"} : unit -> unit +val print_step = {c: "print_step"} : unit -> unit function print_step() = () -val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool -val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool -val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool +val get_config_print_instr = {c:"get_config_print_instr"} : unit -> bool +val get_config_print_reg = {c:"get_config_print_reg"} : unit -> bool +val get_config_print_mem = {c:"get_config_print_mem"} : unit -> bool -val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool +val get_config_print_platform = {c:"get_config_print_platform"} : unit -> bool // defaults for other backends function get_config_print_instr () = false function get_config_print_reg () = false diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 2dc6e7528..79a0beb69 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -15,13 +15,11 @@ */ val elf_tohost = { - ocaml: "Elf_loader.elf_tohost", interpreter: "Elf_loader.elf_tohost", c: "elf_tohost" } : unit -> int val elf_entry = { - ocaml: "Elf_loader.elf_entry", interpreter: "Elf_loader.elf_entry", c: "elf_entry" } : unit -> int @@ -29,11 +27,11 @@ val elf_entry = { // Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096) // because this model performs `cbo.zero` with a single write, and the behaviour // with cache blocks larger than a page is not clearly defined. -val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) +val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) /* Main memory */ -val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits -val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits +val plat_ram_base = {c: "plat_ram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits +val plat_ram_size = {c: "plat_ram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits /* whether the MMU should update dirty bits in PTEs */ val plat_enable_dirty_update = {ocaml: "Platform.enable_dirty_update", @@ -56,15 +54,15 @@ val plat_mtval_has_illegal_inst_bits = {ocaml: "Platform.mtval_has_illegal_inst_ lem: "plat_mtval_has_illegal_inst_bits"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = {ocaml: "Platform.rom_base", interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits +val plat_rom_base = {interpreter: "Platform.rom_base", c: "plat_rom_base", lem: "plat_rom_base"} : unit -> xlenbits +val plat_rom_size = {interpreter: "Platform.rom_size", c: "plat_rom_size", lem: "plat_rom_size"} : unit -> xlenbits /* Location of clock-interface, which should match with the spec in the DTB */ -val plat_clint_base = {ocaml: "Platform.clint_base", interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits -val plat_clint_size = {ocaml: "Platform.clint_size", interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits +val plat_clint_base = {interpreter: "Platform.clint_base", c: "plat_clint_base", lem: "plat_clint_base"} : unit -> xlenbits +val plat_clint_size = {interpreter: "Platform.clint_size", c: "plat_clint_size", lem: "plat_clint_size"} : unit -> xlenbits /* Location of HTIF ports */ -val plat_htif_tohost = {ocaml: "Platform.htif_tohost", c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits +val plat_htif_tohost = {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ()) // todo: fromhost @@ -124,7 +122,7 @@ function within_htif_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen /* CLINT (Core Local Interruptor), based on Spike. */ -val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int +val plat_insns_per_tick = {interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int // assumes a single hart, since this typically is a vector of per-hart registers. register mtimecmp : bits(64) // memory-mapped internal clint register. @@ -284,8 +282,8 @@ function tick_clock() = { /* Basic terminal character I/O. */ -val plat_term_write = {ocaml: "Platform.term_write", c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit -val plat_term_read = {ocaml: "Platform.term_read", c: "plat_term_read", lem: "plat_term_read"} : unit -> bits(8) +val plat_term_write = {c: "plat_term_write", lem: "plat_term_write"} : bits(8) -> unit +val plat_term_read = { c: "plat_term_read", lem: "plat_term_read"} : unit -> bits(8) /* Spike's HTIF device interface, which multiplexes the above MMIO devices. */ diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 3a673feb8..0186a45f5 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -47,84 +47,84 @@ register float_fflags : bits(64) /* **************************************************************** */ /* ADD/SUB/MUL/DIV */ -val extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Add = {c: "softfloat_f16add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Add (rm, v1, v2) = { extern_f16Add(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Sub = {c: "softfloat_f16sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sub (rm, v1, v2) = { extern_f16Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Mul = {c: "softfloat_f16mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Mul (rm, v1, v2) = { extern_f16Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit +val extern_f16Div = {c: "softfloat_f16div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit val riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16Div (rm, v1, v2) = { extern_f16Div(rm, v1, v2); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Add = {c: "softfloat_f32add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit val riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Add (rm, v1, v2) = { extern_f32Add(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Sub = {c: "softfloat_f32sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit val riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Sub (rm, v1, v2) = { extern_f32Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Mul = {c: "softfloat_f32mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit val riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Mul (rm, v1, v2) = { extern_f32Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit +val extern_f32Div = {c: "softfloat_f32div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit val riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32Div (rm, v1, v2) = { extern_f32Div(rm, v1, v2); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Add = {c: "softfloat_f64add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit val riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Add (rm, v1, v2) = { extern_f64Add(rm, v1, v2); (float_fflags[4 .. 0], float_result) } -val extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Sub = {c: "softfloat_f64sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit val riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Sub (rm, v1, v2) = { extern_f64Sub(rm, v1, v2); (float_fflags[4 .. 0], float_result) } -val extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Mul = {c: "softfloat_f64mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit val riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Mul (rm, v1, v2) = { extern_f64Mul(rm, v1, v2); (float_fflags[4 .. 0], float_result) } -val extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit +val extern_f64Div = {c: "softfloat_f64div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit val riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64Div (rm, v1, v2) = { extern_f64Div(rm, v1, v2); @@ -134,21 +134,21 @@ function riscv_f64Div (rm, v1, v2) = { /* **************************************************************** */ /* MULTIPLY-ADD */ -val extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit +val extern_f16MulAdd = {c: "softfloat_f16muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit val riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H) function riscv_f16MulAdd (rm, v1, v2, v3) = { extern_f16MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit +val extern_f32MulAdd = {c: "softfloat_f32muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit val riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S) function riscv_f32MulAdd (rm, v1, v2, v3) = { extern_f32MulAdd(rm, v1, v2, v3); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit +val extern_f64MulAdd = {c: "softfloat_f64muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit val riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D) function riscv_f64MulAdd (rm, v1, v2, v3) = { extern_f64MulAdd(rm, v1, v2, v3); @@ -158,21 +158,21 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = { /* **************************************************************** */ /* SQUARE ROOT */ -val extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit +val extern_f16Sqrt = {c: "softfloat_f16sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit val riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H) function riscv_f16Sqrt (rm, v) = { extern_f16Sqrt(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit +val extern_f32Sqrt = {c: "softfloat_f32sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit val riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S) function riscv_f32Sqrt (rm, v) = { extern_f32Sqrt(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit +val extern_f64Sqrt = {c: "softfloat_f64sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit val riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D) function riscv_f64Sqrt (rm, v) = { extern_f64Sqrt(rm, v); @@ -182,56 +182,56 @@ function riscv_f64Sqrt (rm, v) = { /* **************************************************************** */ /* CONVERSIONS */ -val extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit +val extern_f16ToI32 = {c: "softfloat_f16toi32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit val riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W) function riscv_f16ToI32 (rm, v) = { extern_f16ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit +val extern_f16ToUi32 = {c: "softfloat_f16toui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit val riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU) function riscv_f16ToUi32 (rm, v) = { extern_f16ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit +val extern_i32ToF16 = {c: "softfloat_i32tof16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit val riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H) function riscv_i32ToF16 (rm, v) = { extern_i32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF16 = {c: "softfloat_ui32tof16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit val riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H) function riscv_ui32ToF16 (rm, v) = { extern_ui32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit +val extern_f16ToI64 = {c: "softfloat_f16toi64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit val riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L) function riscv_f16ToI64 (rm, v) = { extern_f16ToI64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit +val extern_f16ToUi64 = {c: "softfloat_f16toui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit val riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU) function riscv_f16ToUi64 (rm, v) = { extern_f16ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit +val extern_i64ToF16 = {c: "softfloat_i64tof16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit val riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H) function riscv_i64ToF16 (rm, v) = { extern_i64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit +val extern_ui64ToF16 = {c: "softfloat_ui64tof16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit val riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H) function riscv_ui64ToF16 (rm, v) = { extern_ui64ToF16(rm, v); @@ -239,154 +239,154 @@ function riscv_ui64ToF16 (rm, v) = { } -val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit +val extern_f32ToI32 = {c: "softfloat_f32toi32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit val riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) function riscv_f32ToI32 (rm, v) = { extern_f32ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit +val extern_f32ToUi32 = {c: "softfloat_f32toui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit val riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU) function riscv_f32ToUi32 (rm, v) = { extern_f32ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit +val extern_i32ToF32 = {c: "softfloat_i32tof32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit val riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S) function riscv_i32ToF32 (rm, v) = { extern_i32ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF32 = {c: "softfloat_ui32tof32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit val riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S) function riscv_ui32ToF32 (rm, v) = { extern_ui32ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit +val extern_f32ToI64 = {c: "softfloat_f32toi64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit val riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L) function riscv_f32ToI64 (rm, v) = { extern_f32ToI64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit +val extern_f32ToUi64 = {c: "softfloat_f32toui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit val riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU) function riscv_f32ToUi64 (rm, v) = { extern_f32ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit +val extern_i64ToF32 = {c: "softfloat_i64tof32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit val riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S) function riscv_i64ToF32 (rm, v) = { extern_i64ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit +val extern_ui64ToF32 = {c: "softfloat_ui64tof32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit val riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S) function riscv_ui64ToF32 (rm, v) = { extern_ui64ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit +val extern_f64ToI32 = {c: "softfloat_f64toi32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit val riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W) function riscv_f64ToI32 (rm, v) = { extern_f64ToI32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit +val extern_f64ToUi32 = {c: "softfloat_f64toui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit val riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU) function riscv_f64ToUi32 (rm, v) = { extern_f64ToUi32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit +val extern_i32ToF64 = {c: "softfloat_i32tof64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit val riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D) function riscv_i32ToF64 (rm, v) = { extern_i32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit +val extern_ui32ToF64 = {c: "softfloat_ui32tof64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit val riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D) function riscv_ui32ToF64 (rm, v) = { extern_ui32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit +val extern_f64ToI64 = {c: "softfloat_f64toi64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit val riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L) function riscv_f64ToI64 (rm, v) = { extern_f64ToI64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit +val extern_f64ToUi64 = {c: "softfloat_f64toui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit val riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU) function riscv_f64ToUi64 (rm, v) = { extern_f64ToUi64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit +val extern_i64ToF64 = {c: "softfloat_i64tof64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit val riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D) function riscv_i64ToF64 (rm, v) = { extern_i64ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit +val extern_ui64ToF64 = {c: "softfloat_ui64tof64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit val riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D) function riscv_ui64ToF64 (rm, v) = { extern_ui64ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit +val extern_f16ToF32 = {c: "softfloat_f16tof32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit val riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) function riscv_f16ToF32 (rm, v) = { extern_f16ToF32(rm, v); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit +val extern_f16ToF64 = {c: "softfloat_f16tof64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit val riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D) function riscv_f16ToF64 (rm, v) = { extern_f16ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit +val extern_f32ToF64 = {c: "softfloat_f32tof64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit val riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D) function riscv_f32ToF64 (rm, v) = { extern_f32ToF64(rm, v); (float_fflags[4 .. 0], float_result) } -val extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit +val extern_f32ToF16 = {c: "softfloat_f32tof16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit val riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H) function riscv_f32ToF16 (rm, v) = { extern_f32ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit +val extern_f64ToF16 = {c: "softfloat_f64tof16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit val riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) function riscv_f64ToF16 (rm, v) = { extern_f64ToF16(rm, v); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit +val extern_f64ToF32 = {c: "softfloat_f64tof32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit val riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S) function riscv_f64ToF32 (rm, v) = { extern_f64ToF32(rm, v); @@ -396,126 +396,126 @@ function riscv_f64ToF32 (rm, v) = { /* **************************************************************** */ /* COMPARISONS */ -val extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit +val extern_f16Lt = {c: "softfloat_f16lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit val riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt (v1, v2) = { extern_f16Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit +val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt_quiet (v1, v2) = { extern_f16Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit +val extern_f16Le = {c: "softfloat_f16le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le (v1, v2) = { extern_f16Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit +val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le_quiet (v1, v2) = { extern_f16Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit +val extern_f16Eq = {c: "softfloat_f16eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { extern_f16Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit +val extern_f32Lt = {c: "softfloat_f32lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt (v1, v2) = { extern_f32Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit +val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt_quiet (v1, v2) = { extern_f32Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit +val extern_f32Le = {c: "softfloat_f32le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le (v1, v2) = { extern_f32Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit +val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le_quiet (v1, v2) = { extern_f32Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit +val extern_f32Eq = {c: "softfloat_f32eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { extern_f32Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit +val extern_f64Lt = {c: "softfloat_f64lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt (v1, v2) = { extern_f64Lt(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit +val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt_quiet (v1, v2) = { extern_f64Lt_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit +val extern_f64Le = {c: "softfloat_f64le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le (v1, v2) = { extern_f64Le(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit +val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le_quiet (v1, v2) = { extern_f64Le_quiet(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit +val extern_f64Eq = {c: "softfloat_f64eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { extern_f64Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit +val extern_f16roundToInt = {c: "softfloat_f16roundToInt", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) function riscv_f16roundToInt (rm, v, exact) = { extern_f16roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[15 .. 0]) } -val extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit +val extern_f32roundToInt = {c: "softfloat_f32roundToInt", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit val riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) function riscv_f32roundToInt (rm, v, exact) = { extern_f32roundToInt(rm, v, exact); (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit +val extern_f64roundToInt = {c: "softfloat_f64roundToInt", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) function riscv_f64roundToInt (rm, v, exact) = { extern_f64roundToInt(rm, v, exact); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 2cd5df2be..12f0bf92e 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -165,11 +165,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = * where cancellation can be performed. */ -val speculate_conditional = monadic {ocaml: "Platform.speculate_conditional", interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool +val speculate_conditional = monadic {interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool -val load_reservation = {ocaml: "Platform.load_reservation", interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit -val match_reservation = {ocaml: "Platform.match_reservation", interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool -val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit +val load_reservation = {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit +val match_reservation = {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool +val cancel_reservation = {interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6d1afd0ee..76199ebd7 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -79,39 +79,39 @@ bitfield Misa : xlenbits = { register misa : Misa /* whether misa is R/W */ -val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool +val sys_enable_writable_misa = {c: "sys_enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool /* whether misa.c was enabled at boot */ -val sys_enable_rvc = {c: "sys_enable_rvc", ocaml: "Platform.enable_rvc", _: "sys_enable_rvc"} : unit -> bool +val sys_enable_rvc = {c: "sys_enable_rvc", _: "sys_enable_rvc"} : unit -> bool /* whether misa.{f,d} were enabled at boot */ -val sys_enable_fdext = {c: "sys_enable_fdext", ocaml: "Platform.enable_fdext", _: "sys_enable_fdext"} : unit -> bool +val sys_enable_fdext = {c: "sys_enable_fdext", _: "sys_enable_fdext"} : unit -> bool /* whether Svinval was enabled at boot */ -val sys_enable_svinval = {c: "sys_enable_svinval", ocaml: "Platform.enable_svinval", _: "sys_enable_svinval"} : unit -> bool +val sys_enable_svinval = {c: "sys_enable_svinval", _: "sys_enable_svinval"} : unit -> bool /* whether Zcb was enabled at boot */ -val sys_enable_zcb = {c: "sys_enable_zcb", ocaml: "Platform.enable_zcb", _: "sys_enable_zcb"} : unit -> bool +val sys_enable_zcb = {c: "sys_enable_zcb", _: "sys_enable_zcb"} : unit -> bool /* whether zfinx was enabled at boot */ -val sys_enable_zfinx = {c: "sys_enable_zfinx", ocaml: "Platform.enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool +val sys_enable_zfinx = {c: "sys_enable_zfinx", _: "sys_enable_zfinx"} : unit -> bool /* whether the N extension was enabled at boot */ -val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "sys_enable_next"} : unit -> bool +val sys_enable_next = {c: "sys_enable_next", _: "sys_enable_next"} : unit -> bool /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if supervisor mode is implemented and non-bare addressing modes are supported. */ -val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool +val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool /* How many PMP entries are implemented. This must be 0, 16 or 64 (this is checked at runtime). */ -val sys_pmp_count = {c: "sys_pmp_count", ocaml: "Platform.pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) +val sys_pmp_count = {c: "sys_pmp_count", _: "sys_pmp_count"} : unit -> range(0, 64) /* G parameter that specifies the PMP grain size. The grain size is 2^(G+2), e.g. G=0 -> 4 bytes, G=10 -> 4096 bytes. */ -val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63) +val sys_pmp_grain = {c: "sys_pmp_grain", _: "sys_pmp_grain"} : unit -> range(0, 63) /* whether misa.v was enabled at boot */ -val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool +val sys_enable_vext = {c: "sys_enable_vext", _: "sys_enable_vext"} : unit -> bool /* whether misa.b was enabled at boot */ -val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool +val sys_enable_bext = {c: "sys_enable_bext", _: "sys_enable_bext"} : unit -> bool // CBO extensions. Zicbop cannot be enabled/disabled because it has no effect // at all on this model. -val sys_enable_zicbom = {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool -val sys_enable_zicboz = {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool +val sys_enable_zicbom = {c: "sys_enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool +val sys_enable_zicboz = {c: "sys_enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on @@ -734,7 +734,6 @@ mapping opst_code : seed_opst <-> bits(2) = { * read_seed_csr. Hence it appears here. */ val get_16_random_bits = { - ocaml: "Platform.get_16_random_bits", interpreter: "Platform.get_16_random_bits", c: "plat_get_16_random_bits", lem: "plat_get_16_random_bits" diff --git a/ocaml_emulator/_tags b/ocaml_emulator/_tags deleted file mode 100644 index 168de09b3..000000000 --- a/ocaml_emulator/_tags +++ /dev/null @@ -1,3 +0,0 @@ -<**/*.ml>: bin_annot, annot -<*.m{l,li}>: package(lem), package(linksem), package(zarith) -: package(lem), package(linksem), package(zarith) diff --git a/ocaml_emulator/_tags.bisect b/ocaml_emulator/_tags.bisect deleted file mode 100644 index ca6f27a9e..000000000 --- a/ocaml_emulator/_tags.bisect +++ /dev/null @@ -1,3 +0,0 @@ -<**/*.ml>: bin_annot, annot -<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(bisect_ppx) -: package(lem), package(linksem), package(zarith), package(bisect_ppx) diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml deleted file mode 100644 index b9921a0c3..000000000 --- a/ocaml_emulator/platform.ml +++ /dev/null @@ -1,197 +0,0 @@ -open Sail_lib;; -module P = Platform_impl;; -module Elf = Elf_loader;; - -(* Platform configuration *) - -let config_enable_rvc = ref true -let config_enable_next = ref false -let config_enable_writable_misa = ref true -let config_enable_dirty_update = ref false -let config_enable_misaligned_access = ref false -let config_mtval_has_illegal_inst_bits = ref false -let config_enable_svinval = ref false -let config_enable_zcb = ref false -let config_enable_writable_fiom = ref true -let config_enable_vext = ref true -let config_enable_bext = ref false -let config_enable_zicbom = ref false -let config_enable_zicboz = ref false -let config_pmp_count = ref Big_int.zero -let config_pmp_grain = ref Big_int.zero - -let set_config_pmp_count x = config_pmp_count := Big_int.of_int x -let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x - -let platform_arch = ref P.RV64 - -(* logging *) - -let config_print_instr = ref true -let config_print_step = ref false -let config_print_reg = ref true -let config_print_mem_access = ref true -let config_print_platform = ref true - -let print_instr s = - if !config_print_instr - then print_endline s - else () - -let print_step () = - if !config_print_step - then print_endline "" - else () - -let print_reg s = - if !config_print_reg - then print_endline s - else () - -let print_mem_access s = - if !config_print_mem_access - then print_endline s - else () - -let print_platform s = - if !config_print_platform - then print_endline s - else () - -let get_config_print_instr () = !config_print_instr -let get_config_print_reg () = !config_print_reg -let get_config_print_mem () = !config_print_mem_access -let get_config_print_platform () = !config_print_platform - -(* Mapping to Sail externs *) -let cur_arch_bitwidth () = - match !platform_arch with - | P.RV64 -> Big_int.of_int 64 - | P.RV32 -> Big_int.of_int 32 - -let arch_bits_of_int i = - get_slice_int (cur_arch_bitwidth (), Big_int.of_int i, Big_int.zero) - -let arch_bits_of_int64 i = - get_slice_int (cur_arch_bitwidth (), Big_int.of_int64 i, Big_int.zero) - -let rom_size_ref = ref 0 -let make_rom arch start_pc = - let reset_vec = - List.concat (List.map P.uint32_to_bytes (P.reset_vec_int arch start_pc)) in - let dtb = P.make_dtb (P.make_dts arch) in - let rom = reset_vec @ dtb in - ( rom_size_ref := List.length rom; - (* - List.iteri (fun i c -> - print_mem_access "rom[0x%Lx] <- %x\n" - (Int64.add P.rom_base (Int64.of_int i)) - c - ) rom; - *) - rom ) - -let enable_writable_misa () = !config_enable_writable_misa -let enable_rvc () = !config_enable_rvc -let enable_next () = !config_enable_next -let enable_fdext () = false -let enable_vext () = !config_enable_vext -let enable_bext () = !config_enable_bext -let enable_zicbom () = !config_enable_zicbom -let enable_zicboz () = !config_enable_zicboz -let enable_dirty_update () = !config_enable_dirty_update -let enable_misaligned_access () = !config_enable_misaligned_access -let mtval_has_illegal_inst_bits () = !config_mtval_has_illegal_inst_bits -let enable_svinval () = !config_enable_svinval -let enable_zcb () = !config_enable_zcb -let enable_zfinx () = false -let enable_writable_fiom () = !config_enable_writable_fiom -let pmp_count () = !config_pmp_count -let pmp_grain () = !config_pmp_grain - -let rom_base () = arch_bits_of_int64 P.rom_base -let rom_size () = arch_bits_of_int !rom_size_ref - -let dram_base () = arch_bits_of_int64 P.dram_base -let dram_size () = arch_bits_of_int64 !P.dram_size_ref - -let cache_block_size_exp () = Big_int.of_int64 !P.cache_block_size_exp_ref - -let clint_base () = arch_bits_of_int64 P.clint_base -let clint_size () = arch_bits_of_int64 P.clint_size - -let insns_per_tick () = Big_int.of_int P.insns_per_tick - -let htif_tohost () = - arch_bits_of_int64 (Big_int.to_int64 (Elf.elf_tohost ())) - -(* Entropy Source - get random bits *) - -(* This function can be changed to support deterministic sequences of - pseudo-random bytes. This is useful for testing. *) -let get_16_random_bits () = arch_bits_of_int (Random.int 0xFFFF) - -(* load reservation *) - -let speculate_conditional () = true - -let reservation = ref "none" (* shouldn't match any valid address *) - -let load_reservation addr = - print_platform (Printf.sprintf "reservation <- %s\n" (string_of_bits addr)); - reservation := string_of_bits addr - -let match_reservation addr = - print_platform (Printf.sprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr)); - string_of_bits addr = !reservation - -let cancel_reservation () = - print_platform (Printf.sprintf "reservation <- none\n"); - reservation := "none" - -let read_mem (rk, addrsize, addr, len) = - Sail_lib.fast_read_ram (len, addr) - -let write_mem_ea _ = () - -let write_mem (wk, addrsize, addr, len, value) = - Sail_lib.write_ram' (len, Sail_lib.uint addr, value); true - -let excl_res _ = true - -let barrier _ = () - -(* terminal I/O *) - -let term_write char_bits = - let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in - P.term_write (char_of_int (Big_int.to_int big_char)) - -let term_read () = - let c = P.term_read () in - arch_bits_of_int (int_of_char c) - -(* physical memory *) - -let get_mem_bytes addr len = - read_mem_bytes addr len - -(* returns starting value for PC, i.e. start of reset vector *) -let init arch elf_file = - platform_arch := arch; - Elf.load_elf elf_file; - - print_platform (Printf.sprintf "\nRegistered htif_tohost at 0x%Lx.\n" (Big_int.to_int64 (Elf.elf_tohost ()))); - print_platform (Printf.sprintf "Registered clint at 0x%Lx (size 0x%Lx).\n%!" P.clint_base P.clint_size); - - let start_pc = Elf.Big_int.to_int64 (Elf.elf_entry ()) in - let rom = make_rom arch start_pc in - let rom_base = Big_int.of_int64 P.rom_base in - let rec write_rom ofs = function - | [] -> () - | h :: tl -> let addr = Big_int.add rom_base (Big_int.of_int ofs) in - (wram addr h); - write_rom (ofs + 1) tl - in ( write_rom 0 rom; - get_slice_int (cur_arch_bitwidth (), rom_base, Big_int.zero) - ) diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml deleted file mode 100644 index 2732d9468..000000000 --- a/ocaml_emulator/platform_impl.ml +++ /dev/null @@ -1,220 +0,0 @@ -(* architecture *) - -type arch = - | RV32 - | RV64 - -let str_of_arch = function - | RV32 -> "RV32" - | RV64 -> "RV64" - -(* int->byte converters in little-endian order *) - -let uint32_to_bytes u = let open Int32 in - List.map to_int - [ logand u 0xffl; - logand (shift_right u 8) 0xffl; - logand (shift_right u 16) 0xffl; - logand (shift_right u 24) 0xffl; - ] - -let uint64_to_bytes u = let open Int64 in - List.map to_int - [ logand u 0xffL; - logand (shift_right u 8) 0xffL; - logand (shift_right u 16) 0xffL; - logand (shift_right u 24) 0xffL; - logand (shift_right u 32) 0xffL; - logand (shift_right u 40) 0xffL; - logand (shift_right u 48) 0xffL; - logand (shift_right u 56) 0xffL; - ] - -(* reset vector for the rom *) - -let reset_vec_size = 8l;; - -let reset_vec_int arch start_pc = [ - 0x297l; (* auipc t0, 0x0 *) - (let open Int32 in - add 0x28593l (shift_left (mul reset_vec_size 4l) 20)); (* addi a1, t0, ofs(dtb) *) - 0xf1402573l; (* csrr a0, mhartid *) - (match arch with - | RV32 -> 0x0182a283l (* lw t0, 24(t0) *) - | RV64 -> 0x0182b283l); (* ld t0, 24(t0) *) - 0x28067l; (* jr t0 *) - 0x0l; - (let open Int64 in to_int32 (logand start_pc 0xffffffffL)); - (let open Int64 in to_int32 (shift_right_logical start_pc 32)); -] - -(* address map *) - -let dram_base = 0x80000000L;; (* Spike::DRAM_BASE *) -let clint_base = 0x02000000L;; (* Spike::CLINT_BASE *) -let clint_size = 0x000c0000L;; (* Spike::CLINT_SIZE *) -let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) - -let dram_size_ref = ref (Int64.(shift_left 64L 20)) - -(* Default 64, which is mandated by RVA22. *) -let cache_block_size_exp_ref = ref (Int64.(6L)) - -type mem_region = { - addr : Int64.t; - size : Int64.t -} - -(* dts from spike *) -let spike_dts isa_spec mmu_spec cpu_hz insns_per_rtc_tick mems = - "/dts-v1/;\n" - ^ "\n" - ^ "/ {\n" - ^ " #address-cells = <2>;\n" - ^ " #size-cells = <2>;\n" - ^ " compatible = \"ucbbar,spike-bare-dev\";\n" - ^ " model = \"ucbbar,spike-bare\";\n" - ^ " cpus {\n" - ^ " #address-cells = <1>;\n" - ^ " #size-cells = <0>;\n" - ^ " timebase-frequency = <" ^ string_of_int (cpu_hz/insns_per_rtc_tick) ^ ">;\n" - ^ " CPU0: cpu@0 {\n" - ^ " device_type = \"cpu\";\n" - ^ " reg = <0>;\n" - ^ " status = \"okay\";\n" - ^ " compatible = \"riscv\";\n" - ^ " riscv,isa = \"" ^ isa_spec ^ "\";\n" - ^ " mmu-type = \"riscv," ^ mmu_spec ^ "\";\n" - ^ " clock-frequency = <" ^ string_of_int cpu_hz ^ ">;\n" - ^ " CPU0_intc: interrupt-controller {\n" - ^ " #interrupt-cells = <1>;\n" - ^ " interrupt-controller;\n" - ^ " compatible = \"riscv,cpu-intc\";\n" - ^ " };\n" - ^ " };\n" - ^ " };\n" - ^ (List.fold_left (^) "" - (List.map (fun m -> - " memory@" ^ Printf.sprintf "%Lx" m.addr ^ " {\n" - ^ " device_type = \"memory\";\n" - ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.addr 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.addr 0xffffffffL) - ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical m.size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand m.size 0xffffffffL) ^ ">;\n" - ^ " };\n") mems)) - ^ " soc {\n" - ^ " #address-cells = <2>;\n" - ^ " #size-cells = <2>;\n" - ^ " compatible = \"ucbbar,spike-bare-soc\", \"simple-bus\";\n" - ^ " ranges;\n" - ^ " clint@" ^ Printf.sprintf "%Lx" clint_base ^ " {\n" - ^ " compatible = \"riscv,clint0\";\n" - ^ " interrupts-extended = <&CPU0_intc 3 &CPU0_intc 7 >;\n" - ^ " reg = <0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_base 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_base 0xffffffffL) - ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(shift_right_logical clint_size 32) ^ " 0x" ^ Printf.sprintf "%Lx" Int64.(logand clint_size 0xffffffffL) ^ ">;\n" - ^ " };\n" - ^ " };\n" - ^ " htif {\n" - ^ " compatible = \"ucb,htif0\";\n" - ^ " };\n" - ^ "};\n" - -let cpu_hz = 1000000000;; -let insns_per_tick = 100;; - -let make_mems () = [{ addr = dram_base; - size = !dram_size_ref }];; - -let make_dts arch = - let isa, mmu = match arch with - | RV64 -> "rv64imac", "sv39" - | RV32 -> "rv32imac", "sv32" in - spike_dts isa mmu cpu_hz insns_per_tick (make_mems ());; - -let bytes_to_string bytes = - String.init (List.length bytes) (fun i -> Char.chr (List.nth bytes i)) - -let dtc_path = ref "/usr/bin/dtc" - -let set_dtc path = - try let st = Unix.stat path in - if st.Unix.st_kind = Unix.S_REG && st.Unix.st_perm != 0 - then dtc_path := path - else ( Printf.eprintf "%s doesn't seem like a valid executable.\n%!" path; - exit 1) - with Unix.Unix_error (e, _, _) -> - ( Printf.eprintf "Error accessing %s: %s\n%!" path (Unix.error_message e); - exit 1) - -let set_dram_size mb = - dram_size_ref := Int64.(shift_left (Int64.of_int mb) 20) - -(* Calculate x=log2(n) and return Some(x) if n is a power of 2, otherwise None. *) -let log2 n = - let rec loop i = - if i >= Sys.int_size - 1 then None - else if (1 lsl i) = n then Some i - else loop (i + 1) - in - if n <= 0 then None else loop 0 - -let set_cache_block_size b = - match log2 b with - | Some(block_size_exp) -> cache_block_size_exp_ref := Int64.(Int64.of_int block_size_exp) - | None -> (Printf.eprintf "Invalid cache block size provided."; exit 1) - -let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) - try - let cmd = Printf.sprintf "%s -I dts" !dtc_path in - let (cfrom, cto, cerr) = - Unix.open_process_full cmd [||] - in ( - output_string cto dts; - (* print_endline " sent dts to dtc ..."; *) - close_out cto; - (* simple and stupid for now *) - let rec accum_bytes cin acc = - match ( - try Some (input_byte cin) - with End_of_file -> None - ) with - | Some b -> accum_bytes cin (b :: acc) - | None -> List.rev acc - in - (* let _ = print_endline " accumulating dtb ..." in *) - let dtb = accum_bytes cfrom [] in - (* let _ = print_endline " accumulating emsg ..." in *) - let emsg = bytes_to_string (accum_bytes cerr []) in - match Unix.close_process_full (cfrom, cto, cerr) with - | Unix.WEXITED 0 -> dtb - | _ -> (Printf.printf "%s\n%!" ("Error executing dtc: " ^ emsg); - exit 1) - ) - with Unix.Unix_error (e, fn, _) -> - (Printf.printf "%s\n" ("Error executing dtc: " ^ fn ^ ": " ^ Unix.error_message e); - exit 1) - -(* Terminal I/O *) - -let term_write char = - ignore (Unix.write_substring Unix.stderr (String.make 1 char) 0 1) - -let rec term_read () = - let buf = Bytes.make 1 '\000' in - let nbytes = Unix.read Unix.stdin buf 0 1 in - (* todo: handle nbytes == 0 *) - Bytes.get buf 0 - -(* Platform diagnostics *) - -let show_bytes s = - output_string stdout s - -let dump_dts arch = show_bytes (make_dts arch) -let dump_dtb arch = show_bytes (bytes_to_string (make_dtb (make_dts arch))) - -(* -let save_string_to_file s fname = - let out = open_out fname in - output_string out s; - close_out out;; - - *) diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml deleted file mode 100644 index 20eaef66f..000000000 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ /dev/null @@ -1,211 +0,0 @@ -open Sail_lib -open Riscv -module PI = Platform_impl -module P = Platform -module Elf = Elf_loader - -(* OCaml driver for generated RISC-V model. *) - -let opt_file_arguments = ref ([] : string list) - -let opt_dump_dts = ref false -let opt_dump_dtb = ref false -let opt_signature_file = ref (None : string option) -let signature_granularity_ref = ref 4 -let opt_isa = ref (None : string option) - -let report_arch () = - Printf.printf "RV%d\n" (Big_int.to_int Riscv.zxlen_val); - exit 0 - -let set_signature_file s = - opt_signature_file := Some s; - (* turn off logging *) - P.config_print_instr := false; - P.config_print_reg := false; - P.config_print_mem_access := false; - P.config_print_platform := false - -let set_signature_granularity sg = - signature_granularity_ref := sg - -let options = Arg.align ([("-dump-dts", - Arg.Set opt_dump_dts, - " dump the platform device-tree source to stdout"); - ("-dump-dtb", - Arg.Set opt_dump_dtb, - " dump the *binary* platform device-tree blob to stdout"); - ("-enable-dirty-update", - Arg.Set P.config_enable_dirty_update, - " enable dirty-bit update during page-table walks"); - ("-enable-misaligned-access", - Arg.Set P.config_enable_misaligned_access, - " enable misaligned accesses without M-mode traps"); - ("-pmp-count", - Arg.Int P.set_config_pmp_count, - " number of supported PMPs (0, 16, 64)"); - ("-pmp-grain", - Arg.Int P.set_config_pmp_grain, - " exponent of granularity of PMP addresses (G in the spec)"); - ("-enable-next", - Arg.Set P.config_enable_next, - " enable N extension"); - ("-mtval-has-illegal-inst-bits", - Arg.Set P.config_mtval_has_illegal_inst_bits, - " mtval stores instruction bits on an illegal instruction exception"); - ("-enable-svinval", - Arg.Set P.config_enable_svinval, - " enable Svinval extension"); - ("-enable-zcb", - Arg.Set P.config_enable_zcb, - " enable Zcb (simple code size) extension"); - ("-enable-writable-fiom", - Arg.Set P.config_enable_writable_fiom, - " enable FIOM (Fence of I/O implies Memory) bit in menvcfg"); - ("-disable-rvc", - Arg.Clear P.config_enable_rvc, - " disable the RVC extension on boot"); - ("-disable-vext", - Arg.Clear P.config_enable_vext, - " disable the RVV extension on boot"); - ("-enable-bext", - Arg.Clear P.config_enable_bext, - " enable the B extension on boot"); - ("-enable-zicbom", - Arg.Set P.config_enable_zicbom, - " enable the Zicbom extension"); - ("-enable-zicboz", - Arg.Set P.config_enable_zicboz, - " enable the Zicboz extension"); - ("-disable-writable-misa-c", - Arg.Clear P.config_enable_writable_misa, - " leave misa hardwired to its initial value"); - ("-ram-size", - Arg.Int PI.set_dram_size, - " size of physical ram memory to use (in MB)"); - ("-cache-block-size", - Arg.Int PI.set_cache_block_size, - " cache block size of the cache block size (default 64; max 4096)"); - ("-report-arch", - Arg.Unit report_arch, - " report model architecture (RV32 or RV64)"); - ("-test-signature", - Arg.String set_signature_file, - " file for signature output (requires ELF signature symbols)"); - ("-signature-granularity", - Arg.Int set_signature_granularity, - " test signature granularity (in bytes)"); - ("-trace-delimit-step", - Arg.Set P.config_print_step, - " delimit instructions in the trace output"); - ("-isa", - Arg.String (fun s -> opt_isa := Some s), - " requested isa"); - ("-with-dtc", - Arg.String PI.set_dtc, - " full path to dtc to use") - ]) - -let usage_msg = "RISC-V platform options:" - -(* ELF architecture checks *) - -let get_arch () = - match Big_int.to_int Riscv.zxlen_val with - | 64 -> PI.RV64 - | 32 -> PI.RV32 - | n -> failwith (Printf.sprintf "Unknown model architecture RV%d" n) - -let str_of_elf = function - | Elf.ELF_Class_64 -> "ELF64" - | Elf.ELF_Class_32 -> "ELF32" - -let elf_arg = - Arg.parse options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) - usage_msg; - if !opt_dump_dts then (PI.dump_dts (get_arch ()); exit 0); - if !opt_dump_dtb then (PI.dump_dtb (get_arch ()); exit 0); - ( match !opt_file_arguments with - | f :: _ -> prerr_endline ("Sail/RISC-V: running ELF file " ^ f); f - | _ -> (prerr_endline "Please provide an ELF file."; exit 0) - ) - -let check_elf () = - match (get_arch (), Elf.elf_class ()) with - | (PI.RV64, Elf.ELF_Class_64) -> - P.print_platform "RV64 model loaded ELF64.\n" - | (PI.RV32, Elf.ELF_Class_32) -> - P.print_platform "RV32 model loaded ELF32.\n" - | (a, e) -> - (let msg = Printf.sprintf "\n%s model cannot execute %s.\n" (PI.str_of_arch a) (str_of_elf e) in - Printf.eprintf "%s" msg; - exit 1) - -(* post execution handlers *) - -let write_bytes fl bytes = - let i = ref 0 in - while !i < Bytes.length bytes do - for j = !signature_granularity_ref - 1 downto 0 do - let s = Printf.sprintf "%02x" - (int_of_char (Bytes.get bytes (!i + j))) in - output_string fl s; - done; - output_string fl "\n"; - i := !i + !signature_granularity_ref; - done - -let write_signature f sig_start sig_end = - let b = Big_int.to_int sig_start in - let len = Big_int.to_int sig_end - b in - let sig_bytes = P.get_mem_bytes sig_start len in - let sig_file = open_out f in - write_bytes sig_file sig_bytes; - close_out sig_file - -let dump_signature () = - match !opt_signature_file with - | None -> () - | Some f -> - match (Elf.elf_symbol "begin_signature", - Elf.elf_symbol "end_signature") with - | Some b, Some e -> write_signature f b e - | None, _ -> Printf.eprintf "no begin_signature symbol in ELF" - | _, None -> Printf.eprintf "no end_signature symbol in ELF" - -let show_times init_s init_e run_e insts = - let init_time = init_e.Unix.tms_utime -. init_s.Unix.tms_utime in - let exec_time = run_e.Unix.tms_utime -. init_e.Unix.tms_utime in - Printf.eprintf "\nInitialization: %g secs\n" init_time; - Printf.eprintf "Execution: %g secs\n" exec_time; - Printf.eprintf "Instructions retired: %Ld\n" insts; - Printf.eprintf "Perf: %g ips\n" ((Int64.to_float insts) /. exec_time) - -(* model execution *) - -let run pc = - sail_call - (fun r -> - try ( zinit_model (); - zPC := pc; - zloop () - ) - with - | ZError_not_implemented (zs) -> - print_string ("Error: Not implemented: ", zs) - | ZError_internal_error (_) -> - prerr_endline "Error: internal error" - ) - -let () = - Random.self_init (); - - let init_start = Unix.times () in - let pc = Platform.init (get_arch ()) elf_arg in - let _ = check_elf () in - let init_end = Unix.times () in - let _ = run pc in - let run_end = Unix.times () in - let insts = Big_int.to_int64 (uint (!Riscv.zminstret)) in - dump_signature (); - show_times init_start init_end run_end insts diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml deleted file mode 100644 index 2b98751a4..000000000 --- a/ocaml_emulator/softfloat.ml +++ /dev/null @@ -1,198 +0,0 @@ - -let f16_add rm v1 v2 = - () - -let f16_sub rm v1 v2 = - () - -let f16_mul rm v1 v2 = - () - -let f16_div rm v1 v2 = - () - -let f32_add rm v1 v2 = - () - -let f32_sub rm v1 v2 = - () - -let f32_mul rm v1 v2 = - () - -let f32_div rm v1 v2 = - () - -let f64_add rm v1 v2 = - () - -let f64_sub rm v1 v2 = - () - -let f64_mul rm v1 v2 = - () - -let f64_div rm v1 v2 = - () - -let f16_muladd rm v1 v2 v3 = - () - -let f32_muladd rm v1 v2 v3 = - () - -let f64_muladd rm v1 v2 v3 = - () - -let f16_sqrt rm v = - () - -let f32_sqrt rm v = - () - -let f64_sqrt rm v = - () - -let f16_to_i32 rm v = - () - -let f16_to_ui32 rm v = - () - -let i32_to_f16 rm v = - () - -let ui32_to_f16 rm v = - () - -let f16_to_i64 rm v = - () - -let f16_to_ui64 rm v = - () - -let i64_to_f16 rm v = - () - -let ui64_to_f16 rm v = - () - -let f32_to_i32 rm v = - () - -let f32_to_ui32 rm v = - () - -let i32_to_f32 rm v = - () - -let ui32_to_f32 rm v = - () - -let f32_to_i64 rm v = - () - -let f32_to_ui64 rm v = - () - -let i64_to_f32 rm v = - () - -let ui64_to_f32 rm v = - () - -let f64_to_i32 rm v = - () - -let f64_to_ui32 rm v = - () - -let i32_to_f64 rm v = - () - -let ui32_to_f64 rm v = - () - -let f64_to_i64 rm v = - () - -let f64_to_ui64 rm v = - () - -let i64_to_f64 rm v = - () - -let ui64_to_f64 rm v = - () - -let f16_to_f32 rm v = - () - -let f16_to_f64 rm v = - () - -let f32_to_f64 rm v = - () - -let f32_to_f16 rm v = - () - -let f64_to_f16 rm v = - () - -let f64_to_f32 rm v = - () - -let f16_lt v1 v2 = - () - -let f16_lt_quiet v1 v2 = - () - -let f16_le v1 v2 = - () - -let f16_le_quiet v1 v2 = - () - -let f16_eq v1 v2 = - () - -let f32_lt v1 v2 = - () - -let f32_lt_quiet v1 v2 = - () - -let f32_le v1 v2 = - () - -let f32_le_quiet v1 v2 = - () - -let f32_eq v1 v2 = - () - -let f64_lt v1 v2 = - () - -let f64_lt_quiet v1 v2 = - () - -let f64_le v1 v2 = - () - -let f64_le_quiet v1 v2 = - () - -let f64_eq v1 v2 = - () - -let f16_round_to_int exact rm v = - () - -let f32_round_to_int exact rm v = - () - -let f64_round_to_int exact rm v = - () diff --git a/ocaml_emulator/tracecmp.ml b/ocaml_emulator/tracecmp.ml deleted file mode 100644 index 5ce397068..000000000 --- a/ocaml_emulator/tracecmp.ml +++ /dev/null @@ -1,358 +0,0 @@ -(* Simple trace comparison checker *) - -type arch = - | RV32 - | RV64 - -type csr_read = { - csrr : string; - rdval : int64 -} - -type csr_write = { - csrw : string; - wrval : int64 -} - -type reg_write = { - reg : int; - rval : int64 -} - -type mem_op = { - vaddr : int64; - paddr : int64; - mval : int64 -} - -type inst = { - count : int; - priv : char; - pc : int64; - inst: int32 -} - -type tick = { - time : int64 -} - -type htif = { - tohost : int64 -} - -type ld_res = - | Res_make of int64 - | Res_match of int64 * int64 - | Res_cancel - -type line = - | L_none - | L_inst of inst - | L_reg_write of reg_write - | L_csr_read of csr_read - | L_csr_write of csr_write - | L_mem_read of mem_op - | L_mem_write of mem_op - | L_tick of tick - | L_htif of htif - | L_ld_res of ld_res - -(* architectural support *) -let sail_arch = ref RV64 - -let arch_val v = - match !sail_arch with - | RV64 -> v - | RV32 -> Int64.logand v 0xFFFFFFFFL (* only lowest 32-bits *) - -let inst_count = ref 0 - -(* csr reads - CSR mscratch -> 0x0000000000000000 - *) - -let parse_csr_read l = - try Scanf.sscanf l " CSR %s -> 0x%Lx" - (fun csrr rdval -> L_csr_read { csrr; rdval = arch_val rdval }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_csr_read r = - Printf.sprintf "CSR %s -> 0x%Lx" r.csrr r.rdval - -(* csr writes - CSR mstatus <- 0x0000000a00020800 (input: 0x0000000a00020800) - *) - -let parse_csr_write l = - try Scanf.sscanf l " CSR %s <- 0x%Lx " - (fun csrw wrval -> L_csr_write { csrw; wrval = arch_val wrval }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_csr_write r = - Printf.sprintf "CSR %s <- 0x%Lx " r.csrw r.wrval - -(* mem reads - mem[V:0x0000000080001000, P:0x0000000080001000] -> 0x0000000000000000 - *) - -(* exclusion list, to avoid comparing reads to mmio htif port by spike *) -let mem_addr_excludes = [ 0x80001000L ] -let parse_mem_read l = - try Scanf.sscanf l " mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx" - (fun va pa v -> - if List.mem va mem_addr_excludes || List.mem pa mem_addr_excludes - then L_none - else L_mem_read { vaddr = arch_val va; paddr = arch_val pa; mval = arch_val v }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_mem_read r = - Printf.sprintf "mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx" r.vaddr r.paddr r.mval - -(* mem writes - mem[V:0x0000000080001000, P:0x0000000080001000] <- 0x0000000000000000 - *) - -let parse_mem_write l = - try Scanf.sscanf l " mem[V:0x%Lx, P:0x%Lx] <- 0x%Lx" - (fun va pa v -> - L_mem_write { vaddr = arch_val va; paddr = arch_val pa; mval = arch_val v }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_mem_write r = - Printf.sprintf "mem[V:0x%Lx, P:0x%Lx] -> 0x%Lx" r.vaddr r.paddr r.mval - -(* reg writes - x16 <- 0x0000000000000000 - *) - -let parse_reg_write l = - try Scanf.sscanf l " x%u <- 0x%Lx" - (fun reg rval -> L_reg_write { reg; rval = arch_val rval }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_reg_write r = - Printf.sprintf "x%u <- 0x%Lx" r.reg r.rval - -(* instructions *) - -let sprint_inst r = - Printf.sprintf "[%u] [%c]: 0x%Lx (0x%lx)" r.count r.priv r.pc r.inst - -(* sail instruction line: - [13000] [M]: 0x0000000080000E4A (0x0107971B) slli a4, a5, 0b10000 - *) - -let parse_sail_inst l = - try Scanf.sscanf l " [%u] [%c]: 0x%Lx (0x%lx) %s" - (fun count priv pc inst _ -> - inst_count := count; - L_inst { count; priv; pc; inst }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -(* spike instruction line: - [2] core 0 [M]: 0x0000000000001008 (0xf1402573) csrr a0, mhartid - *) - -let parse_spike_inst l = - try Scanf.sscanf l " [%u] core 0 [%c]: 0x%Lx (0x%lx) %s" - (fun count priv pc inst _ -> - inst_count := count; - L_inst { count; priv; pc = arch_val pc; inst }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -(* clock tick - clint::tick mtime <- 0x1 - *) - -let parse_tick l = - try Scanf.sscanf l " clint::tick mtime <- 0x%Lx" - (fun time -> L_tick { time }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_tick t = - Printf.sprintf "clint::tick mtime <- 0x%Lx" t.time - -(* htif tick - htif::tick 0x1 - *) - -let parse_htif l = - try Scanf.sscanf l " htif::tick 0x%Lx" - (fun tohost -> L_htif { tohost }) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_htif t = - Printf.sprintf "htif::tick 0x%Lx" t.tohost - -(* Load reservations: - make: reservation <- 0x80002008 - match: reservation: 0xffffffffffffffff, key=0x80002008 - cancel: reservation <- none - - *) -let parse_ldres_match l = - try Scanf.sscanf - l " reservation: 0x%Lx, key=0x%Lx" - (fun res key -> L_ld_res (Res_match (res, key))) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let parse_ldres_match_sail l = - try Scanf.sscanf - l " reservation: none, key=0x%Lx" - (fun key -> L_ld_res (Res_match (Int64.minus_one, key))) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let parse_ldres_change l = - try if l = "reservation <- none" - then L_ld_res Res_cancel - else Scanf.sscanf - l " reservation <- 0x%Lx" - (fun res -> L_ld_res (Res_make res)) - with - | Scanf.Scan_failure _ -> L_none - | End_of_file -> L_none - -let sprint_ldres = function - | Res_make res -> Printf.sprintf "reservation <- 0x%Lx" res - | Res_match (res, key) -> Printf.sprintf "reservation: 0x%Lx, key=0x%Lx" res key - | Res_cancel -> Printf.sprintf "reservation <- none" - -(* scanners *) - -let popt p l = function - | L_none -> p l - | res -> res - -let parse_line l = - parse_csr_read l |> popt parse_csr_write l - |> popt parse_reg_write l |> popt parse_tick l |> popt parse_htif l - |> popt parse_ldres_change l |> popt parse_ldres_match l - -let parse_sail_line l = - parse_line l |> popt parse_sail_inst l |> popt parse_ldres_match_sail l - -let parse_spike_line l = - parse_line l |> popt parse_spike_inst l - -(* printer *) -let sprint_line = function - | L_none -> "" - | L_inst i -> sprint_inst i - | L_reg_write r -> Printf.sprintf "<%d> %s" !inst_count (sprint_reg_write r) - | L_csr_read r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_read r) - | L_csr_write r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_write r) - | L_mem_read m -> Printf.sprintf "<%d> %s" !inst_count (sprint_mem_read m) - | L_mem_write m -> Printf.sprintf "<%d> %s" !inst_count (sprint_mem_write m) - | L_tick t -> Printf.sprintf "<%d> %s" !inst_count (sprint_tick t) - | L_htif t -> Printf.sprintf "<%d> %s" !inst_count (sprint_htif t) - | L_ld_res r -> Printf.sprintf "<%d> %s" !inst_count (sprint_ldres r) - -(* file processing *) - -let rec get_line ch parse = - let line = try Some (input_line ch) - with End_of_file -> None in - match line with - | Some l -> (match parse l with - | L_none -> get_line ch parse - | r -> r - ) - | None -> L_none - -let rec print_lines ch parse = - match (get_line ch parse) with - | L_none -> () - | l -> (print_endline (sprint_line l); - print_lines ch parse) - - -let lines_matched k l = - match k, l with - (* Special case for CSR writes to sie/sip/sstatus, since spike - * does a recursive call which messes the trace log. For these - * registers, we just match the final written value, and need to - * unfortunately ignore the input value. - *) - | L_csr_write kw, L_csr_write lw -> - if ( (kw.csrw = "mie" && lw.csrw = "sie") - || (kw.csrw = "mip" && lw.csrw = "sip") - || (kw.csrw = "mstatus" && lw.csrw = "sstatus")) - then kw.wrval = lw.wrval - else kw = lw - | _, _ -> k = l - -let rec compare_traces k l cnt = - let kro = get_line k parse_spike_line in - let lro = get_line l parse_sail_line in - match kro, lro with - | L_none, L_none -> - print_endline (Printf.sprintf "Matched %d instructions" cnt) - | L_none, lr -> - print_endline "Spike: not reached"; - print_endline ("Sail: " ^ sprint_line lr); - exit 1 - | kr, L_none -> - print_endline ("Spike: " ^ sprint_line kr); - print_endline "Sail: not reached"; - exit 1 - | kr, lr -> - if lines_matched kr lr - then compare_traces k l (cnt + 1) - else (print_endline ("Spike: " ^ sprint_line kr); - print_endline ("Sail: " ^ sprint_line lr); - exit 1) - -let spike_log = ref (None : string option) -let sail_log = ref (None : string option) -let uncompress = ref false - -let in_file f = - if !uncompress - then Unix.open_process_in ("gunzip -c " ^ f) - else open_in f - -let options = - Arg.align ([( "-z", - Arg.Set uncompress, - " uncompress trace files"); - ( "-rv32", - Arg.Unit (fun f -> sail_arch := RV32), - " sail architecture"); - ( "-k", - Arg.String (fun f -> spike_log := Some f), - " spike trace log"); - ( "-l", - Arg.String (fun f -> sail_log := Some f), - " sail trace log")]) -let usage = "usage: tracecmp [options]\n" - -let _ = - Arg.parse options (fun s -> print_endline usage; exit 0) - usage; - match !spike_log, !sail_log with - | None, None -> (print_endline usage; exit 0) - | Some l, None -> print_lines (in_file l) parse_spike_line - | None, Some l -> print_lines (in_file l) parse_sail_line - | Some k, Some l -> compare_traces (in_file k) (in_file l) 0 diff --git a/opam b/opam deleted file mode 100644 index a53d1088b..000000000 --- a/opam +++ /dev/null @@ -1,32 +0,0 @@ -opam-version: "2.0" -name: "sail-riscv" -version: "0.5" -maintainer: "Sail Devs " -authors: [ - "Alasdair Armstrong" - "Thomas Bauereiss" - "Brian Campbell" - "Shaked Flur" - "Jonathan French" - "Prashanth Mundkur" - "Robert Norton" - "Christopher Pulte" - "Peter Sewell" -] -homepage: "https://github.com/rems-project/sail-riscv/" -bug-reports: "https://github.com/rems-project/sail-riscv/issues" -license: "BSD3" -dev-repo: "git+https://github.com/rems-project/sail-riscv.git" -build: [make "LEM_DIR=%{lem:share}%" "SAIL_DIR=%{sail:share}%" "SAIL=sail" "opam-build"] -depends: [ - "ocaml" {>= "4.06.1"} - "ocamlfind" - "ocamlbuild" - "lem" - "sail" {>= "0.9"} - "linksem" {>= "0.3"} - "conf-gmp" - "conf-zlib" -] -synopsis: - "This package installs a RISC-V emulator (32 and 64 bits) built form the Sail model at https://github.com/rems-project/sail-riscv" diff --git a/os-boot/README.md b/os-boot/README.md index 087abacc5..921dd6575 100644 --- a/os-boot/README.md +++ b/os-boot/README.md @@ -35,15 +35,6 @@ performance and benchmarking a model without any execution tracing is available on the optimize branch (`git checkout optimize`) of this repository. This currently requires the latest Sail built from source. -Booting Linux with the OCaml backend ------------------------------------- - -The OCaml model only needs the ELF-version of the BBL, since it can generate its -own DTB. -``` -$ ./ocaml_emulator/riscv_ocaml_sim_ bbl > execution-trace.log 2> console.log -``` - Caveats for OS boot ------------------- diff --git a/test/run_tests.sh b/test/run_tests.sh index 8c0f03f2f..d8016fac5 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -55,31 +55,6 @@ cd $RISCVDIR make clean printf "Building 32-bit RISCV specification...\n" -if ARCH=RV32 make ocaml_emulator/riscv_ocaml_sim_RV32 ; -then - green "Building 32-bit RISCV OCaml emulator" "ok" -else - red "Building 32-bit RISCV OCaml emulator" "fail" -fi -for test in $DIR/riscv-tests/rv32*.elf; do - # skip F/D tests on OCaml for now - pat='rv32ud-.+elf' - if [[ $(basename $test) =~ $pat ]]; - then continue - fi - pat='rv32uf-.+elf' - if [[ $(basename $test) =~ $pat ]]; - then continue - fi - if $RISCVDIR/ocaml_emulator/riscv_ocaml_sim_RV32 "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" - then - green "OCaml-32 $(basename $test)" "ok" - else - red "OCaml-32 $(basename $test)" "fail" - fi -done -finish_suite "32-bit RISCV OCaml tests" - if ARCH=RV32 make c_emulator/riscv_sim_RV32; then @@ -102,31 +77,6 @@ make clean printf "Building 64-bit RISCV specification...\n" -if make ocaml_emulator/riscv_ocaml_sim_RV64 ; -then - green "Building 64-bit RISCV OCaml emulator" "ok" -else - red "Building 64-bit RISCV OCaml emulator" "fail" -fi -for test in $DIR/riscv-tests/rv64*.elf; do - # skip F/D tests on OCaml for now - pat='rv64ud-.+elf' - if [[ $(basename $test) =~ $pat ]]; - then continue - fi - pat='rv64uf-.+elf' - if [[ $(basename $test) =~ $pat ]]; - then continue - fi - if $RISCVDIR/ocaml_emulator/riscv_ocaml_sim_RV64 "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" - then - green "OCaml-64 $(basename $test)" "ok" - else - red "OCaml-64 $(basename $test)" "fail" - fi -done -finish_suite "64-bit RISCV OCaml tests" - if make c_emulator/riscv_sim_RV64; then green "Building 64-bit RISCV C emulator" "ok"