diff options
author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-14 18:39:42 -0800 |
---|---|---|
committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-14 19:02:04 -0800 |
commit | 3fdda1f2e054a01c95ff59593a8d67d85770609a (patch) | |
tree | ce460b93f6240d98eaef659dbff2442402ee627d | |
parent | 3c0168526eb9895292a6f92b42f243fce4fd1a9d (diff) | |
download | sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.zip sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.tar.gz sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.tar.bz2 |
Reorganize directory structure.
-rw-r--r-- | Makefile | 184 | ||||
-rw-r--r-- | README.md | 44 | ||||
-rw-r--r-- | c/riscv_config.h (renamed from riscv_config.h) | 0 | ||||
-rw-r--r-- | c/riscv_platform.c (renamed from riscv_platform.c) | 0 | ||||
-rw-r--r-- | c/riscv_platform.h (renamed from riscv_platform.h) | 0 | ||||
-rw-r--r-- | c/riscv_platform_impl.c (renamed from riscv_platform_impl.c) | 0 | ||||
-rw-r--r-- | c/riscv_platform_impl.h (renamed from riscv_platform_impl.h) | 0 | ||||
-rw-r--r-- | c/riscv_prelude.c (renamed from riscv_prelude.c) | 0 | ||||
-rw-r--r-- | c/riscv_prelude.h (renamed from riscv_prelude.h) | 0 | ||||
-rw-r--r-- | c/riscv_sail.h (renamed from riscv_sail.h) | 0 | ||||
-rw-r--r-- | c/riscv_sim.c (renamed from riscv_sim.c) | 0 | ||||
-rw-r--r-- | coq/riscv_extras.v (renamed from riscv_extras.v) | 0 | ||||
-rw-r--r-- | hol4/Holmakefile (renamed from Holmakefile) | 0 | ||||
-rw-r--r-- | isabelle/ROOT (renamed from ROOT) | 0 | ||||
-rw-r--r-- | lem/riscv_extras.lem (renamed from riscv_extras.lem) | 0 | ||||
-rw-r--r-- | lem/riscv_extras_sequential.lem (renamed from riscv_extras_sequential.lem) | 0 | ||||
-rw-r--r-- | model/main.sail (renamed from main.sail) | 0 | ||||
-rw-r--r-- | model/main_rvfi.sail (renamed from main_rvfi.sail) | 0 | ||||
-rw-r--r-- | model/prelude.sail (renamed from prelude.sail) | 0 | ||||
-rw-r--r-- | model/riscv.sail (renamed from riscv.sail) | 0 | ||||
-rw-r--r-- | model/riscv_analysis.sail (renamed from riscv_analysis.sail) | 0 | ||||
-rw-r--r-- | model/riscv_duopod.sail (renamed from riscv_duopod.sail) | 0 | ||||
-rw-r--r-- | model/riscv_insts_begin.sail (renamed from riscv_insts_begin.sail) | 0 | ||||
-rw-r--r-- | model/riscv_insts_end.sail (renamed from riscv_insts_end.sail) | 0 | ||||
-rw-r--r-- | model/riscv_jalr_rmem.sail (renamed from riscv_jalr_rmem.sail) | 0 | ||||
-rw-r--r-- | model/riscv_jalr_seq.sail (renamed from riscv_jalr_seq.sail) | 0 | ||||
-rw-r--r-- | model/riscv_mem.sail (renamed from riscv_mem.sail) | 0 | ||||
-rw-r--r-- | model/riscv_platform.sail (renamed from riscv_platform.sail) | 0 | ||||
-rw-r--r-- | model/riscv_step.sail (renamed from riscv_step.sail) | 0 | ||||
-rw-r--r-- | model/riscv_sys.sail (renamed from riscv_sys.sail) | 0 | ||||
-rw-r--r-- | model/riscv_termination.sail (renamed from riscv_termination.sail) | 0 | ||||
-rw-r--r-- | model/riscv_types.sail (renamed from riscv_types.sail) | 0 | ||||
-rw-r--r-- | model/riscv_vmem.sail (renamed from riscv_vmem.sail) | 0 | ||||
-rw-r--r-- | model/rvfi_dii.sail (renamed from rvfi_dii.sail) | 0 | ||||
-rw-r--r-- | ocaml/_tags (renamed from _tags) | 0 | ||||
-rw-r--r-- | ocaml/_tags.bisect (renamed from _tags.bisect) | 0 | ||||
-rw-r--r-- | ocaml/platform.ml (renamed from platform.ml) | 0 | ||||
-rw-r--r-- | ocaml/platform_impl.ml (renamed from platform_impl.ml) | 0 | ||||
-rw-r--r-- | ocaml/platform_main.ml (renamed from platform_main.ml) | 0 | ||||
-rw-r--r-- | ocaml/tracecmp.ml (renamed from tracecmp.ml) | 0 | ||||
-rwxr-xr-x | test/run_tests.sh | 8 |
41 files changed, 128 insertions, 108 deletions
@@ -8,12 +8,12 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s SAIL_OTHER_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail SAIL_OTHER_RVFI_SRCS = prelude.sail rvfi_dii.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail -SAIL_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail -SAIL_RMEM_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail -SAIL_RVFI_SRCS = $(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail -SAIL_COQ_SRCS = $(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_termination.sail riscv_analysis.sail +SAIL_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail) +SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_RMEM_INST_SRCS) riscv_step.sail riscv_analysis.sail) +SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_OTHER_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_step.sail riscv_analysis.sail) +SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_OTHER_SRCS) $(SAIL_SEQ_INST_SRCS) riscv_termination.sail riscv_analysis.sail) -PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml +PLATFORM_OCAML_SRCS = $(addprefix ocaml/,platform.ml platform_impl.ml platform_main.ml) #Attempt to work with either sail from opam or built from repo in SAIL_DIR ifneq ($(SAIL_DIR),) @@ -33,10 +33,10 @@ BBV_DIR?=../bbv C_WARNINGS ?= #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function -C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h -C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c +C_INCS = $(addprefix c/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) +C_SRCS = $(addprefix c/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c) -C_FLAGS = -I $(SAIL_LIB_DIR) +C_FLAGS = -I $(SAIL_LIB_DIR) -I c C_LIBS = -lgmp -lz # The C simulator can be built to be linked against Spike for tandem-verification. @@ -57,135 +57,129 @@ else C_FLAGS += -O2 endif -all: platform riscv_sim riscv_isa riscv_coq +all: ocaml/platform c/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 +check: $(SAIL_SRCS) model/main.sail Makefile + $(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -interpret: $(SAIL_SRCS) - $(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) main.sail +interpret: $(SAIL_SRCS) model/main.sail + $(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -cgen: $(SAIL_SRCS) - $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) main.sail +cgen: $(SAIL_SRCS) model/main.sail + $(SAIL) -cgen $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail -_sbuild/riscv.ml: $(SAIL_SRCS) Makefile main.sail - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -o riscv $(SAIL_SRCS) +generated_models/ocaml/riscv.ml: $(SAIL_SRCS) Makefile + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml-nobuild -ocaml_build_dir generated_models/ocaml -o riscv $(SAIL_SRCS) -_sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Makefile - cp _tags $(PLATFORM_OCAML_SRCS) _sbuild - cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native +ocaml/_sbuild/platform_main.native: generated_models/ocaml/riscv.ml ocaml/_tags $(PLATFORM_OCAML_SRCS) Makefile + mkdir -p ocaml/_sbuild + cp ocaml/_tags $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml/_sbuild + cd ocaml/_sbuild && ocamlbuild -use-ocamlfind platform_main.native -_sbuild/coverage.native: _sbuild/riscv.ml _tags.bisect $(PLATFORM_OCAML_SRCS) Makefile - cp $(PLATFORM_OCAML_SRCS) _sbuild - cp _tags.bisect _sbuild/_tags - cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native && cp -L platform_main.native coverage.native +ocaml/_sbuild/coverage.native: ocaml/_sbuild/riscv.ml ocaml/_tags.bisect $(PLATFORM_OCAML_SRCS) Makefile + cp $(PLATFORM_OCAML_SRCS) generated_models/ocaml/*.ml ocaml/_sbuild + cp ocaml/_tags.bisect ocaml/_sbuild/_tags + cd ocaml/_sbuild && ocamlbuild -use-ocamlfind platform_main.native && cp -L platform_main.native coverage.native -platform: _sbuild/platform_main.native - rm -f $@ && ln -s $^ $@ +ocaml/platform: ocaml/_sbuild/platform_main.native + rm -f $@ && ln -s _sbuild/platform_main.native $@ -coverage: _sbuild/coverage.native - rm -f platform && ln -s $^ platform # since the test scripts runs this file - rm -rf bisect*.out bisect coverage - ../test/riscv/run_tests.sh # this will generate bisect*.out files in this directory - mkdir bisect && mv bisect*.out bisect/ - mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out +ocaml/coverage: ocaml/_sbuild/coverage.native + rm -f ocaml/platform && ln -s _sbuild/coverage.native ocaml/platform # since the test scripts runs this file + rm -rf bisect*.out bisect ocaml/coverage + ./test/run_tests.sh # this will generate bisect*.out files in this directory + mkdir ocaml/bisect && mv bisect*.out bisect/ + mkdir ocaml/coverage && bisect-ppx-report -html ocaml/coverage/ -I ocaml/_sbuild/ bisect/bisect*.out gcovr: gcovr -r . --html --html-detail -o index.html -riscv.c: $(SAIL_SRCS) main.sail Makefile - $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) main.sail 1> $@ +generated_models/ocaml/riscv_duopod_ocaml: model/prelude.sail model/riscv_duopod.sail + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_models/ocaml -o riscv_duopod_ocaml $^ -riscv_c: riscv.c $(C_INCS) $(C_SRCS) Makefile - gcc $(C_WARNINGS) $(C_FLAGS) riscv.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c -lgmp -lz -I $(SAIL_LIB_DIR) -o riscv_c +ocaml/tracecmp: ocaml/tracecmp.ml + ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ -riscv_model.c: $(SAIL_SRCS) main.sail Makefile - $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) main.sail 1> $@ +generated_models/c/riscv.c: $(SAIL_SRCS) model/main.sail Makefile + $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h $(SAIL_SRCS) model/main.sail 1> $@ -riscv_sim: riscv_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile - gcc -g $(C_WARNINGS) $(C_FLAGS) riscv_model.c riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ +c/riscv_c: generated_models/c/riscv.c $(C_INCS) $(C_SRCS) Makefile + gcc $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c -lgmp -lz -I $(SAIL_LIB_DIR) -o $@ -riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) main_rvfi.sail Makefile - $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) main_rvfi.sail | sed '/^[[:space:]]*$$/d' > $@ +generated_models/c/riscv_model.c: $(SAIL_SRCS) model/main.sail Makefile + $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail 1> $@ -riscv_rvfi: riscv_rvfi_model.c riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile - gcc -g $(C_WARNINGS) $(C_FLAGS) riscv_rvfi_model.c -DRVFI_DII riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ +c/riscv_sim: generated_models/c/riscv_model.c c/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile + gcc -g $(C_WARNINGS) $(C_FLAGS) $< c/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ -latex: $(SAIL_SRCS) Makefile - $(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS) +generated_models/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main_rvfi.sail Makefile + $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main_rvfi.sail | sed '/^[[:space:]]*$$/d' > $@ -tracecmp: tracecmp.ml - ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ +c/riscv_rvfi: generated_models/c/riscv_rvfi_model.c c/riscv_sim.c $(C_INCS) $(C_SRCS) $(CPP_SRCS) Makefile + gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII c/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ -riscv_duopod_ocaml: prelude.sail riscv_duopod.sail - $(SAIL) $(SAIL_FLAGS) -ocaml -o $@ $^ +latex: $(SAIL_SRCS) Makefile + $(SAIL) -latex -latex_prefix sail -o sail_ltx $(SAIL_SRCS) -riscv_duopod.lem: prelude.sail riscv_duopod.sail - $(SAIL) $(SAIL_FLAGS) -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ -Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem - lem -isa -outdir . -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - riscv_extras.lem \ - riscv_duopod_types.lem \ - riscv_duopod.lem +generated_models/lem/riscv_duopod.lem: $(addprefix model/, prelude.sail riscv_duopod.sail) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_models/lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ +generated_models/isabelle/Riscv_duopod.thy: generated_models/lem/riscv_duopod.lem lem/riscv_extras.lem + lem -isa -outdir generated_models/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ + lem/riscv_extras.lem \ + generated_models/lem/riscv_duopod_types.lem \ + generated_models/lem/riscv_duopod.lem -riscv_duopod: riscv_duopod_ocaml Riscv_duopod.thy +riscv_duopod: generated_models/ocaml/riscv_duopod_ocaml generated_models/isabelle/Riscv_duopod.thy -riscv_isa: Riscv.thy +riscv_isa: generated_models/isabelle/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 \ - riscv.lem - sed -i 's/datatype ast/datatype (plugins only: size) ast/' Riscv_types.thy +generated_models/lem/riscv.lem: $(SAIL_SRCS) Makefile + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_models/lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) -riscv.lem: $(SAIL_SRCS) Makefile - $(SAIL) $(SAIL_FLAGS) -lem -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) +generated_models/lem/riscv_sequential.lem: $(SAIL_SRCS) Makefile + $(SAIL_DIR)/sail -lem -lem_output_dir generated_models/lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) -riscv_sequential.lem: $(SAIL_SRCS) Makefile - $(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) +generated_models/isabelle/Riscv.thy: generated_models/lem/riscv.lem lem/riscv_extras.lem Makefile + lem -isa -outdir generated_models/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ + lem/riscv_extras.lem \ + generated_models/lem/riscv_types.lem \ + generated_models/lem/riscv.lem + sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_models/isabelle/Riscv_types.thy -riscvScript.sml : riscv.lem riscv_extras.lem - lem -hol -outdir . -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ +generated_models/hol4/riscvScript.sml: generated_models/lem/riscv.lem lem/riscv_extras.lem + lem -hol -outdir generated_models/hol4 -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \ - riscv_extras.lem \ - riscv_types.lem \ - riscv.lem + lem/riscv_extras.lem \ + generated_models/lem/riscv_types.lem \ + generated_models/lem/riscv.lem -riscvTheory.uo riscvTheory.ui: riscvScript.sml - Holmake riscvTheory.uo +$(addprefix generated_models/hol4/,riscvTheory.uo riscvTheory.ui): generated_models/hol4/riscvScript.sml + (cd generated_models/hol4 && Holmake riscvTheory.uo) -COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail +COQ_LIBS = -R $(BBV_DIR)/theories bbv -R $(SAIL_LIB_DIR)/coq Sail -R coq '' -R generated_models/coq '' -riscv_coq: riscv.v riscv_types.v +riscv_coq: $(addprefix generated_models/coq/,riscv.v riscv_types.v) -riscv.v riscv_types.v: $(SAIL_COQ_SRCS) Makefile - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_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 $^ +$(addprefix generated_models/coq/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_models/coq -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) +$(addprefix generated_models/coq/,riscv_duopod.v riscv_duopod_types.v): model/prelude.sail model/riscv_duopod.sail + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_models/coq -o riscv_duopod -coq_lib riscv_extras $^ %.vo: %.v coqc $(COQ_LIBS) $< -riscv.vo: riscv_types.vo riscv_extras.vo -riscv_duopod.vo: riscv_duopod_types.vo riscv_extras.vo +generated_models/coq/riscv.vo: generated_models/coq/riscv_types.vo coq/riscv_extras.vo +generated_models/coq/riscv_duopod.vo: generated_models/coq/riscv_duopod_types.vo coq/riscv_extras.vo # we exclude prelude.sail here, most code there should move to sail lib #LOC_FILES:=$(SAIL_SRCS) main.sail #include $(SAIL_DIR)/etc/loc.mk clean: - -rm -rf riscv _sbuild - -rm -f riscv.lem riscv_types.lem - -rm -f Riscv.thy Riscv_types.thy \ - Riscv_extras.thy - -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem - -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml - -rm -f platform_main.native platform coverage.native - -rm -f riscv.vo riscv_types.vo riscv_extras.vo riscv.v riscv_types.v - -rm -f riscv_duopod.vo riscv_duopod_types.vo riscv_duopod.v riscv_duopod_types.v - -rm -f riscv.c riscv_model.c riscv_sim - -rm -f riscv_rvfi_model.c riscv_rvfi + -rm -rf generated_models/ocaml/* generated_models/c/* + -rm -rf generated_models/lem/* generated_models/isabelle/* generated_models/hol4/* generated_models/coq/* + -rm -f c/riscv_sim c/riscv_rvfi + -rm -rf ocaml/_sbuild ocaml/_build ocaml/platform ocaml/tracecmp -rm -f *.gcno *.gcda -Holmake cleanAll ocamlbuild -clean @@ -10,10 +10,36 @@ with a terminal output device. Work on a 32-bit model is ongoing. The model specifies assembly language formats of the instructions, and implements the corresponding encoders and decoders. +Directory Structure +------------------- + +``` +sail-riscv +| ++---- model // Sail specification modules +| ++---- generated_models // Files generated by Sail +| | +| +---- c // C simulator definitions +| +---- ocaml // OCaml simulator definitions +| +---- lem // Lem model +| +---- isabelle // Isabelle model +| +---- coq // Coq model +| +---- hol4 // HOL4 model +| +| // Handwritten files ++---- c // C simulator ++---- ocaml // OCaml simulator ++---- lem // Lem library ++---- coq // Coq library +| ++---- test // unit test files +``` + An outline of the specification ------------------------------- -The model contains the following Sail modules: +The model contains the following Sail modules in the `model` directory: - `prelude.sail` contains useful Sail library functions @@ -51,9 +77,9 @@ your environment pointing to its top-level directory. ``` $ make ``` -will build the OCaml simulator in `platform`, the C simulator in -`riscv_sim`, the Isabelle model in `Riscv.thy`, and the Coq -model in `riscv.v`. +will build the OCaml simulator in `ocaml/platform`, the C simulator in +`c/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq +model in `generated_models/coq/riscv.v`. Executing test binaries ----------------------- @@ -61,11 +87,11 @@ Executing test binaries The C and OCaml simulators can be used to execute small test RV64 binaries. ``` -$ ./platform <elf-file> -$ ./riscv_sim <elf-file> +$ ./ocaml/platform <elf-file> +$ ./c/riscv_sim <elf-file> ``` Some information on additional configuration options for each simulator is available -from `./platform -h` and `./riscv_sim -h`. +from `./ocaml/platform -h` and `./c/riscv_sim -h`. Booting Linux with the C backend -------------------------------- @@ -77,7 +103,7 @@ a DTB (device-tree blob) file describing the platform (say in the file the model should be run as: ``` -$ ./riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ ./c/riscv_sim -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. @@ -88,7 +114,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. ``` -$ ./platform bbl > execution-trace.log 2> console.log +$ ./ocaml/platform bbl > execution-trace.log 2> console.log ``` Generating input files for Linux boot diff --git a/riscv_config.h b/c/riscv_config.h index f8f3eb3..f8f3eb3 100644 --- a/riscv_config.h +++ b/c/riscv_config.h diff --git a/riscv_platform.c b/c/riscv_platform.c index 3587206..3587206 100644 --- a/riscv_platform.c +++ b/c/riscv_platform.c diff --git a/riscv_platform.h b/c/riscv_platform.h index 728555e..728555e 100644 --- a/riscv_platform.h +++ b/c/riscv_platform.h diff --git a/riscv_platform_impl.c b/c/riscv_platform_impl.c index 04a661c..04a661c 100644 --- a/riscv_platform_impl.c +++ b/c/riscv_platform_impl.c diff --git a/riscv_platform_impl.h b/c/riscv_platform_impl.h index 85e25c9..85e25c9 100644 --- a/riscv_platform_impl.h +++ b/c/riscv_platform_impl.h diff --git a/riscv_prelude.c b/c/riscv_prelude.c index 1621913..1621913 100644 --- a/riscv_prelude.c +++ b/c/riscv_prelude.c diff --git a/riscv_prelude.h b/c/riscv_prelude.h index a296c7e..a296c7e 100644 --- a/riscv_prelude.h +++ b/c/riscv_prelude.h diff --git a/riscv_sail.h b/c/riscv_sail.h index 424b64b..424b64b 100644 --- a/riscv_sail.h +++ b/c/riscv_sail.h diff --git a/riscv_sim.c b/c/riscv_sim.c index 2a70167..2a70167 100644 --- a/riscv_sim.c +++ b/c/riscv_sim.c diff --git a/riscv_extras.v b/coq/riscv_extras.v index ff235a9..ff235a9 100644 --- a/riscv_extras.v +++ b/coq/riscv_extras.v diff --git a/Holmakefile b/hol4/Holmakefile index 8269bc3..8269bc3 100644 --- a/Holmakefile +++ b/hol4/Holmakefile diff --git a/riscv_extras.lem b/lem/riscv_extras.lem index c1a52c9..c1a52c9 100644 --- a/riscv_extras.lem +++ b/lem/riscv_extras.lem diff --git a/riscv_extras_sequential.lem b/lem/riscv_extras_sequential.lem index c1a52c9..c1a52c9 100644 --- a/riscv_extras_sequential.lem +++ b/lem/riscv_extras_sequential.lem diff --git a/main.sail b/model/main.sail index dbf41f4..dbf41f4 100644 --- a/main.sail +++ b/model/main.sail diff --git a/main_rvfi.sail b/model/main_rvfi.sail index 0ba4acf..0ba4acf 100644 --- a/main_rvfi.sail +++ b/model/main_rvfi.sail diff --git a/prelude.sail b/model/prelude.sail index c0e93e9..c0e93e9 100644 --- a/prelude.sail +++ b/model/prelude.sail diff --git a/riscv.sail b/model/riscv.sail index 6f1cd2e..6f1cd2e 100644 --- a/riscv.sail +++ b/model/riscv.sail diff --git a/riscv_analysis.sail b/model/riscv_analysis.sail index 34572f8..34572f8 100644 --- a/riscv_analysis.sail +++ b/model/riscv_analysis.sail diff --git a/riscv_duopod.sail b/model/riscv_duopod.sail index 0a5a7f8..0a5a7f8 100644 --- a/riscv_duopod.sail +++ b/model/riscv_duopod.sail diff --git a/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index 56fd8b4..56fd8b4 100644 --- a/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail diff --git a/riscv_insts_end.sail b/model/riscv_insts_end.sail index 144f06e..144f06e 100644 --- a/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail diff --git a/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index daf4bb0..daf4bb0 100644 --- a/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail diff --git a/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index fcf9526..fcf9526 100644 --- a/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail diff --git a/riscv_mem.sail b/model/riscv_mem.sail index 0b3e550..0b3e550 100644 --- a/riscv_mem.sail +++ b/model/riscv_mem.sail diff --git a/riscv_platform.sail b/model/riscv_platform.sail index aee72e4..aee72e4 100644 --- a/riscv_platform.sail +++ b/model/riscv_platform.sail diff --git a/riscv_step.sail b/model/riscv_step.sail index 755420d..755420d 100644 --- a/riscv_step.sail +++ b/model/riscv_step.sail diff --git a/riscv_sys.sail b/model/riscv_sys.sail index 450eb12..450eb12 100644 --- a/riscv_sys.sail +++ b/model/riscv_sys.sail diff --git a/riscv_termination.sail b/model/riscv_termination.sail index 6da4896..6da4896 100644 --- a/riscv_termination.sail +++ b/model/riscv_termination.sail diff --git a/riscv_types.sail b/model/riscv_types.sail index 4d012e0..4d012e0 100644 --- a/riscv_types.sail +++ b/model/riscv_types.sail diff --git a/riscv_vmem.sail b/model/riscv_vmem.sail index b617d29..b617d29 100644 --- a/riscv_vmem.sail +++ b/model/riscv_vmem.sail diff --git a/rvfi_dii.sail b/model/rvfi_dii.sail index 9680ab4..9680ab4 100644 --- a/rvfi_dii.sail +++ b/model/rvfi_dii.sail diff --git a/_tags.bisect b/ocaml/_tags.bisect index d3b996f..d3b996f 100644 --- a/_tags.bisect +++ b/ocaml/_tags.bisect diff --git a/platform.ml b/ocaml/platform.ml index 6ee2d2b..6ee2d2b 100644 --- a/platform.ml +++ b/ocaml/platform.ml diff --git a/platform_impl.ml b/ocaml/platform_impl.ml index 3eb8217..3eb8217 100644 --- a/platform_impl.ml +++ b/ocaml/platform_impl.ml diff --git a/platform_main.ml b/ocaml/platform_main.ml index 1c9ba20..1c9ba20 100644 --- a/platform_main.ml +++ b/ocaml/platform_main.ml diff --git a/tracecmp.ml b/ocaml/tracecmp.ml index 64a918d..64a918d 100644 --- a/tracecmp.ml +++ b/ocaml/tracecmp.ml diff --git a/test/run_tests.sh b/test/run_tests.sh index 04d72a2..491c64c 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -51,7 +51,7 @@ cd $RISCVDIR printf "Building RISCV specification...\n" -if make platform ; +if make ocaml/platform ; then green "Building RISCV specification" "ok" else @@ -59,7 +59,7 @@ else fi for test in $DIR/tests/*.elf; do - if $RISCVDIR/platform "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" + if $RISCVDIR/ocaml/platform "$test" >"${test/.elf/.out}" 2>&1 && grep -q SUCCESS "${test/.elf/.out}" then green "$(basename $test)" "ok" else @@ -69,7 +69,7 @@ done finish_suite "RISCV OCaml tests" -if make riscv_sim; +if make c/riscv_sim; then green "Building RISCV specification to C" "ok" else @@ -77,7 +77,7 @@ else fi for test in $DIR/tests/*.elf; do - if timeout 5 $RISCVDIR/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout + if timeout 5 $RISCVDIR/c/riscv_sim -p $test > ${test%.elf}.cout 2>&1 && grep -q SUCCESS ${test%.elf}.cout then green "$(basename $test)" "ok" else |