diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2018-11-30 09:50:31 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2018-11-30 09:50:31 -0800 |
| commit | ef7312708a7af5ffbf43dbee37f614ddf2da58c1 (patch) | |
| tree | 9ee9c81bda0c107542aa3eeecfbee503f7d7a739 | |
| parent | 231b95ba2900beaa9d406c574fed44712b41398e (diff) | |
| download | sail-riscv-ef7312708a7af5ffbf43dbee37f614ddf2da58c1.zip sail-riscv-ef7312708a7af5ffbf43dbee37f614ddf2da58c1.tar.gz sail-riscv-ef7312708a7af5ffbf43dbee37f614ddf2da58c1.tar.bz2 | |
Update default make targets and README.
| -rw-r--r-- | Makefile | 12 | ||||
| -rw-r--r-- | README.md | 36 |
2 files changed, 37 insertions, 11 deletions
@@ -49,7 +49,9 @@ C_LIBS += -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR) C_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib endif -all: platform Riscv.thy +all: platform riscv_sim riscv_isa riscv_coq + +.PHONY: all riscv_coq riscv_isa check: $(SAIL_SRCS) main.sail Makefile $(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) main.sail @@ -113,7 +115,9 @@ Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem riscv_duopod: riscv_duopod_ocaml Riscv_duopod.thy -Riscv.thy: riscv.lem riscv_extras.lem +riscv_isa: Riscv.thy + +Riscv.thy: riscv.lem riscv_extras.lem Makefile lem -isa -outdir . -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ riscv_extras.lem \ riscv_types.lem \ @@ -138,7 +142,9 @@ riscvTheory.uo riscvTheory.ui: riscvScript.sml COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -riscv.v riscv_types.v: $(SAIL_SRCS) +riscv_coq: riscv.v riscv_types.v + +riscv.v riscv_types.v: $(SAIL_SRCS) Makefile $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_SRCS) riscv_duopod.v riscv_duopod_types.v: prelude.sail riscv_duopod.sail $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv_duopod -coq_lib riscv_extras $^ @@ -1,7 +1,23 @@ RISCV Sail Model ================ -This repository contains a model of the RISCV architecture written in [Sail](https://www.cl.cam.ac.uk/~pes20/sail/). It used to be contained in the [Sail repository](https://github.com/rems-project/sail). +This repository contains a model of the RISCV architecture written in +[Sail](https://www.cl.cam.ac.uk/~pes20/sail/). It used to be contained +in the [Sail repository](https://github.com/rems-project/sail). + + +Building the model: +------------------- + +Install Sail via Opam, or build Sail from source and have SAIL_DIR in +your environment pointing to its top-level directory. + +``` +$ make +``` +will build the OCaml simulator in ```platform```, the C simulator in +```riscv_sim```, and the Isabelle model in ```Riscv.thy```, and the Coq +model in ```riscv.v```. Booting Linux with the C backend: --------------------------------- @@ -10,12 +26,14 @@ The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader) that contains the Linux kernel as an embedded payload. It also needs a DTB (device-tree blob) file describing the platform. Once those are available, the model should be run as: +``` +$ ./riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ tail -f console.log +``` -$ ./riscv_sim -b spike.dtb bbl > execution-trace.log 2>&1 & -$ tail -f term.log - -The term.log file contains the console boot messages. - +The ```console.log``` file contains the console boot messages. Some +information on additional configuration options is available from +```./riscv_sim -h```. Booting Linux with the OCaml backend: ------------------------------------- @@ -23,6 +41,8 @@ Booting Linux with the OCaml backend: The OCaml model only needs the ELF-version of the BBL, since it can generate its own DTB. -$ ./platform bbl > execution-trace.log +$ ./platform bbl > execution-trace.log 2> console.log -The console output is sent to stderr. + Some +information on additional configuration options is available from +```./platform -h```. |