diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-03-05 10:10:57 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-03-05 10:39:03 -0800 |
| commit | 6f549c27b311964bddcb85fa6b71421b15e6e705 (patch) | |
| tree | 2baff2c3df09546a337fbd98fd30915e2ecd8645 | |
| parent | 05a41c1aadfd136f2e3cc1750239e681292fc72a (diff) | |
| download | sail-riscv-6f549c27b311964bddcb85fa6b71421b15e6e705.zip sail-riscv-6f549c27b311964bddcb85fa6b71421b15e6e705.tar.gz sail-riscv-6f549c27b311964bddcb85fa6b71421b15e6e705.tar.bz2 | |
Some fixes to readme and makefile.
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | README.md | 12 |
2 files changed, 11 insertions, 11 deletions
@@ -188,9 +188,9 @@ latex: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/latex $(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS) -generated_definitions/isabelle/ROOT: handwritten_support/ROOT - mkdir -p generated_definitions/isabelle - cp handwritten_support/ROOT generated_definitions/isabelle/ +generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT + mkdir -p generated_definitions/isabelle/$(ARCH) + cp handwritten_support/ROOT generated_definitions/isabelle/$(ARCH)/ generated_definitions/lem/riscv_duopod.lem: $(PRELUDE_SRCS) model/riscv_duopod.sail mkdir -p generated_definitions/lem @@ -211,7 +211,7 @@ endif ifeq ($(wildcard $(SAIL_LIB_DIR)/isabelle),) $(error lib directory of Sail not found. Please set the SAIL_LIB_DIR environment variable) endif - isabelle build -b -d $(LEM_DIR)/isabelle-lib -d $(SAIL_LIB_DIR)/isabelle -d generated_definitions/isabelle Sail-RISC-V + isabelle build -b -d $(LEM_DIR)/isabelle-lib -d $(SAIL_LIB_DIR)/isabelle -d generated_definitions/isabelle/$(ARCH) Sail-RISC-V .PHONY: riscv_isa riscv_isa_build @@ -223,7 +223,7 @@ generated_definitions/lem/$(ARCH)/riscv_sequential.lem: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) $(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) -generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile +generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ handwritten_support/$(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ @@ -90,14 +90,14 @@ have tested Isabelle 2018, Coq 8.8.1, and HOL4 Kananaskis-12. Executing test binaries ----------------------- -The C and OCaml simulators can be used to execute small test RV64 binaries. +The C and OCaml simulators can be used to execute small test binaries. ``` -$ ./ocaml_emulator/riscv_ocaml_sim <elf-file> -$ ./c_emulator/riscv_sim <elf-file> +$ ./ocaml_emulator/riscv_ocaml_sim_<arch> <elf-file> +$ ./c_emulator/riscv_sim_<arch> <elf-file> ``` Some information on additional configuration options for each simulator is available -from `./ocaml_emulator/riscv_ocaml_sim -h` and `./c_emulator/riscv_sim -h`. +from `./ocaml_emulator/riscv_ocaml_sim_<arch> -h` and `./c_emulator/riscv_sim_<arch> -h`. Booting Linux with the C backend -------------------------------- @@ -109,7 +109,7 @@ a DTB (device-tree blob) file describing the platform (say in the file the model should be run as: ``` -$ ./c_emulator/riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ ./c_emulator/riscv_sim_<arch> -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & $ tail -f console.log ``` The `console.log` file contains the console boot messages. For maximum @@ -123,7 +123,7 @@ 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 +$ ./ocaml_emulator/riscv_ocaml_sim_<arch> bbl > execution-trace.log 2> console.log ``` Generating input files for Linux boot |